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"?