VSCode regularly glitching, to the point on unusability

Stream: general

[Scott Morrison]

I've been suffering in silence with this issue for a while, so I thought I should report it in case others are too, and to ask for help.

VSCode regularly (i.e. every session) reaches a state as illustrated in the attached video. Every key stroke causes a recompilation, and the interface lags out many many seconds behind my typing. I can recover by restarting the server or restarting VSCode, but usually within at most a few minutes (and often instantly) I am back in the same state.

https://youtu.be/7xS4WfDrcHE

[Kevin Buzzard]

I've certainly experienced this, but much more rarely, and if I fix it by restarting VS Code then the problem goes away and doesn't come back. However nowadays I am typically working with very short and simple files in a repo which depends on a fully compiled mathlib which I never mess with.

[Scott Morrison]

Yeah. Today I have been working deep at the bottom of the mathlib hierarchy, so I suspect this behaviour is correlated with that.

[Scott Morrison]

Oh. I did just realise I have the Lean extension set to the default limit of 4gb RAM. I'll change that to 40gb and see if things get better. :-)

[Kevin Buzzard]

The other thing one can try is closing all files other than the one you're working on. But I guess it would be good if you could reliably get this to happen (I never could)

[Kevin Buzzard]

PS what are you using instead of the infoview?

[Scott Morrison]

Ah, I'd forgotten that was an extension --- it is the "Error Lens" extension, which is very nice, putting messages inline in the editor! It often means for simple stuff you can avoid needing the infoview.

[Bryan Gin-ge Chen]

If you can get Lean in this state, it might be interesting to see if the server is doing something crazy. If you open the control palette (ctrl+shift+P / cmd+shift+P) and search for "Developer: Open Webview Developer Tools", VS Code should pop up a browser debug window with a console at the bottom, and vscode-lean should be dumping all the messages from the server there.

[Bryan Gin-ge Chen]

Playing around with it a bit now, it looks like you do have to have the infoview window open for the console to show anything.

[Scott Morrison]

Oooh --- disabling the Error Lens extension seems to be helping...

[Scott Morrison]

Or not... same problem returns.

[Mario Carneiro]

The usual tricks I use if I end up in this state are to restart lean, close other files (especially ones that depend on the file I'm working on if it's deep in the dependency tree), and put #exit right after the command I'm working on so that elaborating the rest of the file is quick (which speeds up that character-to-character loop in the video)

[Eric Wieser]

I've had this exact behavior many times before, thanks for getting it on video

[Damiano Testa]

I sometime copy the file content to a different gitgnored file and edit that one, to avoid dependencies.

Sorry if this is a too-obvious-to-even-state trick!

[Sebastian Reichelt]

I also get this really often (in Lean 4) and use the #exit trick for basically every single edit. I don't know if this was recently added as a feature, but increasing the compilation delay in the vscode extension settings helps a lot.

[Bryan Gin-ge Chen]

I'm curious if anyone who sees this is able to check the webview developer console when Lean gets in this state per my suggestion above. It might help in figuring out what's going on.

[Sebastian Reichelt]

I don't get any messages there. But regarding "something crazy", I can indeed reproduce the problem in seconds by making an edit that breaks the entire (large) file, e.g. commenting out a universe declaration at the top.

[Sebastian Reichelt]

However, that is actually not the main reason I often run into this, I think. At least in Lean 4, it seems that when Lean is checking a complicated def, it can't be interrupted, but the extension will happily launch more checks in parallel after typing more characters. This may be somewhat specific to my code, though.

[Patrick Massot]

I also have the impression this is a fairly recent issue. I do get that from time to time, and I don't remember getting it a long time ago.

[Sebastian Ullrich]

Sebastian Reichelt said:

However, that is actually not the main reason I often run into this, I think. At least in Lean 4, it seems that when Lean is checking a complicated def, it can't be interrupted, but the extension will happily launch more checks in parallel after typing more characters. This may be somewhat specific to my code, though.

Yes, this is a current limitation in the Lean 4 elaborator/server interaction. It will never spawn more tasks than your CPU has cores though.

[Eric Wieser]

I don't think this is that recent (in lean 3), I've been seeing this behavior for months

[Bhavik Mehta]

Likewise, I'm pretty sure I've seen this occasionally for at least a year, but never consistently

[Sebastian Ullrich]

For what it's worth, I've never seen anything like that using Lean 4 + Emacs. Even when working in the middle of a file containing many, slow proofs.

[Eric Wieser]

I suspect this is more noticeable on underpowered machines.

[Jireh Loreaux]

Interestingly, my machine is not very powerful, and while I have had this problem from time to time, it's pretty infrequent for me, even when editing low-level files.

[Eric Rodriguez]

I think the cause of this is that Lean wants to greedily check far, far foward. In a large file, even checking to the bottom triggers this, but I find that the best way to reproduce this is to open a leaf file and then edit a file far higher up in the hierarchy that it depends on

[Eric Rodriguez]

I tend to try to put #exit after any code that I'm editing now for this reason (and . before if Lean is really acting up), and unless I'm actively working on two files at the same time (which I dislike doing in general) to close a file and THEN restart Lean before starting to work on another file that's on the same chain

[Eric Rodriguez]

This pretty much fully stops the issue, in my experience

[Bryan Gin-ge Chen]

It's been a long time since I've looked at the code for the extension, but if I remember correctly it shouldn't be sending changes to the server after every single keystroke; I thought there was a buffer of 100 ms or so...

[Eric Rodriguez]

I think this only buffers the changes, as I still remember painfully seeing "unknown identifier subm", "unknown identifier submo", "unknown identifier submod"...

[Bryan Gin-ge Chen]

I can't find the code I was thinking of so I might just be misremembering...

[Eric Wieser]

Is this 300ms relevant? https://github.com/leanprover/vscode-lean/blob/32cdc3fabbeb76b5f395f019f9bb6c3ee806dd85/src/server.ts#L31

[Eric Wieser]

Presumably when build_module is called here, the server should be cancelling any pending tasks to build the same module

[Bryan Gin-ge Chen]

Eric Wieser said:

Is this 300ms relevant? https://github.com/leanprover/vscode-lean/blob/32cdc3fabbeb76b5f395f019f9bb6c3ee806dd85/src/server.ts#L31

From a quick glance, it looks like the extension uses that LowPassFilter for a few different status requests to the server, but there doesn't look like there's any filtering / batching for server requests when typing (handled, as far as I can tell, in sync.ts).

[Gabriel Ebner]

@Scott Morrison This is a performance issue in the Lean 3 server. It happens when you open two files, one at the beginning of the hierarchy, and one at the end of the hierarchy. Editing the file at the beginning will be extremely laggy. The workaround is to close the other files, and restart the Lean server (with the vscode command).

[Gabriel Ebner]

Given the end-of-life status of Lean 3, I don't know if we should justify the time to fix this issue.

[Gabriel Ebner]

(Technical explanation: what happens is that on every file update the server receives, all reverse dependencies of the file are visited to recompile them. The recompilation happens asynchronously of course, but dependency resolution etc. all happens during the original file sync request. Thus: many reverse dependencies = laggy typing. We could try to handle the invalidation part of the file sync request asynchronously, this wouldn't fix everything but at least diagnostics etc. would still be responsive.)