RFC: lake update should update the lean-toolchain

[eric-wieser]

Current behavior

lake update updates all inherited: false dependencies, even if doing so would move to a newer toolchain.
It does not change the value in lean-toolchain, not does it emit any diagnostic to indicate that this might need doing manually.

This frequently bites users of projects which depend on mathlib, as lake update gives them a mathlib version that does not compile with (or at least, has no cache for) their active toolchain

Expected behavior

lake update should attempt to match the lean-toolchain of the new dependency versions. The design could be any of:

1. Look at all the versions of inherited: false dependencies. If there is just one entry in this set, use it. If there is more than one, prompt the user.
2. Look at all the versions of inherited: false dependencies. Attempt to pick the most recent of the options.
3. Add a tracks_toolchain key to the manifest, to indicate precisely which dependency the toolchain should be tracked from. For many users, this would be set to mathlib4.

[Shreyas4991]

About the second option, is it always true that a later toolchain can compile code written for an earlier toolchain?

[eric-wieser]

No, but nor is the reverse true, and if you run lake update you probably are more willing to risk moving forwards than backwards. Certainly a diagnostic is in order for any case except "If there is just one entry in this set".

[Shreyas4991]

Per the discussion on the thread, why can't this be implemented on the vscode extension as a behaviour specific to projects where mathlib is a non-inherited dependency and there are no others? Eventually lake would have some versioning for dependencies that makes this problem go away right?

[tydeu]

@Shreyas4991 Dependency versioning is very difficult in Lean. I think it will be a long while before we have something like semantic versioning. This RFC strikes me as potentially a pretty good general solution for the short term.

[Shreyas4991]

I agree with that. I am aware that dependency management is going to take a while. Which is why I was just wondering if this could be implemented as a vscode command called "update mathlib" as discussed in the thread. (Ref: the first message in the thread linked in my previous comment here). This is fundamentally a mathlib specific workflow request that can be accommodated in a vscode command. The gist of that thread is:

A GUI panel for lake commands is already planned. It is feasible to add mathlib specific options. The people most likely to be unable to solve the issue with lake update are also likely to be uncomfortable with CLIs. So GUI commands that perform safe default actions might be a shorter fix. It would also address in a limited way, the concerns of others that lake is doing many things, including very mathlib specific ones.

[eric-wieser]

This is fundamentally a mathlib specific workflow request that can be accommodated in a vscode command

I don't agree with this at all. The problem as described will affect anyone who depends on a package that changes lean version.

[Shreyas4991]

This is fundamentally a mathlib specific workflow request that can be accommodated in a vscode command

I don't agree with this at all. The problem as described will affect anyone who depends on a package that changes lean version.

Then this could be part of the update command on vscode.

My issue with the current RFC is that for any project with more than one non-inherited dependency (which we must not discount, just because it might be a fraction of current projects), it it not clear that it will work. As Mac points out, dependency management will take time. So, for however long this takes, we have no guarantees that such a project can be built with lake. Further, the 99% who do benefit from this are also likely to be mostly GUI users.

If this RFC is implemented, options 1 and 2 seem to be the best, but option 1 can confuse CLI-averse users with its options. Implementing 2 or 3 as a GUI command on vscode hides the scary CLI stuff for those who don't like CLIs. This is also a temporary fix, so eventually the GUI button can be withdrawn/modified.

EDIT: On second thoughts, if we do take the GUI route for option 2 or 3, then implementing option 1 in the lake CLI will be great for CLI users.

[tydeu]

@Shreyas4991

My issue with the current RFC is that for any project with more than one non-inherited dependency (which we must not discount, just because it might be a fraction of current projects), it it not clear that it will work.

My intended resolution to this RFC would be to check the lean-toolchain of each of the root dependencies and then the following:

• If there is only one distinct toolchain, update the workspace's. If it is clearly newer than the workspace's, print an info that this occurred; otherwise, print a warning.
• If there are multiple toolchains, find the maximum, up the workspace's toolchain with and print a warning.
• If Lake cannot produce a total ordering of the toolchains, do nothing and print a warning.
• Use a new tracks_toolchain require setting to filter which dependencies are checked. (Optional add-on)

