VSCode usage generates huge numbers of Lean processes

Stream: lean4

[Geoffrey Irving]

Recently VSCode (specifically the Cursor version) becomes unusable quite frequently because it generates many 10s of Lean processes until my system grinds to a halt. Anyone else seen this behavior with the Lean VSCode plugin? It's hard to fix when it occurs: sometimes killall lean solves the problem for a while, other times restarting Cursor on a Lean file means the problem reoccurs right away.

I'm on VSCode Lean plugin version 0.0.209, leanprover/lean4:v4.23.0-rc2. (I'm also using the Neovim plugin, but I would hope this doesn't interact in any way.)

[Robert Maxton]

Oh, so it's not just me then? (Also running Cursor.) Though, I'm not sure the problem is with Lean itself, as running the same files in e.g. Gitpod doesn't seem to have the same issues (though of course I have much less precise an idea of how much compute I'm actually using in that case)

I just tried nuking my .lake folder and rebuilding from scratch; it ... might have helped some things some, but it's still pretty bad

[Marc Huisinga]

Are you using the GitHub Pull Requests extension by any chance?

[Marc Huisinga]

(Previous discussion: #lean4 > Many Lean processes on Windows @ 💬)

[Robert Maxton]

I am not, but I am using a Git MCP for Cursor. I've tried disabling it; I'll see if the problem goes away

[Marc Huisinga]

It would also be good to know if the issue only occurs with Cursor, or with regular VS Code as well

[Robert Maxton]

Marc Huisinga said:

It would also be good to know if the issue only occurs with Cursor, or with regular VS Code as well

Disabling the Git MCP did not help, but indeed the problem seems to be restricted to Cursor.

[Kim Morrison]

I started seeing this today as well.

[Marc Huisinga]

I briefly tried reproducing this with Cursor, but didn't see the issue occur. Please let me know if you find a reproduction.

[Geoffrey Irving]

This still hits me reliably after I start doing things with https://github.com/girving/ray. The most recent thing I did was open up Tanh.lean and try to convert from using AnalyticAt to ContDiffAt. After a minute or two my machine grinds to a halt. I don't have a precise reproducing sequence, and it does take a minute or two.

[Marc Huisinga]

I can't reproduce on that file with a fresh Cursor install, either. Does this issue reproduce for you on a fresh install (without being logged in), too?

If I had to give a totally blind guess, Cursor might be opening lots of random Lean documents that aren't opened as an editor to query information from the language server and provide additional context to AI. Since this issue doesn't occur in VS Code, I'd recommend creating a bug report on the Cursor issue tracker.

[Yuri]

FWIW, I have been dealing with a similar problem on and off since last week. Once it happens the user experience is painful.

I wish I had a reproducible case.

Lean (version 4.22.0, arm64-apple-darwin23.6.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05, Release)