lake update: invalid toolchain name

Stream: mathlib4

[David Renshaw]

when I try to update my project to use mathlib more recent than mathlib4#7747, I get this error:

$ lake update
mathlib: updating repository './lake-packages/mathlib' to revision 'ace6e09154439335a48190750134bb5bb5656007'
mathlib: running post-update hooks
error: invalid toolchain name: 'leanprover/lean4:v4.3.0-rc1
'
error: mathlib: failed to fetch cache

[David Renshaw]

That pull request added a newline to mathlib's lean-toolchain, so I thought that maybe updating my project's lean-toolchain to have a matching newline would help. It did not.

[David Renshaw]

Actually, it seems that lake update is modifying my lean-toolchain file to ensure that it always has a newline at the end.

[David Renshaw]

Ah, looks like I can still manually do lake exe cache get and everything works.

[Joachim Breitner]

David Renshaw said:

Actually, it seems that lake update is modifying my lean-toolchain file to ensure that it always has a newline at the end.

I think it’s just copying it from mathlib, with or without newline?

On mathlib, “feat(FieldTheory.AbsoluteGaloisGroup): add the absolute Galois group and its topological abelianization (#7783)” removed the newline and “perf(AlgebraicGeometry): Fix slow and bad proofs (#7747)” added it again :-D

[Patrick Massot]

It would be really nice to fix this issue because students are confused about it.

[David Renshaw]

@Mac Malone do you have any ideas why we're getting this "invalid toolchain name" error?

[Mac Malone]

The problem here is that the post update hook I added does not trim the toolchain when passed to Elan (as this was previously unnecessary), so Elan is getting a toolchain with a newline at the end. Fixing this just requires a mathlibToolchain.trim, though it might also be a good idea to change the Elan command to just "elan" to additionally fix a different post-update hook error mentioned in another Zulip thread.

[Kaiyu Yang]

I'm having the same issue.

[Scott Morrison]

#8401

I haven't done any testing --- if someone affected by this issue could try it out that would be great.

[Joachim Breitner]

as this was previously unnecessary

I’m curious, did elan change, and really support

elan "leanprover/lean:stable "

before, or was it previously not necessary for other reasons (e.g. because it was invoked in a shell like elan $(cat lean-toolchain), where the shell would trim the arguments.)

[Sebastian Ullrich]

It was previously invoked as lean :) . When elan reads the toolchain from the file itself, it does trim the string. There is no regression in elan.

[Sebastian Ullrich]

Actually, I don't understand why we're not just calling lake here. The toolchain file has already been updated.

[Eric Wieser]

Presumably calling lake fails if the "lake path" or "toolchain" setting is overridden in vscode?

[Mauricio Collares]

But if the toolchain is overridden, the lake call "succeeds" and overwrites the current oleans in build/ with ones incompatible with the override, which is what @Joachim Breitner was complaining about earlier.

[Mauricio Collares]

Lean.versionString is part of the cache hash, so calling lake exe cache get with an overridden toolchain would result in a full cache miss, which I think is more desirable (assuming they would get rejected by Lake later on).

[Mac Malone]

Sebastian Ullrich said:

Actually, I don't understand why we're not just calling lake here. The toolchain file has already been updated.

Elan adds the old toolchain's bin directory to the front of PATH when calling the top-level lake. Thus, a bare "lake" will just pick up the old toolchain's Lake.

[Mac Malone]

Joachim Breitner said:

was it previously not necessary for other reasons

It was not necessary because mathlib'slean-toolchain did not previously have a newline. :wink:

[Sebastian Ullrich]

Mac Malone said:

Sebastian Ullrich said:

Actually, I don't understand why we're not just calling lake here. The toolchain file has already been updated.

Elan adds the old toolchain's bin directory to the front of PATH when calling the top-level lake. Thus, a bare "lake" will just pick up the old toolchain's Lake.

Yikes, this is a Windows workaround in rustup that was fixed only this year in https://github.com/rust-lang/rustup/pull/3178. But at least for the time being we're stuck with it.