VS Code lean server crash

Stream: lean4

[Martin Gilchrist]

Hi - am new to Lean so apologies if this is a dumb question. I am trying to us Visual Studio Code to write and run a Lean 4 sample file. However, the InfoView window reports that the Lean server crashes:

Lean (version 4.0.0-nightly-2022-05-08, commit 0fd47fd817eb, Release)
Lean (version 4.0.0-nightly-2022-05-08, commit 0fd47fd817eb, Release)
[Info - 9:21:18 AM] Connection to server got closed. Server will restart.
[Info - 9:21:24 AM] Connection to server got closed. Server will restart.
[Info - 9:21:30 AM] Connection to server got closed. Server will restart.
[Info - 9:21:35 AM] Connection to server got closed. Server will restart.
[Error - 9:21:41 AM] The Lean 4 server crashed 5 times in the last 3 minutes. The server will not be restarted. See the output for more information.
Error: Connection to server got closed. Server will not be restarted.

Here's info about my environment:

Windows 10
Visual Studio Code 1.67.1 (April 2022)
Lean version 4.0.0-nightly-2022-05-08
lean4 extension installed v0.0.72

Thanks in advance for any help! Martin

[Arthur Paulino]

Hello @Martin Gilchrist,
Can you post the code you're trying to run?

[Martin Gilchrist]

Hi - it's the example file Foo.lean when you run the lake init foo command. So the contents of the Foo.lean file are:
def hello := "world"

I'll include a screenshot to help give an idea of what I see.

image.png

[Martin Gilchrist]

I think that this is also relevant: the Windows Event Viewer reports an error:

Faulting application name: lake.exe, version: 0.0.0.0, time stamp: 0x62777050
Faulting module name: libleanshared.dll, version: 0.0.0.0, time stamp: 0x62777026
Exception code: 0xc0000005
Fault offset: 0x0000000000271fb1
Faulting process id: 0x31fc
Faulting application start time: 0x01d868dd8b4a5778
Faulting application path: C:\Users\martinpg\.elan\toolchains\leanprover--lean4---nightly\bin\lake.exe
Faulting module path: C:\Users\martinpg\.elan\toolchains\leanprover--lean4---nightly\bin\libleanshared.dll
Report Id: c8907e50-32a6-4f37-a803-f6a0ef7e774f
Faulting package full name:
Faulting package-relative application ID:

[Chris Lovett]

I just tried installing the leanprover--lean4---nightly on windows and it works fine, does your install directory look like this?

 Directory of C:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly\bin

05/16/2022  04:36 PM    <DIR>          .
05/16/2022  04:36 PM    <DIR>          ..
05/14/2022  12:13 AM           231,936 clang.exe
05/14/2022  12:35 AM         1,526,272 lake.exe
05/14/2022  12:13 AM         7,415,296 ld.lld.exe
05/14/2022  12:34 AM            77,312 lean.exe
05/14/2022  12:34 AM            97,280 leanc.exe
05/14/2022  12:11 AM               860 leanmake
05/14/2022  12:13 AM         1,274,880 libc++.dll
05/14/2022  12:13 AM        99,091,456 libclang-cpp.dll
05/14/2022  12:34 AM        51,060,736 libleanshared.dll
05/14/2022  12:13 AM        95,203,328 libLLVM-14.dll
05/14/2022  12:13 AM           103,936 libunwind.dll
05/14/2022  12:13 AM         7,415,296 lld.exe
05/14/2022  12:13 AM           167,424 llvm-ar.exe
05/14/2022  12:13 AM           105,984 zlib1.dll

and can you print out the following environment variables?

PROCESSOR_ARCHITECTURE=AMD64
PROCESSOR_IDENTIFIER=AMD64 Family 23 Model 113 Stepping 0, AuthenticAMD
PROCESSOR_LEVEL=23
PROCESSOR_REVISION=7100

[Martin Gilchrist]

Here is my install directory:
C:\Users\martinpg\.elan\toolchains\leanprover--lean4---nightly\bin>dir
Volume in drive C has no label.
Volume Serial Number is 184C-2440

Directory of C:\Users\martinpg\.elan\toolchains\leanprover--lean4---nightly\bin

05/08/2022 05:44 AM <DIR> .
05/08/2022 05:44 AM <DIR> ..
05/08/2022 12:08 AM 231,936 clang.exe
05/08/2022 12:25 AM 1,526,272 lake.exe
05/08/2022 12:08 AM 7,415,296 ld.lld.exe
05/08/2022 12:24 AM 77,312 lean.exe
05/08/2022 12:24 AM 97,280 leanc.exe
05/08/2022 12:06 AM 860 leanmake
05/08/2022 12:08 AM 1,274,880 libc++.dll
05/08/2022 12:08 AM 99,091,456 libclang-cpp.dll
05/08/2022 12:24 AM 51,346,432 libleanshared.dll
05/08/2022 12:08 AM 95,203,328 libLLVM-14.dll
05/08/2022 12:08 AM 103,936 libunwind.dll
05/08/2022 12:08 AM 7,415,296 lld.exe
05/08/2022 12:08 AM 167,424 llvm-ar.exe
05/08/2022 12:08 AM 105,984 zlib1.dll
14 File(s) 264,057,692 bytes
2 Dir(s) 705,302,437,888 bytes free

