Lingering lean processes

Stream: lean4

[Marcus Rossel]

I have an issue where Lean 4 sometimes seems to spawn many processes which stick around even after I quit VS Code. Unfortunately I don't know when exactly this happens, but I was just wondering if anybody else is having similar problems? I usually notice this issue by VS Code becoming super slow when working on Lean files.
Activity monitor then shows the following. Once I kill the lean processes manually, the system load goes way down.

[Patrick Massot]

The issue is much clearer on the second picture, it even says is seven times: "Apple" :stuck_out_tongue_wink:

[Floris van Doorn]

Yes, I sometimes have the same issue on Ubuntu and on Windows.

[Gabriel Ebner]

See also this thread here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/how.20to.20run.20.60lake.20exe.20cache.20get.60.20while.20in.20VSCode/near/341935382

[Shreyas Srinivas]

Marcus Rossel said:

I have an issue where Lean 4 sometimes seems to spawn many processes which stick around even after I quit VS Code. Unfortunately I don't know when exactly this happens, but I was just wondering if anybody else is having similar problems? I usually notice this issue by VS Code becoming super slow when working on Lean files.
Activity monitor then shows the following. Once I kill the lean processes manually, the system load goes way down.

I had this issue when on macOS whenever there was a typo w.r.t finsets and finset operations.