Install help needed

Stream: general

[Shuffle]

run "lake build" gets "error: toolchain 'leanprover/lean4:v4.9.0-rc1' is not installed", how to resolve it?

[Julian Berman]

What is type -a lake and how did you install elan?

[Shuffle]

image.png

[Shuffle]

Julian Berman 发言道：

What is type -a lake and how did you install elan?

and i should installed elan use the default vscode extension

[Shuffle]

image.png
I already have stable and 4.7.0 installed in .elan/toolchains

I am curious that we can install only two versions of lean? Or indeed more than two

[Julian Berman]

Shuffle said:

image.png
I already have stable and 4.7.0 installed in .elan/toolchains

I am curious that we can install only two versions of lean? Or indeed more than two

That's essentially the entire purpose of elan, yeah -- so something strange is happening.

[Julian Berman]

What does elan toolchain install 4.9.0-rc1 say?

[Shuffle]

image.png

[Shuffle]

image.png
Actually this works

[Julian Berman]

Yes, you left off the toolchain in the first one.

[Julian Berman]

And now does lake build work?

[Julian Berman]

Also what's elan --version?

[Shuffle]

elan --version is elan 3.1.1 (71ddc6633 2024-02-22), and lake build works now.

[Shuffle]

Thanks a lot. I am a bit confused by how elan works, just as you see i forget the toolchain, I cannot find detailed document for elan

[Julian Berman]

That looks right. I'm confused as to why your lake didn't install the toolchain automatically, as that's what the wrapper is meant for. Your PATH looks a bit screwy (as evidenced by seeing the same directory 10 times or whatever) but that shouldn't affect things.

[Julian Berman]

I actually don't know where longer docs for elan live either now that I think about it, if they do live somewhere. There seems to be no man page. Eventually it will live here: https://lean-lang.org/doc/reference/latest/Elan/#elan but the page is a TODO right now.

[Julian Berman]

elan --help will have at least basic information.

[Shuffle]

thanks a lot. I think they will have a document later, but for now let me just use the elan --help

[Julian Berman]

Most of the point is you really shouldn't have to interact with elan at all, so the "real problem" is if lake build is not automatically installing toolchains for you. If it happens again I think we try to figure out why.