Lean Server stopping repeatedly

Stream: new members

[Anthony Peterson]

I am running Lean 4 in VSCode on Windows, and I'm getting "Lean Server has stopped unexpectedly" every few minutes.

Are there some basic steps I can do to see if there's something on my end that is the problem? I updated Lean 4 a month ago. Restarting VScode seems to help briefly, but then the Lean server continues to crash repeatedly.

[Mario Carneiro]

There should be some more diagnostic information, e.g. in the sidebar, or in the output panel (if there is a popup with the error it should include a button to take you to the output panel). Also it's possible that the code you are working on is related to the issue, so getting a #mwe example is helpful for replication.

Note that Lean moves fast and "I updated Lean 4 a month ago" means you are on an old version, so I recommend updating lean and see if the problem persists. But I don't think there is any recent issue that sounds like this one, so there's a good chance the current version also has the same problem, whatever it is.

[Anthony Peterson]

I am a Coq user learning Lean, I’ve been trying to copy some theorems over into lean. I may have messed a few up.

I will post an example if I run into it again.