Freeze the Lean Infoview while typing

Stream: new members

[Giovanni Mascellani]

Hi, I installed Lean and the VSCode extension following the instructions on https://leanprover-community.github.io/install/macos.html. When writing proofs with VSCode, it often happens that I start typing, e.g., a tactic name, and then realize that I would like to check again the current proof state, because maybe I don't remember which hypothesis I wanted to refer. However, by that time, the Lean source code does not parse, and the Lean Infoview box doesn't display any helpful information. I need to either delete what I've written, or complete it somehow to have the information back. It's not terrible, but it wastes my focus. Is there a way to keep the Infoview frozen while the source code doesn't parse?

[Johan Commelin]

Are you using Lean 3? If so, you can click the pause :pause: button in the Info View.

[Johan Commelin]

(Not sure if Lean 4 already has that.)

[Giovanni Mascellani]

Thanks for your answer. Yes, I am using Lean 3 and that button works for me. Though it's not ideal, it still means that I have to do that in advance and it requires an explicit action on my side, both to lock and to unlock (BTW, does it have a keyboard shortcut? It would be better then having to click with the mouse already). I was hoping for something more automatical.

[Bryan Gin-ge Chen]

There isn't a default keybind, but you can bind a key to it if you click the gear in the bottom left of VS Code, select Keyboard Shortcuts, and then search for "Lean: Info View: Toggle Updating".

[Patrick Johnson]

Coq IDE doesn't update proof state as you type, and instead you need to update it explicitly after each line. I personally find it more natural, because it allows me to watch the current proof state while typing the next tactic. It will be nice if we can have such option in Lean 4.

[Patrick Johnson]

Currently (in Lean 3) the people who dislike update-as-you-type feature need to toggle updating two times after each proof line (once to see the new proof state, and again to freeze the infoview again).

[Wojciech Nawrocki]

Patrick Johnson said:

Currently (in Lean 3) the people who dislike update-as-you-type feature need to toggle updating two times after each proof line (once to see the new proof state, and again to freeze the infoview again).

In Lean 4 you can keep the view paused as there is an 'update' button you can click when appropriate. It doesn't appear to have a corresponding command so it cannot be bound to a key, but it would be pretty easy to add such a command.

[Damiano Testa]

I sometimes add -- at the beginning of a line that I am typing to comment out the line and prevent lean from updating too much. Lean still elaborates, before it realizes that nothing has changed.

The advantage over the pause button is that this is something that can be done "after the fact".

[Giovanni Mascellani]

Damiano Testa said:

I sometimes add -- at the beginning of a line that I am typing to comment out the line and prevent lean from updating too much. Lean still elaborates, before it realizes that nothing has changed.

That's an interesting idea. Combined with the key combination that toggles the comment on the current line (Shift-Command-7 by default on Mac) gives a relatively good approximation of what I wanted. Thanks!

[Ryan McCorvie]

I've also been trying to figure out the best keyboard workflow for Lean in VSCode.

With Lean, sometimes I wish for something like F9 in excel, for "recalcate all formulas". I'm going to experiment with the "update" button. I get frustrated by the fact that typing often destroys the context display, so I've also hit on the trick of putting in a sorry as the final tactic then commenting lines while they are being edited. On windows, ctrl-/ toggles a comment. On the other hand, since the infoview is dependent on the cursor location, I sometimes find myself moving character-by-character to see the feedback at different locations, and this is harder with explicit refresh. I'm used to REPL environments in scripting languages where there's an explicit key stroke to evaluate each new statement or command, but I can see how REPL may not be well suited for Lean.