Zulip Chat Archive

Stream: general

Topic: VSCode regularly glitching, to the point on unusability


Scott Morrison (Feb 27 2022 at 01:10):

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 (Feb 27 2022 at 01:15):

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 (Feb 27 2022 at 01:18):

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 (Feb 27 2022 at 01:19):

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 (Feb 27 2022 at 01:21):

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 (Feb 27 2022 at 01:21):

PS what are you using instead of the infoview?

Scott Morrison (Feb 27 2022 at 01:37):

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 (Feb 27 2022 at 01:39):

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 (Feb 27 2022 at 01:42):

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 (Feb 27 2022 at 01:42):

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

Scott Morrison (Feb 27 2022 at 02:16):

Or not... same problem returns.

Mario Carneiro (Feb 27 2022 at 08:19):

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 (Feb 27 2022 at 08:28):

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

Damiano Testa (Feb 27 2022 at 08:30):

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 (Feb 27 2022 at 13:36):

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 (Feb 27 2022 at 13:41):

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 (Feb 27 2022 at 13:54):

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 (Feb 27 2022 at 13:58):

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 (Feb 27 2022 at 14:18):

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 (Feb 27 2022 at 14:49):

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 (Feb 27 2022 at 15:02):

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

Bhavik Mehta (Feb 27 2022 at 15:10):

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

Sebastian Ullrich (Feb 27 2022 at 15:13):

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 (Feb 27 2022 at 15:46):

I suspect this is more noticeable on underpowered machines.

Jireh Loreaux (Feb 27 2022 at 16:10):

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 (Feb 27 2022 at 17:07):

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 (Feb 27 2022 at 17:08):

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 (Feb 27 2022 at 17:08):

This pretty much fully stops the issue, in my experience

Bryan Gin-ge Chen (Feb 27 2022 at 17:10):

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 (Feb 27 2022 at 17:16):

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 (Feb 27 2022 at 17:19):

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

Eric Wieser (Feb 27 2022 at 18:36):

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

Eric Wieser (Feb 27 2022 at 18:48):

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

Bryan Gin-ge Chen (Feb 27 2022 at 18:51):

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 (Feb 28 2022 at 10:27):

@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 (Feb 28 2022 at 10:29):

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 (Feb 28 2022 at 10:34):

(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.)


Last updated: Dec 20 2023 at 11:08 UTC