Undo in VSCode using Vim undoes the previous `simp?` click

Stream: lean4

[Geoffrey Irving]

I'm using VSCode with the Vim extension. The following sequence of actions doesn't do what I expect:

1. Type a simp? [...]
2. Click on the expansion to get a concrete simp only [...] tactic
3. Do an unrelated text editing action
4. Type u to undo

What I expect to happen in (4) is that (3) is undone, but in fact both (3) and (2) are undone, leaving me with the simp? tactic which I have to click on again.

Is this a known problem?

[Patrick Massot]

undo is the main reason why I stopped using the vim extension in VSCode. The undo buffer of vim and VSCode simply can't seem to coexist peacefully (let alone cooperate).

[Geoffrey Irving]

Is there a better alternative, or do you just go without nice keybindings?

[Joachim Breitner]

Still using the extension, and getting used to things like undo with u, try to redo with Ctrl-R, noticing (again) that this doesn't work in VSCode, and then using Ctrl-u to undo the effect of u. It's surprising what kind of weird ways still build out muscle memory.

[Johan Commelin]

@Geoffrey Irving Are you aware of the Lean plugin for neovim? Several people use it and are quite happy with it.

[Geoffrey Irving]

Thank you, I wasn’t aware of that. This undo bug probably isn’t enough for me to switch, though.