best workflow for bumping mathlib

Stream: lean4

[Jakob von Raumer]

Has anybody found a good workflow to bump lean and (several months of) mathlib versions in big libraries of proofs that depend on it? There's probably not a catch-all answer to this, but is there anything better than to have two copies of the code and compare proof states manually? Any tools that give you the point of divergence or that would track renamings or other changes in mathlib and apply parallel changes to another codebase?

[Kim Morrison]

The only tooling that exists at present is the deprecation warnings, which we are trying to be more consistent about!

[Kim Morrison]

Search for leanup for discussion of an ambitious but as yet non-existent tool to help.

[Jakob von Raumer]

The deprecation warnings are already super helpful :smile:

[Kim Morrison]

Are you able to share which library? (Possibly privately?)

[Kim Morrison]

My main piece of advice would be to bump one version at a time -- i.e. using the v4.X.0 tags.

[Jakob von Raumer]

Mostly verifications of functions using Aegis, including verifying fixed-point arithmetics approximations of real-valued specifications, so changes regarding ZMod and casts cause most of the breakage.

[Kim Morrison]

We create a v4.X.0 for the first commit when Mathlib has moved to the new release v4.X.0.

[Kim Morrison]

You could even try bumping to both these tags (at which point you need to deal with language changes) and between, bumping to the commits immediately prior to those tags (the language has not changed, but Mathlib has evolved).

[Jakob von Raumer]

Thanks, I'll try that!

[llllvvuu]

At some point I also brought up the idea of using conventional commit's ! (e.g. "feat!", "refactor!"). Maybe too hard though.