Open kim-em opened 4 months ago
This also had this happen to a student just now.
lean-toolchain
? (I'm currently just copying the file from a dependency, but that is probably outdated).Additional suggestions:
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
)lake update-toolchain
into lake update
.
lake update
runs into an error when reading the lakefile of a dependency, then it runs lake update-toolchain
and retries lake update
.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.
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:
The underlying problem here is that the project was still on
v4.4.0-rc1
, and the upstream repositoryaesop
has now moved to alakefile.toml
, which of course can't be understood byv4.4.0-rc1
.The underlying cause --- that in order for
lake update
to be successful, the user will need to update theirlean-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:
lean-toolchain
in the current project.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).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".