Issue with toolchain for `lean4:v4.5.0-rc1`

Stream: general

[Paul Lezeau]

I've recently (for the past two days or so) been having issues with the toolchain for lean4:v4.5.0-rc1, which seems to fail to install on my laptop. For instance, today when opening a new copy of mathlib4 (via the download project option on VS code), I got the following error:

Cannot determine Lean version: selected elan default toolchain not installed - please set a new default toolchain.

When running elan show, I get this output:

installed toolchains
--------------------

nightly
leanprover-community/lean:3.50.3
leanprover-community/lean:3.51.1
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:stable
leanprover/lean4:v4.2.0-rc1
leanprover/lean4:v4.3.0
leanprover/lean4:v4.3.0-rc2
leanprover/lean4:v4.4.0-rc1
v4.5.0-rc1
4.5.0-rc1 (default)

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

leanprover/lean4:v4.5.0-rc1 (overridden by '\\?\C:\Users\paull\Desktop\temp\mathlib\lean-toolchain')
(toolchain not installed)

Would anyone know how to deal with this sort of issue?

[Yaël Dillies]

(note this has nothing to do with the cache outage)

[Mauricio Collares]

Running elan default stable should fix it. The problem is that the default toolchain is set to something invalid at the moment.

[Mauricio Collares]

What is your elan version, by the way? Maybe running elan self update is advisable, just in case

[Paul Lezeau]

Mauricio Collares said:

What is your elan version, by the way? Maybe running elan self update is advisable, just in case

Seems like my version is elan 3.0.0 (cdb40bff5 2023-09-08)

[Mauricio Collares]

Ah, sorry, my bad. I didn't realize you were opening a project. Did you or an antivirus delete part of your .elan folder? If so, you can completely delete it and it should download the required tool chains.

[Paul Lezeau]

No worries! I'll try to delete and see what happens!

[Paul Lezeau]

It's worth mentioning I had the exact same issue when working on the PFR project the other day

[Paul Lezeau]

@Mauricio Collares It seems like deleting the .elan folder fixed my issue, thanks a lot for your help!