Error starting lean language client

Stream: lean4

[Martin Gilchrist]

Hi - I am learning Lean by following the Mathematics in Lean book tutorial. Unfortunately, I have run into a problem very early on! My basic environment is Windows 10 and Visual Studio Code 1.85 (see below for details). I have checked out the MathLib tutorial and clicked into S01_Getting_Started.lean. In the Lean Infoview, I can see the message Waiting for Lean server to start...

VS Code also displays Starting Lean language client, but this message never goes away. I selected the Manage Extension window, and under RUNTIME STATUS, I see this message (displayed twice): Header must provide a Content-Length property.

Does anyone know what the problem is, and how I can get past this problem? Thanks for any help, Martin

Version: 1.85.1 (system setup)
Commit: 0ee08df0cf4527e40edc9aa28f4b5bd38bbff2b2
Date: 2023-12-13T09:49:37.021Z
Electron: 25.9.7
ElectronBuildId: 25551756
Chromium: 114.0.5735.289
Node.js: 18.15.0
V8: 11.4.183.29-electron.0
OS: Windows_NT x64 10.0.19045

[Patrick Massot]

Are you sure you opened the correct folder in VSCode? Could you share a screenshot of your VSCode with the file explorer panel opened?

[Martin Gilchrist]

Hi, here's a screenshot:
image.png

[Patrick Massot]

It looks like you opened the correct folder. So there is really something uncommon going on.

[Eric Wieser]

This could be overzealous antivirus being a lossy MitM

[Martin Gilchrist]

Hi - I have disabled all anti-virus protection and network protection (that I know of) on this machine, and still see the same problem. I wouldn't claim to know either VS Code or Lean well, but do you which log files I should be looking at next to see if there is a more useful error message? Do you think that this is likely to be a VS Code problem or a Lean problem?

[Scott Morrison]

We may need to summon @Marc Huisinga here, as the principal VSCode extension expert! :-)

[Marc Huisinga]

@Martin Gilchrist When encountering this error, could you click on the ∀ button in the top right and then "Troubleshooting: Show Output"?

[Martin Gilchrist]

Hi, here's what I see when I show output:

lean +leanprover/lean4:stable --version
Lean (version 4.0.0-nightly-2022-06-09, commit d0499ebf4d92, Release)

d:\mathematics\mathematics_in_lean> lean +leanprover/lean4:v4.4.0-rc1 --version
Lean (version 4.0.0-nightly-2022-06-09, commit d0499ebf4d92, Release)

error: package configuration .\lakefile.lean has errors

I have attached the lakefile.lean file that is in the mathematics_in_lean directory.
lakefile.lean

[Marc Huisinga]

That Lean version looks very old. If you run elan show in the MiL directory, what does that yield?

[Martin Gilchrist]

Here's the output:

D:\mathematics\mathematics_in_lean>elan show
info: downloading component 'lean'
183.5 MiB / 183.5 MiB (100 %) 44.0 MiB/s ETA: 0 s
info: installing component 'lean'
installed toolchains

---

leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2022-04-16

active toolchain

---

leanprover/lean4:v4.4.0-rc1 (overridden by '\\?\D:\mathematics\mathematics_in_lean\lean-toolchain')
Lean (version 4.4.0-rc1, commit b0fe9d6cdca8, Release)

[Shreyas Srinivas]

You could try this : Run elan default leanprover/lean4:v4.4.0-rc1. Once that is done, try running cloning a fresh copy of the MIL repository and opening it.

[Marc Huisinga]

elan self update on top of that may also be a good idea.

[Martin Gilchrist]

