Vscode recompiles after each character

Stream: general

[Eric Wieser]

While editing files within mathlib with vscode, I'm repeatedly finding that lean is recompiling after every single keypress, and my goal window painfully steps through

unknown identifier 's'
unknown identifier 'sl'
unknown identifier 'slo'
unknown identifier 'slow'

Restarting lean helps, but it seem to regress back to this state very quickly.

Has anyone else seen this behavior?

[Alex Peattie]

I think this is expected behaviour (in that VSCode should query the server each time you press a key, move your cursor etc.)...

It might be helpful to restrict what files/lines Lean is checking, if you open the Command Palette and type "lean check" you can see the various options (check open files only, check only lines above cursor etc.)

[Alex Peattie]

You can also access the settings by clicking on the part of the bottom blue bar that says "Lean: :checkbox:️ (checking open files)"

[Eric Wieser]

The problem is that 4 key events get queued, and the lean server seems to process them one at a time, rather than processing only the most recent

[Eric Wieser]

I currently have it set to "checking visible files"

[Bryan Gin-ge Chen]

This has happened to me too since the widget view came out. It's probably related to the discussion in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/katex/near/208358629

[Yakov Pechersky]

Patrick has suggested that it is due to having too many files open at the same time.

[Eric Wieser]

I have only one visible file open

[Eric Wieser]

And the ones in the background shouldn't matter if "check visible files" is selected, right?

[Kevin Buzzard]

I've also seen this phenomenon but I'm not sure how to reproduce it.

[Eric Wieser]

It's hitting me constantly at the moment

[Pedro Minicz]

For this exact reason I added a keyboard shortcut for pausing the proof state buffer.

[Eric Wieser]

What is that shortcut?

[Pedro Minicz]

It is custom made, I mapped it to ctrl+k, however that was a few months ago

[Pedro Minicz]

I am trying to find the thread I created here a while ago, the shortcut was someone's suggestion...

[Pedro Minicz]

And I am no longer sure how I made it :cry:

[Heather Macbeth]

found it! (I was there too)
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/lean.20for.20coq.20users.3F

[Heather Macbeth]

Bryan Gin-ge Chen said:

Not by default, but you can add one by searching for "toggle updating" in VS Code's keyboard shortcuts.

[Pedro Minicz]

Heather Macbeth said:

Bryan Gin-ge Chen said:

Not by default, but you can add one by searching for "toggle updating" in VS Code's keyboard shortcuts.

For future reference: File > Preferences > Keyboard Shortcuts

[Eric Wieser]

Unfortunately pausing does not appear to stop the compilation, the orange bars in the editor pane still flash up over and over again

[Bryan Gin-ge Chen]

Sometimes restarting Lean can get it out of these cycles. ctrl+p and search for "Lean: restart".

[Eric Wieser]

That does fix the problem, but the cycle restarts only a few seconds later

[Kevin Buzzard]

Did you try restarting VS Code?

[Kevin Buzzard]

I can't remember what I did which made Lean stop acting weird like this, but I've seen it a few times (not regularly though)

[Floris van Doorn]

I've seen this plenty of times. I'm also not sure what causes it, but usually it happens when I switch branches/files a couple times (sometimes it happens just after a "Jump to Definition" to a different file). I've also noticed that "Lean: Restart" doesn't really solve it. I tend to close VSCode, do another leanproject get-cache and reopen VSCode, which tends to fix it.

[Eric Wieser]

What if I have local commits, and leanproject get-cache can't find anything?

[Edward Ayers]

I think this is the same bug: https://github.com/leanprover-community/lean/issues/379
I'm not sure what's causing it but somewhere deep in the server code, tasks aren't being cancelled and it ends up recompiling everything after every keypress. I had a go at finding the cause but I couldn't track it down.

I can get it to reliably slow down to the point of being awful by having multiple code windows open and pinning a goal state in a later window. It looks like it ends up making vast numbers of 'checking import for sorry' tasks.

[Edward Ayers]

It might be caused by the new extension window which polls the server every few seconds if the info stored at its position is not ready yet, and these requests are not being cancelled properly and all trigger a long-running operation.

[Floris van Doorn]

Eric Wieser said:

What if I have local commits, and leanproject get-cache can't find anything?

Two options:

• git checkout the latest commit that does exist in leanprover-community/mathlib, leanproject get-cache and then git checkout your branch/commit again.
• Push your commits to a branch of mathlib, and wait for it to compile.

Option 1 is good if you haven't changed low-level files in your commits. If you did, use option 2.

[Eric Wieser]

Unfortunately I've been doing a lot of low-level stuff recently. Would it be possible to have the azure upload of oleans happen in parallel with the GitHub build, rather that only when it completes?

[Bryan Gin-ge Chen]

It's not really feasible with the current setup since the oleans are distributed as a single .tar.xz file.

[Chris Hughes]

Whenever I have this problem it can usually be fixed by closing files that depend on the file I'm editing.

[Johan Commelin]

That also seems to work for me