toolchain leanprover/lean4:v4.7.0-rc2

Stream: lean4

[Antoine Chambert-Loir]

I just cloned a fresh mathlib, it requests leanprover/lean4:v4.7.0-rc2 as a toolchain, but when I try to install it, using

elan toolchain install leanprover/lean4:v4.7.0-rc2

I get an error message that this toolchain is unchanged (toolchain not installed).
On the other hand, I could install v4.7.0-rc2.

What did I do wrong?

[Antoine Chambert-Loir]

(Meanwhile, I renamed the directory ~/.elan/toolchains/v4.7.0-rc2, and that seems to work.)

[Kevin Buzzard]

If you clone a fresh mathlib with git clone and then type lake exe cache get in the directory which just appeared then everything should just get installed automatically. In particular you should not need to know or care which version of lean it's using. Is this not what happened to you?

[Kevin Buzzard]

I would be very cautious about manually doing anything inside the .elan directory

[Antoine Chambert-Loir]

Apparently not… I could try again to see if this works better.

[Kevin Buzzard]

You might want to remove the directory in .elan which you created before you do anything else

[Kevin Buzzard]

Although you might already have broken .elan (every toolchain is tied to several directories and files in other places all of which are coordinated internally and which the user shouldn't need to touch). You just moving one directory might have broken various assumptions that elan makes

[Kevin Buzzard]

You might want to browse through the entire elan directory to see if there are any other files or directories that you might want to consider renaming, now you have renamed one thing

[Kevin Buzzard]

For example, if you want to uninstall a toolchain and you do it by deleting the directory (only) (eg by renaming it), this is a disaster, because now it is actually only partially installed and it is no longer possible to either fully install or uninstall it using elan