## Stream: general

### Topic: vim extension on VSCode

#### 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?

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

#### Bhavik Mehta (Aug 24 2020 at 01:35):

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

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

#### 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:

#### 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

#### 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)"

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

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

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

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

#### Patrick Massot (Aug 24 2020 at 15:02):

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

#### Patrick Massot (Aug 24 2020 at 15:02):

And vim undo in VSCode is a completely unpredictable nightmare.

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

#### Gabriel Ebner (Aug 24 2020 at 15:11):

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

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

#### 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