Trouble in VS Code

Stream: lean4

[Chris Mascioli]

I just installed lean (via WSL) and have it working in terminal, but after installing the Lean package in VS Code I'm getting "Unable to start the lean server process: Error: spawn lean ENOENT --- The lean.executablePath "lean" may be incorrect, make sure it is a valid lean executab;e

I've added "C:\Users\Chris\.elan\bin\lean" (the response to which lean in git bash) to my system path

[Chris Mascioli]

I also made WSL the default profile and lean works inside the terminal in VSCode

[Chris Mascioli]

Resolved, installed 'lean4' instead of 'lean' as the VSCode extension

[Kevin Buzzard]

Three times this month I have seen students with ENOENT errors in VS Code when trying to use Lean 3 projects. One just sent me a screenshot:
ENOENT.png
Right now the solution seems to be "random fiddling and hope that the error goes away" and sometimes it does. This is when attempting to run Lean 3 projects, sometimes on systems which seem to otherwise work fine (lean -v works fine from the command line etc). Can anyone guess a potential diagnosis? The executable is just lean for the problems I've seen.

[Chris Lovett]

I think with the lean3 extension you have to have your PATH setup right, whereas the lean4 extension does not require that. The lean4 extension looks in the default elan install location and if it finds lean there then it uses it without you having to mess with your PATH. So perhaps the lean3 extension could do something similar...

[Kevin Buzzard]

Everyone I've talked to has said that the problem has gone away after a reboot btw

[Julian Berman]

Any commonalities in operating system for them?

[Julian Berman]

Not sure it's what's happening, but perhaps worth mentioning ENOENT can lie a bit -- it means "the executable isn't found", but if lean indeed exists, you can also get ENOENT (at least on macos) if e.g. the cwd that is being used to execute the process itself doesn't exist.

[Julian Berman]

https://github.com/leanprover/vscode-lean/blob/79c91c31f3a33cfb205380f45ebba9d6954d8a31/src/server.ts#L107-L109 it looks like is where that message gets raised.. which I think is saying the original error message is also present there unchanged, so that's.. not helpful to diagnose it seems.