advice on updating libraries

Stream: general

[Kim Morrison]

Keep updating to new toolchains, and creating a tag v4.X.0 every time you update, so downstream libraries can pin to a compatible version. There are some automatic tools to create these tags for you.

See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md and
https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md

[Leo Sin]

Kim Morrison said:

Keep updating to new toolchains, and creating a tag v4.X.0 every time you update, so downstream libraries can pin to a compatible version. There are some automatic tools to create these tags for you.

See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md and
https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md

Thanks for pointing out those CI actions, they're useful when you're dealing with actively maintained libraries or when a project only depends on batteries and/or mathlib.

Where I've felt the pain most is in the less-maintained parts of the ecosystem. For example, when I tried to port my Haskell Advent of Code solutions to Lean recently, I wanted to use Megaparsec, a monadic parser combinator library, which was stuck on v4.0.0 and depended on 3 other unmaintained libraries. I ended up forking and migrating all those dependencies for several releases (v4.21.0-rc3 -> ... -> v4.22.0-rc4 -> v4.23.0-rc2), just so I could keep moving forward. While it was a good learning exercise, it's obviously not something that scales well for casual contributors...

I completely understand that Lean is still evolving, and stability isn't promised yet as stated in leanprover/lean4:RELEASES.md. That's part of the deal to play with cutting-edge tools.
My concern is more about the sustainability: how to keep contributors from burning out on upgrade work while still staying aligned with the latest toolchain.

Maybe the answer is some mix of: some tooling to patch common import breakages across version upgrades (might require some form of explicit marking on commits) and/or having some shim packages to bridge versions like six in python?

I would be curious to hear what others think... especially about lightweight ways to reduce the upgrade tax without dragging the momentum of lean moving forward

[Ruben Van de Velde]

We have talked about these issues before - the main thing we've set up so far is somewhat consistent deprecation warnings for removed decorations and files that stay around at least one release but usually 6 months. So if you bump once a month to the new stable version, it's usually pretty smooth. There's also GitHub actions that keep trying to update mathlib more frequently and file an issue as soon as something goes wrong, but that's probably not going to work if you have multiple dependencies that need updating in tandem

[Ruben Van de Velde]

There's also been discussions about tooling that will automate downstream changes even further, but I don't know if that's on anyone's roadmap right now

[Kim Morrison]

In a thread far far away, @Leo Sin asked:

Leo Sin said:

Btw just wondering are there any tips/prescriptions/best practices in terms of managing lean-toolchain versions to keep forward compatibility for third-party library maintainers?
Because some libraries with old toolchain version seems do not play well with new versions of batteries and/or mathlib...

[Notification Bot]

A message was moved from this topic to #general > advice on updating libraries by Kim Morrison.

[François G. Dorais]

Kim Morrison said:

Keep updating to new toolchains, and creating a tag v4.X.0 every time you update, so downstream libraries can pin to a compatible version. There are some automatic tools to create these tags for you.

The tag v4.X.0 conflicts with using semver for a project. I think lean-v4.X.0 would be a better alternative for these tags on downstream projects.

[Michael Rothgang]

Indeed. Mathlib does not follow semver, but downstream projects could.

[Michael Rothgang]

I'd argue that for projects depending on mathlib, most of the benefits of semver are already harnessed by following these rallying points, and that compatibility with the Lean core version is more important. Yet, semver is (as I understand it), incredibly useful in (e.g.) the Rust ecosystem, and not obstructing that unnecessarily sounds useful.

[Fabrizio Montesi]

Kim Morrison said:

Keep updating to new toolchains, and creating a tag v4.X.0 every time you update, so downstream libraries can pin to a compatible version. There are some automatic tools to create these tags for you.

See https://github.com/leanprover-community/mathlib-update-action/blob/HEAD/README.md and
https://github.com/leanprover-community/lean-release-tag/blob/HEAD/README.md

This looks very useful, thanks!
It means making projects downstream live on the bleeding edge to upgrade, but this seems ok given how quickly the Lean ecosystem is still evolving.

What is Lean's release/tag cadence? This becomes relevant info as soon as one considers the action. Might be worth putting a link to that in the action's documentation.

[Ruben Van de Velde]

Monthly stable releases