lakefile.lean vs lean-toolchain for specifying lean version

Stream: new members

[rzeta0]

The recent 4.9.0 update causes me enough problem to need wiping and restoring from backups.

Both lean-toolchain and lakefile.lean specific which version of lean I want. This seems wrong, especially if they conflict (as happened with the update).

lean-toolchain:

leanprover/lean4:v4.9.0

lakefile.lean:

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

This latter entry didn't have the specific version specified and it all worked fine for weeks, until the update was announced and I was recommended to. update the lean-toolchain.

Question: Is there a good reason for two versions of the truth, which as we have seen can conflict?

[Mario Carneiro]

The latter entry is just a reference to which branch of the target project (here mathlib) to use. Compiling a branch with the wrong version of lean is unlikely to work. It just so happens that mathlib (and several other projects) create tags/branches named after the lean versions they are targeting, and someday lake might get special support for this naming convention so you don't need to repeat yourself

[rzeta0]

if lean-toolchain says 4.9.0 then not specifying version/branch in wakeful.lean gets the latest RC - which I feel is wrong, but I know others disagree.

developers should have the inconvenience of adding "-rc", normal users should have the easy path

(imho)

[Mario Carneiro]

sure, I don't disagree, I'm just relaying the situation

[Mario Carneiro]

the fact that lake update fails to work to update on pretty much every stable is a major issue which I think the devs are aware of

[Mario Carneiro]

this is caused by the fact that lean-toolchain is only second-class supported by lake, even though it is critical to lake's functionality because it determines which lake will run

[rzeta0]

thanks - and i guess it is voices like ours that push it up the priority list

[fonqL]

My lakefile.lean is:

...
require batteries from git "git@github.com:leanprover-community/batteries.git" @ s!"v{Lean.versionString}"
...

Maybe it would be helpful for the issue?

[rzeta0]

Thanks @fonqL I think your suggestion will help many others. For me, having read that even stable updates may break code, I think I will pin it to 4.9.0 and only manually upgrade of I have the time to recheck all my future content.