Vtec234
commented
3 months ago Have you noticed that a yellow tint appears on the location (myfile.lean:12:34) when it is loading? Are you requesting a more prominent indication?
Open hargoniX opened 3 months ago
Vtec234
commented
3 months ago Have you noticed that a yellow tint appears on the location (myfile.lean:12:34) when it is loading? Are you requesting a more prominent indication?
hargoniX
commented
3 months ago I do think a more prominent indication would be sensible yes. I talked to a few users and none of them (including myself) even noticed that this feature exists, let alone its meaning.
Proposal
Show some form of indicator for when the goal state that's currently being presented in the info view is out of date / being recomputed.
User Experience: Users can clearly judge when the information they are being presented is current. With recent features such as incrementality or the planned feature to show goals before the entire proof was elaborated this type of information becomes more important.
Beneficiaries: People that write large proofs on Lean releases with incrementality etc. know precisely when the information they are looking at is out of date/up to date.
Maintainability: Unclear.
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.