Potential vscode extension issue

Stream: lean4

[Shreyas Srinivas]

OS : Ubuntu 24.04
Issue : On upgrading from vscode from 1.89.1 to 1.90, my open lean project got ridiculously laggy and slow. I didn't observe anything nearly as bad with other projects.
Tentative fix: I have fixed this issue by reverting to 1.89.1 for now. The lean project window is fast again.
Is this just me or did anybody else encounter this as well?

[Yaël Dillies]

No issue over here in gitpod

[Ira Fesefeldt]

I have the same problem. Its now the second time I had to revert back to 1.89...

[Shreyas Srinivas]

Same here. This is the second time I have reverted versions recently

[Marc Huisinga]

There are a dozen-or-so reports of this issue on the VS Code issue tracker, even for people using VS Code without any extensions.