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