Lake update behaviour

Stream: mathlib4

[Shreyas Srinivas]

The following happened today:

1. I have a (verification) project that depends on mathlib4.
2. I run lake update inside the project directory.
3. lake downloads new versions of mathlib, Qq, Aesop, and Std.
4. The lean-toolchain files of these deps are last week's nightly.
5. But the lean-toolchain of the project itself remained unchanged. I manually updated lean-toolchain
6. I performed lake exe cache get! followed by lake build, which worked

The question is about step 5. This issue has come up before, but does this behaviour of lake update make sense? Wouldn't it be better if lake update also copy pasted the toolchain and downloaded it, along with the dependencies?

[Sebastian Ullrich]

Shreyas Srinivas said:

4. The lean-toolchain files of these deps are last week's nightly.

If only it was that simple:

$ rg . **/lean-toolchain
lean-toolchain
1:leanprover/lean4:nightly-2023-05-06

lake-packages/std/lean-toolchain
1:leanprover/lean4:nightly-2023-04-20

lake-packages/aesop/lean-toolchain
1:leanprover/lean4:nightly-2023-04-11

lake-packages/Qq/lean-toolchain
1:leanprover/lean4:nightly-2023-03-17

What should happen now? Should Lake ignore all but the toolchains of direct dependencies? What if there are multiple direct dependencies that disagree?

[Shreyas Srinivas]

That's a fair point. the toolchains of std and Qq are different for me too. So I tried switching to the toolchain of Std. Funnily enough after lake exe cache get!, lake build worked with no errors. But vscode did give me errors.

[Shreyas Srinivas]

So either mathlib has a stronger requirement or the latest of the four toolchains is needed. This is a bit confusing.

[Shreyas Srinivas]

or somehow the vscode extension behaves differently

[Shreyas Srinivas]

Either way, at least for mathlib projects, the successfully working heuristic seems to be "match lean-toolchain with mathlib's lean-toolchain"

[Shreyas Srinivas]

Perhaps we could have a lake update math subcommand?

[Adam Topaz]

Have we considered doing something similar to Haskell stack?

[Sebastian Ullrich]

One simple approach would be to add a Lakefile flag "keep toolchain in sync with this dependency" and have init math set this flag for mathlib4, i.e. a sticky opt-in

[Shreyas Srinivas]

Sebastian Ullrich said:

One simple approach would be to add a Lakefile flag "keep toolchain in sync with this dependency" and have init math set this flag for mathlib4, i.e. a sticky opt-in

This would be nice.

I am still curious why lake build worked as it did but the vscode extension threw errors.