vscode cursor position bug

Stream: lean4

[Geoffrey Irving]

I'm hitting a weird bug in VSCode which makes it hard to add new lemmas to a simp list (which is a thing I do a lot!). Basically, if I type something like \left (space at the end) to enter a unicode character, after the space the cursor position is wrong (and thus continuing to type does weird stuff. Here's a movie showing the cursor position issue:

vscode-lean-bug.mov

Anyone else hitting this? I can file it if it seems new.

I'm using

1. Version: 1.85.2 (Universal)Commit: 8b3775030ed1a69b13e4f4c628c612
2. VSCode Lean plugin v0.0.125
3. VSCode Vim plugin v1.27.2
4. Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

This is new: I think it started today or yesterday.

[Michael Stoll]

I've been experiencing similar problems for quite some time. It appears to be somewhat random whether the cursor is where you expect it or one position to the left. See vscode-lean4#332 and here.

[Geoffrey Irving]

Yes, I was getting the off by one thing too: sometimes it would appear right after the unicode character (no space), and sometimes it would leave a space. But now it's full haywire and it's often several steps to the right, on top of other text.

[Geoffrey Irving]

Ah, neat, and it was just (hopefully) fixed!

[Geoffrey Irving]

Though it seems the v0.0.125 version that I'm using includes those fixes (https://github.com/leanprover/vscode-lean4/releases/tag/v0.0.125), so it's possible those fixes are what recently made the problem way worse.

[Marc Huisinga]

Are you using any other extensions that may affect input?

[Michael Stoll]

OK; I wasn't reading carefully enough. Come to think of it, I don't think I had the "off-by-one" problem recently...

[Geoffrey Irving]

Marc Huisinga said:

Are you using any other extensions that may affect input?

Yes, VSCode Vim plugin v1.27.2 as mentioned.

[Marc Huisinga]

Yes, it looks like that's the culprit. I can't reproduce the issue without the Vim plugin but I can reproduce it with it.

[Joachim Breitner]

Also observing this, I kinda assumed it must be some local oddity (vim extension), because if it'd affect the default setup, it would be known already :-)

[Marc Huisinga]

Before the mitigation for the abbreviation issues, the VS Code extension would execute an edit against the text editor and then always manually displace the cursor afterwards. Since the text can change in-between those two points in time, the cursor placement was sometimes wrong.
The mitigation now instead uses VS Code's builtin method of moving the cursor, so that the cursor move and text edit occur atomically.
Either the Vim plugin does some manual cursor manipulation of its own, or the edits that it sends to VS Code somehow interfere with that of vscode-lean4, making VS Code decide that the cursor now needs to be placed after that word.

[Marc Huisinga]

I'll look into it tomorrow, but I suspect that there might be no good fix for this. Maybe I can add a fallback to the old behavior for Vim plugin users, though that will still exhibit the race condition bugs that occurred before.

[Geoffrey Irving]

Thank you! The new behavior is quite difficult to work with, so while it would be nice to have determinism the new behavior is reliably bad.

[Jireh Loreaux]

So, interestingly, I have all the same info as Geoffrey, except I'm on VS Code 1.85.1 instead of 1.85.2, and I use the Vim extension, but I don't reproduce his issue.

[Geoffrey Irving]

Using https://github.com/vscode-neovim/vscode-neovim as the Vim plugin instead seems to fix it (hard to wait for a fix since it's hard for me to type without working vim + unicode).

[Geoffrey Irving]

So I am set for now. :)

[Marc Huisinga]

Jireh Loreaux said:

So, interestingly, I have all the same info as Geoffrey, except I'm on VS Code 1.85.1 instead of 1.85.2, and I use the Vim extension, but I don't reproduce his issue.

There's a chance that it's affected by the order in which VS Code decides to execute both extensions, but I don't think that we can change that regardless.

[Geoffrey Irving]

Thank you for struggling through what sounds like broken surrounding software! The lack of transactions seems like a major glitch.

[Marc Huisinga]

The mitigation suggested above has been released now and you should be able to use vscode-lean4 together with VSCodeVim again. Nonetheless, using the NeoVim plugin instead is preferable because it is not subject to abbreviation race conditions.

[Geoffrey Irving]

I do think the neovim plugin feels quite a bit snappier, possibly because of those race conditions. Though it does have some other (much less bad) bugs: https://github.com/vscode-neovim/vscode-neovim/issues/1766