Struggling to run Lean 3 and Lean 4 side by side in vscode

Stream: new members

[Richard Evans]

Hi, I installed vscode with extensions for Lean 3 and Lean 4. The Lean 4 extension works nicely, but I cannot get the Lean 3 extension to work.

It says:

> bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover-community/lean:3.20.0 || echo && read -n 1 -s -r -p "Install failed, press ENTER to continue..."' && exit
info: downloading installer
info: updating existing elan installation

Install failed, press ENTER to continue...

Does anybody know whether/how it is possible to have both versions of Lean running within VSCode? thanks in advance -

[Richard Evans]

Here is a screenshot of what happens when I open up a Lean3 file in vscode:

lean-error.png

(If I load a Lean4 file, everything works just fine).

[Richard Evans]

I have both lean and lean4 extensions installed.

Here is a screenshot of a Lean4 file working just fine:
lean-working.png

[Arthur Paulino]

Someone else might have a better solution, but I cherry pick the workspaces for which the extensions will be triggered by hand. For Lean 3, it's allowed to trigger on mathlib, only... And I keep the Lean 4 extension off there. And for everything else I let the Lean 4 extension trigger automatically and have the Lean 3 extension off by default (I work with Lean 4 mostly)

[Chris B]

It's definitely possible. What are your version numbers for vscode and the lean4 extension?

[Richard Evans]

For lean4, it is v0.0.71. For lean, it is v0.16.46. For VSCode, it is 1.66.2. (Running on Mac).

[Chris B]

That's the same setup I'm using; what's the output of elan toolchain list? When I have issues with elan, I usually just uninstall/reinstall (elan self uninstall).

[Richard Evans]

I get:

> elan toolchain list
leanprover-community/lean:3.20.0
leanprover/lean4:nightly (default)

and:

> elan show
installed toolchains
--------------------

leanprover-community/lean:3.20.0
leanprover/lean4:nightly (default)

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

leanprover/lean4:nightly (default)
Lean (version 4.0.0-nightly-2022-03-28, commit 4e008cf8b701, Release)

Is it significant that lean3 is not in the list of active toolchains?

[Mauricio Collares]

What happens if you execute elan show inside the logical_verification_2020 folder?

[Richard Evans]

Inside the logical_verification_2020 folder, I get:

> elan show
installed toolchains
--------------------

leanprover-community/lean:3.20.0
leanprover/lean4:nightly (default)

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

leanprover-community/lean:3.20.0 (overridden by '/Users/richardevans/Documents/research/work/projects/lean/logical_verification_2020/leanpkg.toml')
(error reading lean version)

[Mauricio Collares]

"error reading lean version" is suspicious. What is the error you get when running lean --version inside the LV2020 folder?

[Richard Evans]

> lean --version
dyld[2506]: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib
  Referenced from: /Users/richardevans/.elan/toolchains/leanprover-community--lean---3.20.0/bin/lean
  Reason: tried: '/Users/richardevans/.elan/toolchains/leanprover-community--lean---3.20.0/lib/libgmp.10.dylib' (no such file), '/usr/local/opt/gmp/lib/libgmp.10.dylib' (no such file), '/usr/local/lib/libgmp.10.dylib' (no such file), '/usr/lib/libgmp.10.dylib' (no such file)
Abort trap: 6

[Mauricio Collares]

Are you using a M1 Mac? If so, this part of the elan readme might be useful:

Lean 4 has native macOS/aarch64 releases (nightly only so far) that you can install as above by choosing the leanprover/lean4:nightly toolchain. For Lean 3, you need to run the installer under Rosetta (install using softwareupdate --install-rosetta if you haven't already done so) because there are no M1 releases for it right now:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | arch -x86_64 sh

[Richard Evans]

Thanks Mauricio. I will try that.

[Richard Evans]

Oh no hang on. It isn't an M1 mac - it is an intel.

[Mauricio Collares]

Ah, I see! The instructions on the lean-community website could be useful then: https://leanprover-community.github.io/install/macos.html#intel-macs. The script installs elan via brew, which probably installs dependencies such as gmp automatically.

[Mauricio Collares]

I am not a Mac user, so I'll have to let more experienced people help you if this fails

[Richard Evans]

Thanks! I will try this...

[Richard Evans]

Thanks for all your help everyone. It is working now :)