Zulip Chat Archive

Stream: general

Topic: Vscode recompiles after each character


view this post on Zulip Eric Wieser (Sep 22 2020 at 16:43):

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?

view this post on Zulip Alex Peattie (Sep 22 2020 at 16:46):

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

view this post on Zulip Alex Peattie (Sep 22 2020 at 16:46):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 16:49):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 16:49):

I currently have it set to "checking visible files"

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2020 at 16:51):

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

view this post on Zulip Yakov Pechersky (Sep 22 2020 at 16:54):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 16:59):

I have only one visible file open

view this post on Zulip Eric Wieser (Sep 22 2020 at 17:00):

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

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:02):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 17:11):

It's hitting me constantly at the moment

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:11):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 17:11):

What is that shortcut?

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:15):

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

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:15):

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

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:16):

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

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:18):

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

view this post on Zulip Heather Macbeth (Sep 22 2020 at 17:19):

Bryan Gin-ge Chen said:

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

view this post on Zulip Pedro Minicz (Sep 22 2020 at 17:19):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 17:21):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 22 2020 at 17:22):

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

view this post on Zulip Eric Wieser (Sep 22 2020 at 17:24):

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

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:39):

Did you try restarting VS Code?

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 17:40):

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)

view this post on Zulip Floris van Doorn (Sep 22 2020 at 18:54):

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.

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:18):

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

view this post on Zulip Edward Ayers (Sep 25 2020 at 17:11):

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.

view this post on Zulip Edward Ayers (Sep 25 2020 at 17:15):

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.

view this post on Zulip Floris van Doorn (Sep 25 2020 at 17:27):

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.

view this post on Zulip Eric Wieser (Sep 25 2020 at 19:52):

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?

view this post on Zulip Bryan Gin-ge Chen (Sep 25 2020 at 19:54):

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

view this post on Zulip Chris Hughes (Sep 26 2020 at 02:30):

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

view this post on Zulip Johan Commelin (Sep 26 2020 at 05:23):

That also seems to work for me


Last updated: May 15 2021 at 22:14 UTC