Lake update across lake versions

PatrickMassot commented 1 year ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Running lake update in an old project lead to errors because it tries to use and old version of lake to handle the modern lakefiles of dependencies.

Context

This happens if you run lake update in a project that depend on Mathlib and is old enough to not know about weakLeanArgs.

Steps to Reproduce

Create directory foo containing the lakefile

import Lake
open Lake DSL

package «foo» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Foo» {
  -- add any library configuration options here
}

and the lean-toolchain file containing leanprover/lean4:nightly-2023-06-20

run lake update

Expected behavior: [Clear and concise description of what you expect to happen]

I expect lake to clone a recent version of mathlib without any error message.

Actual behavior: [Clear and concise description of what actually happens]

Get messages:

cloning https://github.com/leanprover-community/mathlib4.git to lake-packages/mathlib
error: ./lake-packages/mathlib/lakefile.lean:31:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:55:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

Versions

Lean (version 4.0.0-nightly-2023-06-20, commit a44dd71ad62a, Release) on Ubuntu 22.04

I guess this cannot be fixed in old lake of course, but it would be nice to act now so that future lake won't break like this.

tydeu commented 1 year ago

I think this connects with leanprover/lean4#2752. Lake should check toolchain versions and compare with its own. If its toolchain is older than the packages it downloads it should error / warn cleanly about that.

tydeu commented 1 year ago

Reviewing this again, I noticed that the issue's expected behavior is for this to "just work" and my previous suggestion would still error (just in a different way). It is not clear to me how this could generally "just work". There are some major concerns:

Updating the Lean toolchain: If the Lake version is to old, we need update the toolchain, and as leanprover/lean4#2752 notes, there will not always be a good toolchain. Even in the context of mathlib it is possible for downstream projects to depend both on mathlib and some other project whose newest toolchains are incompatible (e.g., a project may want mathlib and LeanInfer and mathlib master may be on a newer toolchain than LeanInfer supports). In such a case, an error would be necessary as far as I can tell.
Update requires loading the configuration: When an updating a package, even with all needed static information contained in the manifest (which may itself produce errors with incompatible manifests), Lake still needs the dynamic information from the elaborated configuration. This is required to evaluate conditions for conditional dependencies like doc-gen4 and run update hooks like #2603 that may even be useful to mathlib. Since such things may effect dependency resolution, they also effect what toolchain is the best to update to. If the configuration is too new, it cannot be evaluated to further resolve dependencies and discover which is the toolchain is needed to fix the errors. One potential approach is to automatically bump the Lean toolchain and try again and then repeat this process for as many bumps as necessary. However, this still has the following problem.
Updating the Lean toolchain can break the root package: If Lake decides to auto-update itself to update upstream dependencies, this can into lead to a Lake that is too new to support the root package's current configuration. If this happens, then every other lake command will break until the updated toolchain is reverted (including all interactive editor features), which seems quite risky.

These problems make it seem very difficult to generally auto-resolve problems caused by incompatible Lake versions. That is why I suggested the above solution were Lake simply cleanly errors if the toolchain is incompatible. However, it is entirely possible I am simply being too pessimistic here and there is a nice solution that would work in most cases and could be recovered from in the edge cases, but I do not yet see it. Any suggestions on what should be done here technically?

digama0 commented 1 year ago

A simple solution to (1) is to have the user specify that they want to track the lean-toolchain of a dependency (like mathlib). If it errors then so be it, but this is a 90% solution that is clearly actionable by the user if anything goes wrong. (You can give a warning if you detect an incompatibility, but IIUC there isn't really any way to determine whether toolchains are "incompatible" without just trying it and seeing what works.)

tydeu commented 1 year ago

@digama0

A simple solution to (1) is to have the user specify that they want to track the lean-toolchain of a dependency (like mathlib). If it errors then so be it.

I agree that this is good solution assuming "if it errors then so be it" is acceptable.

One remaining technically difficult is restarting Lake from within Lake to continue with the update while preserving some of the configuration but not the toolchain. That is, once the first lake update updates the toolchain, it would need to start a second lake update on the toolchain to successfully elaborate the file and that lake update needs to be configured in approximately the same way minus the toolchain. This is doable, but can be quite finicky (just like the passing of arguments from lean --server to lean --worker can be finicky). This finickiness is one of the reasons I originally shied away from this kind of feature, but if it is in high demand it is likely worth it.

leanprover / lean4