feat: replace stale dep notifs with "restart file" infoview button

[mhuisi]

This PR adds a "Restart File" button to the bottom right of the InfoView and deletes stale dependency notifications entirely.
I've found the latter to be way too noisy, especially now that Lean 4 on master will inform us about stale dependencies as soon as the dependency changes (it's especially noisy when switching branches).
The central issue with the notifications is that they stick around even after you switch away from the file.

Now, after fixing the fullRange behavior of the extension, the stale dependency diagnostic will be displayed in "Messages" anywhere in the file. The button in the InfoView should also be sufficiently visible that after reading the message, users know what to do.

This PR also fixes a bug where the InfoView would not correctly display the "imports out of date" error in the InfoView because the server doesn't respond to requests when it doesn't keep going after processing the header.

[Vtec234]

I can confirm this works, but I don't love the look of the button. It is really distracting and visually distinct from all the other buttons (which use codicons instead of the webview-ui-toolkit). It makes it look like you're supposed to click it as soon as it shows up, given how prominent it is. Is an infoview button really needed for this, i.e., why is having access to the 'restart file' command not sufficient? If users aren't aware of it, could we simply change the message to point them to it?

[mhuisi]

It is really distracting and visually distinct from all the other buttons (which use codicons instead of the webview-ui-toolkit).

I don't consider all the other buttons in the InfoView integral for working with Lean - you can get along fine without knowing about them, and I'm sure that most users never use any of the codicon buttons specifically because they don't stick out much. "Restart File" however is central to working with Lean and you often cannot even get started with working on a file without using it.

This kind of button shouldn't be hidden away behind an obscure keybinding, a menu with an obscure icon or an obscure feature like the command palette. It should be immediately visible and immediately accessible within a single click.

Is an infoview button really needed for this, i.e., why is having access to the 'restart file' command not sufficient?

For one, mouse-heavy users may find it annoying to use the command palette (you have to take your hand off the mouse to type in the command you want). This is important because "Restart File" is typically something you use while navigating code, not while writing code. The forall menu is easier to access, but it still requires multiple clicks to run the command, which I find especially annoying when using Lean with a touchpad. The keybinding is the best option even for mouse-heavy users (at least as long as your mouse is on the right side of the keyboard), but I suspect certain user groups of Lean (e.g. math undergrads) aren't used to heavy use of keybindings and may avoid it due to a general unfamiliarity with keybindings.

If users aren't aware of it, could we simply change the message to point them to it?

I'm hesitant to have the language server emit diagnostics that are specific to the VS Code extension. Another option is to hack the InfoView to display a more specific message for the stale dependency diagnostics (perhaps even with a link to run the command), but this is very ugly to maintain, especially as Lean 4 evolves, so I decided against it. The stale dependency notifications do this, and I'm very unhappy with it.

[Screenshot]

I don't think the screenshot you posted is fair. Here's what it looks like on a regular 1920x1080 screen at 125% scaling (i.e. for use on a small 13 inch laptop screen):

I find the whole "Restart File" situation to be generally unfortunate from a UX standpoint especially for less technically inclined users, but there's sadly nothing we can do about it at this point.

[Vtec234]

You mentioned that this will be urgently needed for the next Lean RC, and I don't want to block you on that. The implementation looks fine at a glance (I did not review in detail). I would midly prefer not to pull in a dependency on webview-ui-toolkit and just use plain CSS to style the button, but I will leave that decision to you.

"Restart File" however is central to working with Lean and you often cannot even get started with working on a file without using it.
I find the whole "Restart File" situation to be generally unfortunate from a UX standpoint especially for less technically inclined users, but there's sadly nothing we can do about it at this point.

Maybe the central issue that has to be addressed is not the button or lack thereof, but this point about the system's design. At various points we discussed re-adding an option for users to configure the server to behave a bit more like Lean 3 and auto-reload any file whose dependencies have changed. It is already computing stale dep notifications, so it sounds like that might not be too complex implementation-wise. The original issue in Lean 3, noted on Lean.Server, was that given a dep chain A->B, Lean 3 would refresh A as soon as B changed even if B wasn't saved. I think it would be completely okay to refresh only if the user saves B; this way accidental changes don't trigger recompilation, but the 'restart file' notifications/button become less frequently needed. What do you think? Why do you say nothing can be done?

[Kha]

Automatically rebuilding saved files was the previous Lean 4 behavior, people did not like it. Thus the status quo.

edit: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Imports/near/268441788

[mhuisi]

It is already computing stale dep notifications, so it sounds like that might not be too complex implementation-wise.

It's worth pointing out that this is not perfect, since we use file watchers and didSave notifications to issue the diagnostic, so triggering a rebuild whenever users see the diagnostic will be too frequent. Only when opening the file do we actually query Lake to detect stale dependencies, since we don't want to poll Lake for every file worker. There are several ways to improve this, but each is currently too expensive to implement.

I think it would be completely okay to refresh only if the user saves B; this way accidental changes don't trigger recompilation, but the 'restart file' notifications/button become less frequently needed.

As Sebastian mentioned above, we've seen a lot of feedback from Mathlib users that manually indicating that they want to trigger a rebuild is what they want, even when initially opening a file and well after saving a change.

Why do you say nothing can be done?

Because we've tried more automatic approaches and people strongly expressed that they were unhappy with them.

The fundamental problem is that getting the semantic information back in sync after a change is so expensive in Lean and that so many files need to be rebuilt entirely. If this could be improved and both cost and latency to get the language server back in sync were acceptable, then we could move to an interaction model that is closer to other language servers.

[Vtec234]

Automatically rebuilding saved files was the previous Lean 4 behavior, people did not like it. Thus the status quo.

edit: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Imports/near/268441788

As Sebastian mentioned above, we've seen a lot of feedback from Mathlib users that manually indicating that they want to trigger a rebuild is what they want

I can see Gabriel expressing a preference there because he has autosave on, so that rebuild-saved-files is equivalent to rebuild-changed-files. Other strongly prefer the other behaviour. One thing I missed in our discussion here is that there already is an option to auto-rebuild when opening a file! But there is no option to also auto-rebuild when a dependency changes and the file is already open. As you mention Marc, this could result in unnecessarily eager rebuilds, but I still think it would be great to have such an option (off by default).

Also, I am realizing now (after merge; sorry) that there is a regression in the UI: Lean no longer indicates that there exist dependencies that have changed. Could we have a followup PR making the Restart File button become yellow when this happens? This would be analogous to how other UI elements are yellow when something is loading.

[mhuisi]

Also, I am realizing now (after merge; sorry) that there is a regression in the UI: Lean no longer indicates that there exist dependencies that have changed. Could we have a followup PR making the Restart File button become yellow when this happens? This would be analogous to how other UI elements are yellow when something is loading.

The diagnostic should be visible under 'Messages' (modulo #424).

[Vtec234]

You're right, my bad.

[mhuisi]

I can see Gabriel expressing a preference there because he has autosave on, so that rebuild-saved-files is equivalent to rebuild-changed-files. Other strongly prefer the other behaviour. One thing I missed in our discussion here is that there already is an option to auto-rebuild when opening a file! But there is no option to also auto-rebuild when a dependency changes and the file is already open. As you mention Marc, this could result in unnecessarily eager rebuilds, but I still think it would be great to have such an option (off by default).

I don't mind supporting an option for this. I'll put it on my to-do list :-)