Lean 4 setup help

Stream: mathlib4

[Michael Stoll]

Not sure that this is the right place for this question, but:
I'm trying to get Lean 4 installed and running, following the instructions here. I installed the Lean 4 extension in VSCode and opened a new file and selected lean4 as language. Then I copied the sample contents import Lean / #eval Lean.versionString into the file, but I'm stuck at "Waiting for Lean server to start...". Reloading the window didn't help.
In the ~/.elan/toolchains directory, there is now a new subfolder leanprover--lean4---nightly/.
When I try to set up a project via lake init test, I get an error

error: toolchain 'stable' does not have the binary `/home/mstoll/.elan/toolchains/stable/bin/lake`

(the .../bin/lake/ directory contains lean, leanchecker and leanpkg).
How do I proceed?

[Michael Stoll]

There is a lake in .../toolchains/leanprover--lean4---nightly/bin/, though. So it seems to look in the wrong place.

[Eric Wieser]

I recommend making a new thread for lean4 setup help

[Michael Stoll]

Within "mathlib4" or "lean4"?

[Notification Bot]

4 messages were moved here from #mathlib4 > Forward porting #17483 by Michael Stoll.

[Michael Stoll]

Checking out mathlib4 seems to work, btw. (and results in another toolchain (lean4:nightly-2023-03-09) to be added).

[Michael Stoll]

Now when I try to set up a new project with Lean3, I run into the same problem. After leanproject new test, cd test, code . and opening a new file in VSCode, clicking on select a language and then entering Lean (and not Lean 4), saving the file to src/test.lean and entering import tactic, the info view is stuck at "Waiting for Lean server to start...". If I try to restart the Lean server, I get the error message Command 'Lean: Restart' resulted in an error (command 'lean.restartServer' not found).
This seems to indicate that it did try to start the Lean 4 language server instead of the Lean language server, but I don't know how to check or/and fix that.

[Michael Stoll]

The leanpkg.toml file has the line lean_version = "leanprover-community/lean:3.50.3", so that looks OK.

[Michael Stoll]

After disabling the Lean 4 extension, quitting VSCode and restarting it, it works again.
But I guess it should be possible to have both the Lean and the Lean4 extension enabled in parallel, and VSCode can figure out which one to use?

[Kevin Buzzard]

Yes I've got both enabled on this computer and it has no problems with VS Code opening a random lean project -- the system just magically decides if it's Lean 3 or Lean 4.