## Stream: general

### Topic: Vscode recompiles after each character

#### 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?

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

#### 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)"

#### 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

#### Eric Wieser (Sep 22 2020 at 16:49):

I currently have it set to "checking visible files"

#### 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

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

#### Eric Wieser (Sep 22 2020 at 16:59):

I have only one visible file open

#### Eric Wieser (Sep 22 2020 at 17:00):

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

#### Kevin Buzzard (Sep 22 2020 at 17:02):

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

#### Eric Wieser (Sep 22 2020 at 17:11):

It's hitting me constantly at the moment

#### Pedro Minicz (Sep 22 2020 at 17:11):

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

#### Eric Wieser (Sep 22 2020 at 17:11):

What is that shortcut?

#### 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

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

#### Pedro Minicz (Sep 22 2020 at 17:16):

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

#### 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

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

#### 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

#### 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

#### 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".

#### Eric Wieser (Sep 22 2020 at 17:24):

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

#### Kevin Buzzard (Sep 22 2020 at 17:39):

Did you try restarting VS Code?

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

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

#### Eric Wieser (Sep 25 2020 at 15:18):

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

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

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

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

#### 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?

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

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

#### Johan Commelin (Sep 26 2020 at 05:23):

That also seems to work for me

Last updated: May 15 2021 at 22:14 UTC