However, it is worth nothing that none of these solutions will fix the case where lake update fails because Lake is too old. I am not sure what you and @eric-wieser think about that case.

[Shreyas4991]

Overall, sounds good.
Two details:

If lake cannot produce a total ordering...

Is a total ordering necessary here? Isn't what we need a partial ordering with a least upper bound?

none of these solutions will fix the case where lake update fails because Lake is too old.

Could lake be decoupled from the toolchain and managed by elan? cargo version appears to be managed by rustup for example. Why is it currently bundled with the toolchain?

[tydeu]

@Shreyas4991

Could lake be decoupled from the toolchain and managed by elan? cargo version appears to be managed by rustup for example. Why is it currently bundled with the toolchain?

It is managed by elan, the toolchain version is how it is managed.

[Shreyas4991]

What I mean is whether we could decouple the two: Let elan manage lake separately from the rest of the toolchain.

[eric-wieser]

and print a warning.

I'm happy with this compromise as long as the warning includes all the lean-toolchain versions (and the packages that they come from) as part of the warning. It would be especially great if it could show the versions before and after the update).

[tydeu]

@Shreyas4991 We want Lake to be part of the toolchain, though. Otherwise, breaking changes would leave old Lake projects unbuildable.

[eric-wieser]

I am not sure what you and @eric-wieser think about that case.

I have no opinions on this case, as I have not seen it happen.

[tydeu]

@eric-wieser

the warning includes all the lean-toolchain versions (and the packages that they come from) as part of the warning. It would be especially great if it could show the versions before and after the update).

Why does it need this much information? If Lake has no clue, I doubt the user will either. In such a case, they will likely have do some manually checking across the packages for what changes were made and which one needs what. Or, if they just forgot to update their toolchain to specific version already in mind, a simple warning should be enough to make them remember.

[tydeu]

More specifically, I was thinking of a warning of the following form (if the dependencies are incomparable):

warning: could not construct an ordering of the dependencies' toolchains; they may be incompatible; you should check their documentation to figure out what toolchain is necessary to make them work together (if any exists)

[eric-wieser]

If Lake has no clue, I doubt the user will either.

Lake has easy access to information that the user doesn't; the version of the toolchains that the dependencies were using before they ran lake update. I would be happier with something more like:

warning: the direct dependencies have possibly-incompatible toolchains:
  mathlib          : lean-4.0.0 -> lean-4.1.0
  my_other_package : lean-4.0.0 -> lean-4.1.0-my-hacky-pr
The current package's toolchain has been updated as
  this_package     : lean-4.0.0 -> lean-4.1.0
which may be incompatible; you should check the documentation of the dependencies to figure out what toolchain is necessary to make them work together (if any exists).

where this tells the user "oh, I probably want to paste lean-4.1.0-my-hacky-pr into my lean-toolchain".

[tydeu]

@eric-wieser Fair enough. Minor note: in the situation for this warning, the workspace toolchain would not be updated.

[eric-wieser]

Minor note: in the situation for this warning, the workspace toolchain would not be updated.

Indeed; the template was intended as inspiration for all the other "print a warning" options in your list, some of which I believe do involve an update.

[semorrison]

I think this can now be closed in favour of leanprover-community/mathlib4#7846

[tydeu]

@semorrison That is just mathlib-specific. The goal for this issue is to provide a general solution toolchain updates as part of lake update.

[eric-wieser]

In particular, anyone using Std but not mathlib will still experience this issue

[Kha]

There are other situations where a lean-toolchain sync would be important as well, such as adding new dependencies to the lakefile. Should this issue be generalized or should this be tracked separately?

[semorrison]

Updating lean-toolchain from Lake is now on the critical path to moving Mathlib from a lakefile.lean to a lakefile.toml. The only obstacle remaining is Mathlib's post-update script. (We've removed the meta if for doc-gen4 already.)