vim extension on VSCode

Stream: general

[Yakov Pechersky]

I use the vim bindings extension in VSCode. When I am typing in an open lean file, the VSCode Lean extension tries to recompile even while I am still typing, which results in a lot more lag in getting a response from the widget. It gets hung up on things like unmatched parens, or unknown tokens. Has anyone else faced this?

[Frédéric Dupuis]

Yeah -- is it really specific to the vim extension? It would be nice to have a shortcut to start/stop the compilation.

[Bhavik Mehta]

Yeah I've had this too, it's really frustrating

[Gabriel Ebner]

This is typically because you have two files open that are on the opposite end of the import hierarchy (like tactic.core and geometry.manifold.mfderiv).

[Alex Peattie]

Frédéric Dupuis said:

Yeah -- is it really specific to the vim extension? It would be nice to have a shortcut to start/stop the compilation.

I believe you can open the Command Palette and choose "Lean: Check Nothing" to disable compilation :relaxed:

[Alex Peattie]

And more generally you can use the "Lean: Check ..." commands to control how aggressive Lean/VSCode will be about compiling. For example "Lean: Check visible files" should stop the problem Gabriel mentioned caused by imports

[Alex Peattie]

You can also access the settings by clicking on the part of the bottom blue bar that says "Lean: :checkbox:️ (checking open files)"

[Frédéric Dupuis]

Thanks! Do you know if there's a way to turn this into keyboard shortcuts? I was hoping to be able to do this very quickly when moving large blocks of code around.

[Bryan Gin-ge Chen]

Yes, it is possible. The command names for those selections are here (click on "The choices can also be made directly:") and then you can add custom keybindings for those.

To do so, open "Keyboard Shortcuts" in VS Code via the menu in the bottom left gear (or press ctrl+k then ctrl+s, or search the ctrl+p menu). Then search for lean.roiMode.

[Patrick Massot]

I suspect this is hiding a deeper issue though. I've been using Lean for a long time, including editing mathlib and I never felt the need to constantly change this setting.

[Yakov Pechersky]

I think it has to do with how the vim extension is firing keypress events into VSCode itself. For example, it has a separate undo stack (via u) than the VSCode ctrl-Z stack. And ctrl-z will sometimes undo a keypress at a time, which isn't really how undo should work.

[Patrick Massot]

I'm also using the vim extension (both of them actually, depending on the computer).

[Patrick Massot]

And vim undo in VSCode is a completely unpredictable nightmare.

[Yakov Pechersky]

So every time it fires the keypress event, it triggers the underlying "visible file has changed" event for sending the buffer to the lean server. As opposed to waiting for input to stop via your Esc sequence.

[Gabriel Ebner]

Relevant vscodevim bug: https://github.com/VSCodeVim/Vim/issues/1490#issuecomment-352167221

[Yakov Pechersky]

Basically, I'm saying, as exemplified by the weird vim undo in VSCode is that the vim extension doesn't play nicely with what counts as a changing (right now, in this moment) buffer over a buffer that has recently been changed (and isn't about to).

[Yakov Pechersky]

And my guess is that the vim extension always makes it seem like the latter to VSCode and other extensions, even when it is really the former.