lake: bouncing between versions

Stream: lean4

[Cody Roux]

I have a project that has branches that live between versions. E.g. in one the lakefile.toml contains

[[require]]
  name = "batteries"
  scope = "leanprover-community"
 rev = "main"

and in the other

[[require]]
  name = "batteries"
  scope = "leanprover-community"
 rev = "v4.23.0-rc2"

I'm having trouble switching between the two without pain; what steps should I be running? If I go from the latter to the former and do lake clean && lake update && lake build, the last step fails with (among many others)

trace: .> LEAN_PATH=/workplace/codyroux/plausible/.lake/packages/batteries/.lake/build/lib/lean:/workplace/codyroux/plausible/.lake/build/lib/lean /local/home/codyroux/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/lean /workplace/codyroux/plausible/.lake/packages/batteries/Batteries/Data/Rat/Float.lean -o /workplace/codyroux/plausible/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Rat/Float.olean -i /workplace/codyroux/plausible/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Rat/Float.ilean -c /workplace/codyroux/plausible/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Rat/Float.c --setup /workplace/codyroux/plausible/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Rat/Float.setup.json --json
[...]
error: Batteries/Data/Rat/Float.lean:26:0: instance does not provide concrete values for (semi-)out-params
  Coe ?Rat Float

which suggests that there's a mismatch between the lean Std and Batteries.

What should I be doing? Why is this error occurring?

[Mac Malone]

Running lake update on the branch that points to batteries at main will cause it update the version of batteries used to the latest main.

[Mac Malone]

Ideally, all you should need to run is lake build when swtiching between branches. Lake should be smart enough to checkout the right versions of dependencies and rebuild the changed files.

[Cody Roux]

So how could I possibly be getting the error above?

[Cody Roux]

Let me clarify: the issue is that the wrong version of lean is being used; and that's very likely the culprit.

but lake-toolchain is correctly showing v4.24.0-rc1!

[Mac Malone]

Cody Roux said:

Let me clarify: the issue is that the wrong version of lean is being used; and that's very likely the culprit.

I am confused. What makes you htink the wrong version of Lean is being used? I don't see anything in the error message you posted that suggests that. Do you have more information?

[Cody Roux]

ooooh; shucks; I figured it out: there was a elan override active I had forgotten about.

[Cody Roux]

(I updated the error message, the version being used was 4.23.x)

[Cody Roux]

on a slightly different note, I'm a little disturbed that lean update smashes the lean-toolchain file; is that reasonable?

[Ruben Van de Velde]

This is considered a feature, not a bug :)

[Cody Roux]

I guess I get it. Made my first attempt at backporting quite confusing, though :)

[Cody Roux]

(I also note that --keep-toolchain doesn't seem to appear in the --help docs)

[Andrés Goens]

Ruben Van de Velde said:

This is considered a feature, not a bug :)

is there any way to turn off that "feature" if we don't want it? e.g. if you want to use a specific lean version and add a dependency, how do you fetch the dependency without lake changing the lean version?

[Yaël Dillies]

You cannot do this, unless the dependency also has the same lean version. If you are in this later case, you can write rev = commithashhere under the corresponding entry in the lakefile, where commithashhere refers to a commit of the dependency that is on the same lean version as the rest of your project

[Mac Malone]

Andrés Goens said:

e.g. if you want to use a specific lean version and add a dependency, how do you fetch the dependency without lake changing the lean version?

lake update --keep-toolchain

[Kim Morrison]

Better than specifying a SHA in the rev field is to specify a tag. Many projects in the Lean ecosystem add tag of the form v4.X.0 when they first move to that toolchain.