(VS Code) Pending response rejected error

Stream: lean4

[Thomas Murrills]

Often when working with lean4 PR releases in VS code in mathlib4 I get into a state where every time I try to restart Lean, it immediately stops unexpectedly, and I get an error notification saying

Pending response rejected since connection got disposed

What's strange is that this seems to persist across VS code reboots, even when I've run killall lean and killall lake in between. I'm not exactly sure what circumstances cause it; I've noticed it while looking at the lakefile, and when restarting the server after the lean version has changed (possibly while a file is building? I'm not sure). It happens, perhaps unsurprisingly, after lake update (which I need to run).

Has anyone else encountered this? (Fwiw, I'm on macOS.)

[Kalle Kytölä]

I encountered this now (on Linux Mint 21.1) on a project depending on Mathlib.

I tried exactly the same: close VS Code, killall lean, killall lake, restart --- still crashes.

[Kalle Kytölä]

Oh, I did lake clean and my whole folder was erased! (Absolutely everything, including subfolders and hidden files.)

[Kalle Kytölä]

I had noticed a discussion/warning about such a possibility, but I (think I) had followed the advice on deleting lakefile.olean and had updated to rc4.