Many Lean processes on Windows

Stream: lean4

[Floris van Doorn]

Can someone on Windows test the following:

1. Open Task Manager
2. Create a new file in Mathlib with the following contents and wait for Lean to finish compiling the file

import Mathlib


#check Ring
#check Field
#check Module.Finite
#check IsArtinian
#check Module.Free

3. I now have 2 visible processes lean.exe in the task manager
4. Jump to the definition of Ring, which opens in a new file, and wait for that file to finish compiling
5. Close the new tab
6. Repeat steps 4-5 for all other definitions.
7. Check how many processes lean.exe are running in the task manager

After each iteration of steps 4-5, I get one additional Lean executable running in the task manager, so at the end, lean.exe is running ~7 times. I am on Lean v4.22.0-rc3.

[Floris van Doorn]

After multiple such tasks, Lean can slow down significantly (probably because they are competing for CPU/Memory).

[Floris van Doorn]

Something that I couldn't quite make reproducible, but also had happen to me a few times: the task in my main editor stopped responding at all (the "yellow bar" wouldn't move past simple commands like a variable or attribute or set_option command, even after giving it 10+ seconds).
This happened when I was browsing the output of trace/profiler commands, sometimes jumping to definitions, sometimes editing the file a bit. (EDIT: posted this here #lean4 > Lean freezes with `#count_heartbeats` )

[Marc Huisinga]

I tried this on a Windows machine but can't seem to reproduce that the processes linger around after closing the tab.

[Floris van Doorn]

Hmm... Do you have any ideas how I could help diagnose this further (post logs, ways to try to minimize this behavior, or maybe I should try it on a fresh copy of Mathlib or something)?

[Floris van Doorn]

FWIW, I can still reproduce it without importing any Mathlib files (this is still a file in the Mathlib directory of my local copy of Mathlib:

import Lean
#check Nat
#check Int
#check Lean.MetaM
#check Lean.Parser.adaptCacheableContext

[Marc Huisinga]

(FWIW, I checked with a recent Mathlib on v4.22.0-rc4, probably good to double-check on that one first)

I think the first thing to check would be whether the language server gets the correct messages from VS Code. Set 'Lean 4 > Trace: Server' to 'compact', restart VS Code without any open tabs, open the Lean output window (command: 'Show Troubleshooting Output') and repeat your reproduction up to the step where you've closed the file for Ring and a process that shouldn't be there anymore is still sticking around. There should be a bunch of output in the 'Lean: Editor' panel that would be helpful to know about.

You could also try whether using gdb works on Windows (I think it's shipped with e.g. mingw) and then we can try looking at the backtraces.

1. Get your reproduction into the state where you have three processes, one of which shouldn't be there (for the closed tab).
2. Figure out the process ID (pid) of all of your lean processes (e.g. using the "Resource Monitor" on Windows)
3. One after another, run gdb -p <pid> for each of these process ID, and then thread apply all bt in gdb to get the backtraces. Copy each set of backtraces and then use quit to leave each gdb session.

[Floris van Doorn]

Ok, going through the steps:
I can still reproduce this on Lean v4.22-rc4.

[Floris van Doorn]

Here is the server trace file: https://gist.github.com/fpvandoorn/7e26b87fadde89db2e5432b6be99ae1a
I believe I closed the secondary file (Lean.Parser.Attr) at 6:53:44, and afterwards, I still see keepAlive notifications.

[Floris van Doorn]

Here is the output of gdb, of what I think is the process that shouldn't be there:
https://gist.github.com/fpvandoorn/8a4fa6c179053d5a0b7123e0fae6318f
Here is the output of gdb of another run with all three processes: (I think the second one, starting at line 273, is the one that shouldn't be there)
https://gist.github.com/fpvandoorn/e743b5e952345bf5f0928499876dd89d

[Floris van Doorn]

I hope this helps!

[Marc Huisinga]

Oh, interesting. I'm glad I asked for the LSP log - the client never emits a didClose notification for the document for some reason, so the server doesn't know to terminate the process.

It probably isn't the cause of the issue, but could you also ensure that both VS Code and the extension are up-to-date? The most recent VS Code version is 1.102.2 and the most recent extension version is 0.0.209.

[Marc Huisinga]

(I'd also be curious if anyone else with a Windows system can reproduce this / not reproduce it)

[Marc Huisinga]

Another shot in the dark: Are you running any other VS Code extensions? Does disabling them make a difference?

[Sébastien Gouëzel]

I just tried it on my windows system (windows 11, mathlib and vscode up to date), and I can't reproduce: when I close a tab, a Lean process disappears.

[Floris van Doorn]

I did update VSCode this morning. I now have the versions you mentioned for VSCode and the extension, and the issue still persists.
The issue also persists after disabling all extensions except the Lean 4 extension. (EDIT: this was false)

[Marc Huisinga]

Argh. I assume your settings.json doesn't contain any non-standard settings, either? (Settings > "Open Settings (JSON)" in the top right)

[Marc Huisinga]

(If that's not it either, I'll see if I can build you a custom version of the extension that produces more debug output)

[Marc Huisinga]

When debugging further, we found out that this problem is caused by the fairly common "GitHub Pull Requests" extension. If you have it installed, I'd recommend disabling it and restarting VS Code afterwards.
This issue is also independent of Windows, and running it myself while working on a TypeScript project caused some other strange bugs (e.g. issues in the "Problems" view for TypeScript wouldn't clear when closing the file, as it usually does).

I'm 90% sure that this issue is independent of Lean; VS Code will simply not emit any more didClose events for certain files when using this extension.

[Floris van Doorn]

Would it make sense to open an issue in their repo?

[Marc Huisinga]

I've created https://github.com/microsoft/vscode-pull-request-github/issues/7403