Can't get lean4 working with VS Code.

Stream: lean4

[Wrenna Robson]

I have a working install of lean 3 on this machine, but I wanted to try out switching to lean4. I followed the instructions for installing lean 4 and activating it in my current directory, it appears to be able to run, but VS Code just says "Waiting for the Lean server to start..." and hangs there. This is on WSL in Windows 11.

Also: what is the best way to manage having active lean 3 and lean 4 projects? I don't seem to be able to use lake unless lean4 is activated in a directory: so how do I start a new lean 4 project if lean 3 is my default?

[Wrenna Robson]

(My understanding is that leanproject is only to be used with lean 3 and it's lake that should be used with lean 4?)

[Wrenna Robson]

OK so if I do elan default leanprover/lean4:stable, that works (wheras elan override set leanprover/lean4:stable did not).

[Wrenna Robson]

But then I need to do elean default stable if I want to switch back to Lean 3. So do they just not coexist well?

[Moritz Doll]

doesn't VSCode automatically find the correct Lean version for you? The VSCode extension should take care of everything. If I start in a Lean4 folder VSCode says "Lean 4" instead of "Lean" in the bottom right corner. On elan my default toolchain is leanprover-community/lean:stable

[Alex J. Best]

Do you have both the "lean" and "lean4" extensions installed in vscode?

[Alex J. Best]

In my experience they coexist fairly well, creating a new project is one point where it is a little bit tricky though, but normally its not something I do too often:
You can also use commands like

elan run leanprover-community/lean:3.45.0 leanpkg new blah
elan run leanprover/lean4:nightly lake new blah

rather than setting overrides if you want to make a new project for a specific version

[Wrenna Robson]

No, VS Code seems to get confused

[Kevin Buzzard]

Yeah I've been running lean 3 and lean 4 together on my laptop (Ubuntu 20.04) no problem, switching between various branches of mathlib in lean 3 and various branches of mathlib4 in lean 4 and it's working seamlessly for me

[Chris Lovett]

@Wrenna Robson this should be fixed by https://github.com/leanprover/vscode-lean4/pull/264