lake update breaks lean-toolchain

Stream: lean4

[Floris van Doorn]

I cannot reproduce this on my own laptop, but there was some weird behavior @Melanie Matchett Wood experienced.
She worked on a project downsteam from Mathlib, and had a lean-toolchain that specified v4.20.0 and a lakefile.toml that pinned Mathlib to v4.20.0 (this last part was not intentional). Then, running lake update from the command line cause the lean-toolchain file to somehow get updated to 4.24.0-rc1, which then broke Cache.
Any ideas what could have gone wrong here?

[Floris van Doorn]

I just realized another very important extra piece of information: lakefile.toml also specified a doc-gen dependency with revision main hardcoded. Whose responsibility is it to raise an error that there is a Lean version mismatch in the dependencies? I expect it is the responsibility of lake update, right? I don't think such an error was raised.

[Notification Bot]

This topic was moved here from #mathlib4 > lake update breaks lean-toolchain by Floris van Doorn.

[Kim Morrison]

I'm pretty sure there is no such check (that the lean-toolchains of all dependencies agree), let alone a check that different paths through the dependency graph reach the same revision.

[Kim Morrison]

Note that it's pretty common to run on different toolchains: e.g. in testing Mathlib against nightly releases (or PR toolchain releases), it is essential to be able to use upstream libraries at older releases, rather than also bumping them.

[Jon Eugster]

It's the users responsibility to raise that error ;)

I thought only the mathlib post-update hook used to update the lean_toolchain by copying it from somewhere, not aware of any other mechanism. no, that's deprecated information

[Jon Eugster]

Apparently, the relevant function to look at is Lake.Workspace.updateToolchain. There the algorithm iterates over all toolchains of the (direct?) dependencies with the following test:

if depTc ≤ tc then
  return (src, tc, tcs)
else if tc < depTc then
  return (dep.name, depTc, tcs)
else
  return (src, tc, tcs.push (dep.name, depTc))

so concretely, it tries to find the newest toolchain to update to. Which would probably be the toolchain of doc-gen@main in your example.

I'm a bit surprised that this is the chosen behaviour, especially since in the next line of code it looks like there is already the setup to warn users when they have (direct?) dependencies with mismatching toolchains:

if 0 < tcs.size then
    let s := "toolchain not updated; multiple toolchain candidates:"

I think you can avoid the automatic toolchain bump with lake --keep-toolchain update.

[Jon Eugster]

(I guess there is a slight conflict of interest, from lake's perspective it makes sense to update to the newest version if possible and not prioritise any dependencies. It's unfortunate that in praxis a lot of users would want to follow mathlib's version no matter what because mathlib is their largest dependency and most likely to break with the wrong toolchain)

[Floris van Doorn]

Jon Eugster said:

It's the users responsibility to raise that error ;)

I think it would be good if lake update raises a warning when it finds that different dependencies have a hard-coded a version that uses a different Lean version.
In this case, we had a Lean beginner that used someone else's setup which was workable 4 months ago, but now the meaning of "stable" has changed. Nothing pointed the beginner to the fact that there might be something wrong in lakefile.toml (and even as the expert it took a few tries before considering a problem in lakefile.toml).

[Jon Eugster]

I completely agree:+1:

(If that didn't come across, with this comment I meant to hint at my impression that lake is quite fiddly to get set up correctly, and I would love to have better warnings and less possibilities to end up in a bad state by running the wrong commands in the wrong order. But I do apprechiate that package managing a complex task with many possibilities and quite hard to get completely right)

[Mac Malone]

Floris van Doorn said:

I think it would be good if lake update raises a warning when it finds that different dependencies have a hard-coded a version that uses a different Lean version.

It is not quite clear to me what you are suggesting Lake should do here. Lake currently does log the fact that it updates the toolchain. Are you suggesting that Lake should promote this to a warning whenever there are dependencies with different Lean toolchains? As Kim noted, it is very common for a package to have dependencies at different toolchains (as many packages bump toolchains infrequnetly as they may not break every release), and the goal is usually to build them all on the most up-to-date toolchain. Making this a warning seems quite odd when that is the usually desired behavior.

I am also not sure what you mean by "hard-coded a version". All dependencies are pinned to some version. I presume you don't mean a specific commit hash / tag, as your example was using "stable" and "main". Even when pinned to a specific hash / tag, it is not clear that indicates incompatibilty across toolcahins. The tag can represent a specific package version, not a toolchain version, after all.

[Mac Malone]

On the flip side, one way to improve the UX here could be to add a configuration optiona that allows Mathlib to specify it only works on a specific toolchain. That way Lake could know that it should produce an error if it wants to move to newer toolchain for another dependency.

[Eric Wieser]

Isn't the new intended way to use doc-gen not to put it in the main lakefile?

[Floris van Doorn]

Mac Malone said:

Floris van Doorn said:

I think it would be good if lake update raises a warning when it finds that different dependencies have a hard-coded a version that uses a different Lean version.

It is not quite clear to me what you are suggesting Lake should do here. Lake currently does log the fact that it updates the toolchain. Are you suggesting that Lake should promote this to a warning whenever there are dependencies with different Lean toolchains? As Kim noted, it is very common for a package to have dependencies at different toolchains (as many packages bump toolchains infrequnetly as they may not break every release), and the goal is usually to build them all on the most up-to-date toolchain. Making this a warning seems quite odd when that is the usually desired behavior.

I am also not sure what you mean by "hard-coded a version". All dependencies are pinned to some version. I presume you don't mean a specific commit hash / tag, as your example was using "stable" and "main". Even when pinned to a specific hash / tag, it is not clear that indicates incompatibilty across toolcahins. The tag can represent a specific package version, not a toolchain version, after all.

With "hardcoded a version" I mean something like rev = v4.20.0 in the lakefile.toml.
I can assure you that if the Lean version of your project is any different than the Lean version of your Mathlib dependency, then that is almost never the desired behavior, will almost always lead to errors, and these errors will confuse both beginners and experts.
I respect that in other cases this is desirable, and I don't know the best solution. Maybe lake can hardcode a check like this for Mathlib (and anything that depends on Mathlib)?

[TyDHC]

Maybe you can try specify the lean version in the "lakefile.toml" and "lean-toolchain", like this

1. lakefile.toml

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.23.0"

2. lean-toolchain

leanprover/lean4:v4.23.0