elan now expects lake?

Stream: lean4

[Scott Morrison]

I'm getting errors from elan, saying:

error: toolchain 'leanprover/lean4:nightly-2021-10-12' does not have the binary `/home/lean/.elan/toolchains/leanprover--lean4---nightly-2021-10-12/bin/lake`

Presumably this means that elan is now expecting binaries to contain lake, but this hasn't quite happened yet?

[Scott Morrison]

@Mac, do you know the status here?

[Scott Morrison]

Ah, I see, this is presumably elan getting ahead of the PR that adds lake to lean4 https://github.com/leanprover/lean4/pull/683, and once that has merged then elan will work with all subsequent nightlies.

[Mac]

I guess one should not update to elan 1.1.0 until then

[Scott Morrison]

Sometimes it's hard to avoid updating -- e.g. even if you run an old elan-init.sh, it obtains v1.1.0. :-( It's okay, I can wait on this.

[Mac]

It might be a good idea for elan to only produce a warning rather than error if a nightly is missing lake

[Mac]

(especially as that may be required to support downloading older nightlies/versions)

[Scott Morrison]

Exactly. I'm stuck on this with mathport today. (Trying to make a reproducible build of mathport, but it's hard because I can't download a fresh copy of elan. :-)

[Mac]

@Scott Morrison you should be able to just grab the release for your OS of an older elan from the releases page and use that

[Mac]

which is probably a better idea than using the master elan-init.sh for a reproducible build (e.g., a docker container) as it fixes the version of elan being used

[Sebastian Ullrich]

@Scott Morrison I assume you have a locally built lake in your PATH. Putting that ahead of elan/bin should fix this error.

[Mac]

@Sebastian Ullrich fair enough, but I imagine we still want elan to regain support for downloading older nightlies without a Lake executable, correct? Or does the error not actually prevent the successful download/install of a toolchain lacking Lake?

[Sebastian Ullrich]

It shouldn't. Lean 3 doesn't have leanc either after all.