and here are my PROCESSOR environment variables:

PROCESSOR_ARCHITECTURE=AMD64
PROCESSOR_IDENTIFIER=Intel64 Family 6 Model 37 Stepping 2, GenuineIntel
PROCESSOR_LEVEL=6
PROCESSOR_REVISION=2502

[Kevin Buzzard]

You can use #backticks for code

[Chris Lovett]

@Martin Gilchrist can you try and wipe C:\Users\martinpg\.elan then restart VS code and follow the prompts as per https://leanprover.github.io/lean4/doc/quickstart.html and let me know what happens?

[Martin Gilchrist]

@Chris Lovett Thank you, I think that has fixed my problem. I now have a relatively simple project and Lean infoview window which is not complaining about server crashes! That said, I now cannot work out how to create a project that references mathlib4, but will try a different thread for that.

[Chris Lovett]

Something like this should work in your lakefile.lean:

import Lake
open Lake DSL

package MathTest {
  -- add configuration options here
  dependencies := #[
    {
      name := `mathlib
      src := Source.git "https://github.com/leanprover-community/mathlib4.git" "6895646674b04c0d7bcd085b4da3f7bb354ceaa9"
    }
  ]
}

Then your Main.lean can do some mathlib magic:

import Mathlib.Data.Nat.Gcd
#eval Nat.gcd 12 15 -- 3

[Brooks Bryant]

I've been using Lean for the past week and everything has worked fine, but now when I open VS code, I get the error :
Lake version 5.0.0-873ef2d (Lean version 4.8.0-rc2)

error: unspecified system_category error (error code: 193)

[Error - 2:59:29 PM] Server initialization failed.

Message: Pending response rejected since connection got disposed

Code: -32097

[Error - 2:59:29 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.

[Error - 2:59:29 PM] Lean 4 client: couldn't create connection to server.

Message: Pending response rejected since connection got disposed

Code: -32097

This is my setup information:
Operating system: Windows_NT (release: 10.0.22631)
CPU architecture: x64
CPU model: 8 x Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz
Available RAM: 8.46 GB

VS Code version: Reasonably up-to-date (version: 1.91.1)
Lean 4 extension version: 0.0.174
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.9.0)
Project: No open project

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------

leanprover/lean4:stable (default)

Lean (version 4.9.0, x86_64-w64-windows-gnu, commit 1b78cb4836cf, Release)

I tried uninstalling lean and installing it again and restarting my computer, but nothing has changed. Any help would be appreciated.

[Kevin Buzzard]

I don't know anything about windows but just to remark that you claim you're using 4.9 whereas the error mentions 4.8.0-rc2. In fact the version of lean you use depends on the project you're working on. What happens if you create a new project and try opening that in VS Code?

[Marc Huisinga]

The setup information shows that no project is currently open. Did you call it in a file that belongs to the project you are trying to work in?

[Brooks Bryant]

Just created a new project, got the same error. The setup info shows the project being open now:
Operating system: Windows_NT (release: 10.0.22631)
CPU architecture: x64
CPU model: 8 x Intel(R) Core(TM) i7-8550U CPU @ 1.80GHz
Available RAM: 8.46 GB

VS Code version: Reasonably up-to-date (version: 1.91.1)
Lean 4 extension version: 0.0.175
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.9.0)
Project: Valid Lean project (path: c:\Users\Brooks Bryant\lean_test\test)

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.8.0-rc2


active toolchain
----------------

leanprover/lean4:stable (overridden by '\\?\C:\Users\Brooks Bryant\lean_test\test\lean-toolchain')

Lean (version 4.9.0, x86_64-w64-windows-gnu, commit 1b78cb4836cf, Release)

error:
error: unspecified system_category error (error code: 193)

[Error - 11:58:49 AM] Server initialization failed.

Message: Pending response rejected since connection got disposed

Code: -32097

[Error - 11:58:49 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.

[Error - 11:58:49 AM] Lean 4 client: couldn't create connection to server.

Message: Pending response rejected since connection got disposed

Code: -32097

[Marc Huisinga]

Oh, there's a space in your Windows user name. I wonder if it's this issue again? https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Installation.20troubles/near/398093722 (cc: @Sebastian Ullrich )

[Brooks Bryant]

Could be, the problem is with my laptop, and my desktop (which doesn't have a space in the username) still works fine. Although it seems weird that it was perfectly fine with a space being there for a week before it decided to break.

[Sebastian Ullrich]

Just to be perfectly sure, does the path C:\Users\Brooks, i.e. up to the space, exist (now)?

[Brooks Bryant]

There's no folder there, although I just checked and there are these 4 files in C:\Users that were created July 20th when it stopped working:
Brooks
Brooks_000_vcRuntimeMinimum_x64.txt
Brooks_000_vcRuntimeMinimum_x86.txt
Brooks_001_vcRuntimeAdditional_x64.txt
Brooks_001_vcRuntimeAdditional_x86.txt
Seems like this has to be related to the problem, although I don't really know what the solution is.

[Brooks Bryant]

Yooo removing all those files fixed it! Thanks for the help!