Zulip Chat Archive

Stream: general

Topic: vim extension on VSCode


view this post on Zulip Yakov Pechersky (Aug 24 2020 at 01:07):

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?

view this post on Zulip Frédéric Dupuis (Aug 24 2020 at 01:33):

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

view this post on Zulip Bhavik Mehta (Aug 24 2020 at 01:35):

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

view this post on Zulip Gabriel Ebner (Aug 24 2020 at 08:05):

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).

view this post on Zulip Alex Peattie (Aug 24 2020 at 10:09):

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:

view this post on Zulip Alex Peattie (Aug 24 2020 at 10:11):

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

view this post on Zulip Alex Peattie (Aug 24 2020 at 10:13):

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

view this post on Zulip Frédéric Dupuis (Aug 24 2020 at 13:49):

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.

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2020 at 14:42):

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.

view this post on Zulip Patrick Massot (Aug 24 2020 at 14:45):

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.

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 15:01):

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.

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:02):

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

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:02):

And vim undo in VSCode is a completely unpredictable nightmare.

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 15:03):

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.

view this post on Zulip Gabriel Ebner (Aug 24 2020 at 15:11):

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

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 15:12):

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).

view this post on Zulip Yakov Pechersky (Aug 24 2020 at 15:12):

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.


Last updated: May 08 2021 at 18:17 UTC