leanprover/lean4

`lake update` should print a warning, if moving dependencies to a later toolchain than the local toolchain

Opened this issue · 3 comments

semorrison commented

Recently a @BoltonBailey was trying to run lake update in their https://github.com/BoltonBailey/formal-snarks-project project (see commit 6159c012f69556d2adbc3207b5bcdb29e7a3e9e8 if you'd like to be able to reproduce).

They received the output:

$ lake update
mathlib: updating repository './.lake/packages/mathlib' to revision '294ff6a495e19ae5a32188033d6e487ca42aded5'
Qq: updating repository './.lake/packages/Qq' to revision '53156671405fbbd5402ed17a79bd129b961bd8d6'
aesop: updating repository './.lake/packages/aesop' to revision '2225b0e4a3528da20499e2304b521e0c4c2a4563'
proofwidgets: updating repository './.lake/packages/proofwidgets' to revision 'e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5'
Cli: updating repository './.lake/packages/Cli' to revision 'a11566029bd9ec4f68a65394e8c3ff1af74c1a29'
error: ./.lake/packages/aesop/lakefile.toml:1:0: error: unexpected identifier; expected command
error: ./.lake/packages/aesop/lakefile.toml: package configuration has errors

The underlying problem here is that the project was still on v4.4.0-rc1, and the upstream repository aesop has now moved to a lakefile.toml, which of course can't be understood by v4.4.0-rc1.

The underlying cause --- that in order for lake update to be successful, the user will need to update their lean-toolchain --- is completely invisible here, and unresolvable without coming to zulip to ask for help.

Going forward, how can lake help here? It seems that as soon as it has checked out each upstream repo (e.g. starting with Mathlib), lake can notice that it is on a later toolchain, and issue a warning.

The warning should explain that the dependency is on a later toolchain, and suggest one of three options:

  1. Update the lean-toolchain in the current project.
  2. Pin the dependency on a particular commit or sha (ideally, in this case, being clever enough to suggest pinning mathlib to v4.4.0-rc1, or even better there would be a way to say "I want mathlib at the tag corresponding to my toolchain", as we've seen users such as @joneugster doing in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/v4.2E8.2E0-rc1.20discussion/near/437228497).
  3. Add some way to say in the require statement: "look, I know this dependency is going to be on a later toolchain, I am an expert, please don't warn me about it".
fpvandoorn commented

This also had this happen to a student just now.

  • Is this caused by the root file not existing/not importing anything? (that was something we fixed afterwards).
  • What is a reliable way to update lean-toolchain? (I'm currently just copying the file from a dependency, but that is probably outdated).
fpvandoorn commented

Additional suggestions:

  • Would it be possible to have a command lake update-toolchain which asks Github for the latest (release candidate) version of Lean, and replaces the lean-toolchain file with that version. (Note: this command is not that useful by itself, but can fix errors like in the OP when running lake update)
  • Perhaps integrate lake update-toolchain into lake update.
    • when lake update runs into an error when reading the lakefile of a dependency, then it runs lake update-toolchain and retries lake update.
    • a command lake update! which is a shortcut for lake update-toolchain && lake update (this should probably not be the default, since it might download 2 separate versions of Lean).

I'm just brainstorming ideas here. @tydeu probably has a better idea what is good here.

  • 👍1