Hi, I did all of the above, but still see the same problem (here's the output from elan show in the new directory):

D:\mathematics\mathematics_in_lean_2\mathematics_in_lean>elan show
installed toolchains

---

leanprover/lean4:nightly
leanprover/lean4:nightly-2022-04-16
leanprover/lean4:stable
leanprover/lean4:v4.4.0-rc1 (default)

active toolchain

---

leanprover/lean4:v4.4.0-rc1 (overridden by '\\?\D:\mathematics\mathematics_in_lean_2\mathematics_in_lean\lean-toolchain')
Lean (version 4.4.0-rc1, commit b0fe9d6cdca8, Release)

[Martin Gilchrist]

I think the problem must be either in my installation of Lean or how VS Code is configured to use Lean. Any ideas how I could force a complete re-install of Lean and/or VS Code's configuration?

[Marc Huisinga]

One thing you can try to reset the VS Code configuration is to open File > Preferences > Settings and then click the small "Open settings" button in the top right (see the attached picture). Are there any settings in that file prefixed with lean4? If so, you could delete them, save the file and restart VS Code.

image.png

[Martin Gilchrist]

Hi - there were only two settings relating to lean4 (see screenshot). I have removed both of them and restarted VS Code.
image.png

Unfortunately, still the same problem.

I guess my basic question is this: how can I completely clean this machine so that I have only the most up-to-date version of elan/lean installed, and know that VS Code is configured to use these? Is 4.4.0-rc1 the most up-to-date version or is there a higher version that I should be using?

[Marc Huisinga]

1. You can uninstall Lean entirely using elan self uninstall (this should also remove all toolchains, but you can double-check whether there is still a .elan folder after running the command in your Windows home directory).
2. Removing the Lean 4 extension isn't as easy because VS Code caches it, but since there is no state except for the config and you've already checked that there are no problematic config entries, it shouldn't be necessary to reinstall it. Make sure to close all VS Code windows and restart VS Code, though.
3. You can then reinstall Lean by following the quickstart guide.
4. In the setup guide in VS Code that you open as part of the quickstart guide, there is a button to download an existing project, see the attached image. You can click it, paste the MiL link, select a directory and the extension should do the rest. Lean's version manager Elan should automatically download the correct Lean version for MiL and use it.

image.png

I am still really confused about what is going on in your setup, though. It looks like your VS Code is using an old Lean version in VS Code, but not when you are using the terminal. The only way that can happen that I know of is if someone sets the Lean 4 extension Lean version override setting, which clearly you haven't set.

[Mauricio Collares]

Martin, did you experiment with Lean 4 a long time ago? I'm asking because very old versions of the Lean 4 VS Code extension exposed different override options, and maybe they got saved somewhere on your computer.

[Martin Gilchrist]

Hi, Marc - thanks for help and patience. I will do this. In the meantime, if I complete this and re-install everything, what version of elan/lean should I see?
Hi, Maurico - yes, I I first tried out Lean4 about a year or so ago, but ran into difficulties then so I put this to one side. There may even be a thread on Zulip which I started back then!

[Marc Huisinga]

When you re-install Elan, it will automatically install the most recent stable version for you. Note that this is only the Lean version that Elan uses when you are not in a project directory, and within project directories, it will use the correct version of that project that is specified in the lean-toolchain file of that project (for MiL, this is v4.4.0-rc1).

[Martin Gilchrist]

Hi - am having a problem running the uninstall command (running in a console window as Administrator):

D:\mathematics\mathematics_in_lean_2\mathematics_in_lean>c:\Users\martinpg\.elan\bin\elan self uninstall

This will uninstall all Lean toolchains and data, and remove
%USERPROFILE%\.elan/bin from your PATH environment variable.

Continue? (y/N) y

info: removing elan home
error: could not remove 'elan_home' directory: 'C:\Users\martinpg\.elan\toolchains'
info: caused by: Access is denied. (os error 5)

I think that this is my problem so will try to get this resolved before bothering you again!

[Kim Morrison]

It should be safe to just delete .elan by any means necessary, if you are planning on reinstalling.

[Martin Gilchrist]

@Scott Morrison Yes, that's effectively what I did. I think things are working now, but the MIL modules are taking a long time to build... Definite progress though!
image.png

[Kim Morrison]

Ah -- you shouldn't have to build that stuff locally!

[Kim Morrison]

Run lake exe cache get in the MIL directory.

[Kim Morrison]

Alternatively in VSCode click the forall icon in the top right, select "Project actions" then "Fetch mathlib build cache".

[Kim Morrison]

Hopefully this step is documented in whatever instructions you are following, but after your unexpected difficulties it's not surprising you missed it! :-)

[Martin Gilchrist]

@Scott Morrison Hi - I tried to run lake exec cache get a couple of days ago, but got an error. At the time, I put it to one side because of the problems above, but once the local building has finished, I'll try to run it and see if the error is also fixed by updating my elan/lean environment.

[Kim Morrison]

I'd encourage you to just cancel the local build. It should never be necessary, and lake exe cache get is always the preferred option.

[Martin Gilchrist]

@Scott Morrison Thanks - will try that next.

I just wanted to add a big thank you to Eric, Patrick, Marc, Mauricio, Scott, and Shreyas for your help and patience. It has been a very positive experience getting help so quickly!

[Moti Ben-Ari]

(deleted)

[Thomas Browning]

I seem to have a similar issue. I cloned MIL, and am stuck with "starting lean language client", even after uninstalling and reinstalling elan.
The terminal output is:

c:\Users\thoma\Documents\lean\mathematics_in_lean_source> lean --version
Lean (version 4.10.0-rc2, x86_64-w64-windows-gnu, commit 702c31b80712, Release)
c:\Users\thoma\Documents\lean\mathematics_in_lean_source> lake --version
Lake version 5.0.0-702c31b (Lean version 4.10.0-rc2)

elan show gives

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

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

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

leanprover/lean4:v4.10.0-rc2 (overridden by '\\?\C:\Users\thoma\Documents\lean\mathematics_in_lean_source\lean-toolchain')
Lean (version 4.10.0-rc2, x86_64-w64-windows-gnu, commit 702c31b80712, Release)

Any suggestions?
image.png

[Thomas Browning]

Actually, disregard, things have started moving again (although with errors)