Zulip Chat Archive

Lean (version 4.1.0, commit a832f398b80a, Release)
elan 3.0.0 (cdb40bff5 2023-09-08)
Watchdog error: unspecified system_category error (error code: 193)
[Error - 2:12:32 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Do you know what to do?

Shreyas Srinivas (Oct 18 2023 at 12:33):

Quick fix step 1 : close vscode. start it in the folder again. ping here if the error persists.

Shreyas Srinivas (Oct 18 2023 at 12:36):

alternatively if you are familiar with vscode commands, then open the command panel and execute the reload developer window command.

Alex J. Best (Oct 18 2023 at 13:33):

Also please give some more information about how you installed lean and what sort of file / project you were trying to open and what sort of machine you have

Dimitri Zvonkine (Oct 22 2023 at 21:21):

Thank you for your suggestions; unfortunately, so far the problem persists exactly as before. I have Windows 10 pro on a Dell computer, Latitude 5490. I installed Lean following the procedure on this page: https://leanprover-community.github.io/install/windows.html . After the problem arose I uninstalled elan and reinstalled it manually, added it and vscode to the list of allowed apps on the antivirus (Avast), installed Lean again in the command window:

C:\WINDOWS\system32>elan default stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.1.0
info: downloading component 'lean'
180.0 MiB / 180.0 MiB (100 %) 7.8 MiB/s ETA: 0 s
info: installing component 'lean'
info: default toolchain set to 'stable'

stable installed - Lean (version 4.1.0, commit a832f398b80a, Release)

I have also tried the quick fixes you suggested. But none of this changes anything. As soon as I open a new file in vscode it crushes within a second. I have not attempted to open any project, I just have a file that reads

lean4
#eval 1+2

And after a second I get the message

Lean (version 4.1.0, commit a832f398b80a, Release)
elan 3.0.0 (cdb40bff5 2023-09-08)
Watchdog error: unspecified system_category error (error code: 193)
[Error - 11:14:14 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Alex J. Best (Oct 22 2023 at 21:24):

why are you setting elan default while inside system32?

Alex J. Best (Oct 22 2023 at 21:25):

If you open a command prompt inside some ordinary folder and type lean -v what happens?

Dimitri Zvonkine (Oct 22 2023 at 21:28):

C:\Users\Dimitri Zvonkine>lean -v
Lean (version 4.1.0, commit a832f398b80a, Release)

Alex J. Best (Oct 22 2023 at 21:39):

ok so it looks like its installed ok, I'm just guessing but it could perhaps be something to do with the space in your username, could you try making a lean project (with lake new blah) in a directory whose full path doesn't have a space in, and then open that in vscode?

Dimitri Zvonkine (Oct 22 2023 at 21:47):

I've tried this in the Temp folder. I still get an error, but a new one:

[Error - 11:45:30 PM] Lean 4 client: couldn't create connection to server.
Message: Pending response rejected since connection got disposed
Code: -32097

Dimitri Zvonkine (Oct 22 2023 at 21:55):

But the error actually occurs even in a new file before it is saved. Also after I saved it on the Desktop.

Alex J. Best (Oct 22 2023 at 23:00):

What about if you save it inside some actual lean project (created with lake as above)?

Alex J. Best (Oct 22 2023 at 23:02):

To be clear I'd expect more issues with unsaved files and files saved in random folders than with a file inside an actual lean project where the folder was opened via vscodes "open folder" menu item

Dimitri Zvonkine (Oct 23 2023 at 00:42):

This is an attempt to open a folder created by lake with the "open folder" command, and with a path containing no spaces.

Lean (version 4.1.0, commit a832f398b80a, Release)
elan 3.0.0 (cdb40bff5 2023-09-08)
Watchdog error: unspecified system_category error (error code: 193)
[Error - 2:40:26 AM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Still more or less the same.

Sebastian Ullrich (Oct 23 2023 at 07:18):

The space in the home directory name is an interesting clue, but it might be that Lean itself needs to be moved to a space-free path if we want to test this hypothesis. Does running lake serve on the cmdline inside the space-free project directory already fail?

Mauricio Collares (Oct 23 2023 at 07:26):

Sebastian fixed Unicode support in v4.2.0-rc4. Is that relevant?

Dimitri Zvonkine (Oct 23 2023 at 10:55):

Yes, running lake serve inside a space-free project does fail. I will try to uninstall everything and re-install it inside the user "Public" instead of "Dimitri Zvonkine" and report the results.

Sebastian Ullrich (Oct 23 2023 at 11:37):

Thanks for your help! You shouldn't have to uninstall anything in the existing user for that, for what it's worth

Dimitri Zvonkine (Oct 23 2023 at 14:09):

In the end I undertook a rather bold move of changing the name of my user folder from "Dimitri Zvonkine" do "DimitriZvonkine" and editing the corresponding registers. And it solved the problem! So it was indeed the space that was causing the issue. Thanks a lot for your help!

(There doesn't seem to be an easy way to install lean in a different folder, except creating a new user. Both VScode and the elan installer choose the installation folder without asking me.)

Patrick Massot (Oct 23 2023 at 14:13):

We are really sorry about this mess. Hopefully someday Lean will support spaces in folder names.

Sebastian Ullrich (Oct 24 2023 at 21:20):

I just created a new Windows 10 user with a space in its name and Lean 4.1.0 worked without issues

Kevin Buzzard (Oct 24 2023 at 21:42):

And the "unicode character in userid" issue is also resolved too, right? This is great :-) Spaces in usernames are not that uncommon for maths undergrads using Windows, and unicode is also not uncommon for mainland Europeans.

Alex J. Best (Oct 24 2023 at 22:29):

Sebastian Ullrich said: