Strange behaviour of abbreviations feature with new VSCode

Stream: lean4

[Marc Huisinga]

Using the most recent VSCode update, some students at the theorem prover lab here noticed that when typing in abbreviations quickly, the cursor can jump to different places in the file. Afaict this issue did not exist before the most recent VSCode update. For instance, typing in \<\< quickly sometimes causes the cursor to jump in between the second \<, but students also reported that the cursor can jump to entirely different lines on different inputs. The issue with abbreviations not working also seems to occur more often according to students (I can't really reproduce this atm).
Has anyone else noticed similar issues, perhaps something that is easily reproducible?

[Gabriel Ebner]

I have also noticed this jumping around recently. But I thought that this was due to vim extension.

[Yakov Pechersky]

Yes, I've seen this. I agree that the vim extension might make this worse. But the largest determinant of this is CPU load.

[Gabriel Ebner]

Restarting vscode seems to help. I don't remember whether it was related to abbreviation usage or not.

[Eric Wieser]

I see this all the time with lean3, and am pretty sure it's a race condition because sometimes the only way for me to fix it is to type more slowly