updating from leanprover/lean4:v4.15.0

Stream: general

[Paige Thomas]

Where could I go about finding instructions for updating an existing repo that uses mathlib?

[Paige Thomas]

lake update doesn't seem to change anything.

[Paige Thomas]

I guess I need to remove the tagged revision from mathlib.

[Paige Thomas]

I changed the revision in lean-toolchain to leanprover/lean4:v4.22.0 and the revision tag for mathlib in lakefile.toml to

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.22.0"

and tried lake build, but it gave a lot of errors.

[Paige Thomas]

I think I see. I think maybe I have to update my external library first.

[Ruben Van de Velde]

You do need lake update after changing lakefile.tomp, though I would recommend only changing one minor version at a time (i.e. 15 → 16 → 17 → ···)

[Jon Eugster]

Paige Thomas said:

I think I see. I think maybe I have to update my external library first.

one major pitfall with multiple dependencies is that there is only ever one version of each (secondary) dependency. So if another dependency also requires e.g. batteries but at a different commit than mathlib does, then you will get countless errors as it tries to build mathlib on this wrong batteries version. It's kind of your responsibility to ensure all required dependencies are compatible. Best to update your external library to stable releases and tag them with e.g. v4.22.0 too

[Paige Thomas]

I see. I think that is probably what is going on. Thank you.

[Alok Singh]

Jon Eugster said:

Paige Thomas said:

I think I see. I think maybe I have to update my external library first.

one major pitfall with multiple dependencies is that there is only ever one version of each (secondary) dependency. So if another dependency also requires e.g. batteries but at a different commit than mathlib does, then you will get countless errors as it tries to build mathlib on this wrong batteries version. It's kind of your responsibility to ensure all required dependencies are compatible. Best to update your external library to stable releases and tag them with e.g. v4.22.0 too

Does the FRO have plans to address this/can it be addressed? This has bitten me and is an especially vexing paper cut.

[Kim Morrison]

Yes, we're definitely thinking about it, and Mac has been working on it.

I think if you are careful not to include any transitively implied dependencies in your lakefile, then the current system usually works okay: pin each dependency to a v4.X.0 tag, and specify the same in lean-toolchain. If there are examples of this not working (i.e. incompatibilities between libraries at the same toolchain tag), please highlight them.