Open philderbeast opened 7 months ago
I was then able to link so I'm good to go but those error messages had me worried that things were messed up;
$ elan toolchain link lean4 build/release/stage1
$ elan toolchain link lean4-stage0 build/release/stage0
$ elan show
installed toolchains
--------------------
stable (default)
lean4
lean4-stage0
leanprover/lean4:stable
active toolchain
----------------
lean4 (overridden by '~/.../lean4/lean-toolchain')
Lean (version 4.6.0, commit 73b87f255824, Release)
$ lake --version
Lake version 5.0.0-src (Lean version 4.6.0, commit 73b87f2558245e3e867d95e1948f4fdeca2ffbf4)
$ lean --version
Lean (version 4.6.0, commit 73b87f255824, Release)
On first use of
elan
it is complaining about a nonexistant lean version it cannot download.I think I did a
make install
for lean4 maybe a month ago. I only installedelan
today. It had complained that I had an existing installation of lean in/usr/local/bin
so I deleted what lean things I had in/usr/local/bin
and then (possibly after using vscodeversion management|setup|install elan
) I installed elan from the command line with instructions for the development setup;I have these in my profile;