nightly does not have binary lake

Stream: lean4

[Floris van Doorn]

On Windows, after updating mathlib to latest version, I get the following error.

Floris@MSI MINGW64 /d/projects/mathlib4 ((41e9d745...))
$ lake build
error: toolchain 'leanprover/lean4:nightly-2023-01-29' does not have the binary `C:\Users\Floris\.elan\toolchains\leanprover--lean4---nightly-2023-01-29\bin\lake.exe`

Is this temporary?

[Sebastian Ullrich]

Broken download? Try deleting and reinstalling the toolchain.

[Floris van Doorn]

I deleted the folder. It didn't seem to contain much (no lake or lean). How do I reinstall the toolchain?

Floris@MSI MINGW64 /d/projects/mathlib4 (port/Data.Finset.Pointwise)
$ ls /c/Users/Floris/.elan/toolchains/leanprover--lean4---nightly-2023-01-29/bin -al
total 199728
drwxr-xr-x 1 Floris 197121        0 Jan 30 12:19 ./
drwxr-xr-x 1 Floris 197121        0 Jan 30 12:19 ../
-rwxr-xr-x 1 Floris 197121 69604352 Jan 29 08:19 libclang-cpp.dll*
-rwxr-xr-x 1 Floris 197121 61553664 Jan 29 08:49 libleanshared.dll*
-rwxr-xr-x 1 Floris 197121 73348608 Jan 29 08:19 libLLVM-15.dll*

[Jannis Limperg]

Remove the entire toolchain folder and the corresponding folder in .elan/update-hashes. (This is how it works on Linux at least.)

[Floris van Doorn]

Ok, it probably was a broken download. After downloading the toolchain folder and the folder in .elan/update-hashes everything is working normally.

[Floris van Doorn]

Ideally there would be a lake command that forces a redownload of the current toolchain. But it's good to know the current method of deleting two folders.

[Arthur Paulino]

Maybe a elan command

[Sebastian Ullrich]

Ideally elan would detect the broken download! I'm actually surprised the HTTP library doesn't do that for us

[Arthur Paulino]

I don't understand much about HTTP but I would implement the failure detection with a hash match check. And I wouldn't be surprised if servers didn't compute hashes by default. But that's something that can be done by hand

[Kevin Buzzard]

Just to remark that "delete the directory and the corresponding file in .elan/update-hashes" is also the solution to "I accidentally edited a file in core Lean and now I am in orange bar hell" which I give to UGs, once they've told me that re-downloading mathlib caches did not solve the problem. There is this rumour that core lean (3) should be read-only if installed by tooling but apparently this only works for a proper subset of the standard OSs.

[Sebastian Ullrich]

That is correct, @Johan Commelin implemented it for Linux and macOS. In any case, core is never recompiled in Lean 4.

[Kevin Buzzard]

I think what was happening in lean 3 was that students were right clicking on a thing in a file (e.g. a mathlib file), being transported to core Lean and then accidentally pressing the space bar or whatever. I have not had any experience with teaching lean 4 yet (I'm starting in October) so I don't know if this is still a possibility and whether it still has such catastrophic consequences.

[Arthur Paulino]

I've (intentionally) tried to change something in core Lean 4 once just to see what would happen. No rebuild was triggered :+1:

[Gabriel Ebner]

Ideally elan would detect the broken download!

I think there's two other failure modes where you end up with a broken toolchain:

• If you press ctrl-c while downloading, and
• when more than one elan is started at the same time (e.g. if you open and editor and run lake exe cache get without waiting)