versioning

Stream: FLT

[Kevin Buzzard]

I was just reading the blog post for Lean v4.12 and it talks about versioning:

FLTversion.png

Should comments like this apply to the FLT repo? Do people have suggestions about what if anything we should be doing here?

[Pietro Monticone]

I don’t believe that semantic versioning is necessary for FLT, as it functions as a project repository rather than a package repository.

Do you anticipate that it will be used as a package in the future?

[Eric Wieser]

I suspect in general the way versioning will be used is to just match the version number of Lean

[Kim Morrison]

Yes, maths projects shouldn't worry about versioning.

[Kim Morrison]

Should have made that clear.

[Kim Morrison]

Just try to keep up with Mathlib.

[Kim Morrison]

And if you like, specifically update to Mathlib's v4.12.0 and/or v4.13.0-rc1 tags, and then create that tag yourself.

[Kim Morrison]

This then gives anyone coming later a way of getting a snapshot of a project that worked with a particular Mathlib that hopefully other projects also worked with. :-)

[Kevin Buzzard]

Should a v4.12.0 mean "it works with some random mathlib of that month, and Lean 4.12.0" or "it works with the version of mathlib tagged v4.12.0?

In other words, for example, right now FLT is on Lean v4.12.0-rc1 and some random mathlib which uses this version of Lean. Can I safely tag the most recent commit with v4.12.0-rc1?

[Eric Wieser]

It's best practice to be exactly on the v4.12.0 commit of mathlib, in case anyone wants to depend on two projects downstream of mathlib simultaneously

[Johan Commelin]

But of course, once you've bumped to v4.x.y of mathlib and tagged that commit of your repo with v4.x.y you are free to bump mathlib again later that month, if that is helpful.

[Kevin Buzzard]

Ok thanks these comments are very helpful!

[Pietro Monticone]

I have just written and added to the LeanProject template a create-release workflow which automates the creation of a new Git tag and GitHub release when the lean-toolchain file is updated in the main branch.

Let me know if you want to use it in FLT.

[Kevin Buzzard]

I can't really let you know because I don't really understand what all this means. Happy to hear informed advice though!

[Ruben Van de Velde]

It's basically a way of saying "this version of FLT works with this version of mathlib". I think it would be useful for the monthly v4.XX.0 versions, but I'm less convinced it's useful for versions in between (though this is not strongly held)

[Shreyas Srinivas]

It is useful for downstream users of your library. I am not sure how it helps contributors who need to work off the latest possible commit on the main branch

[Ruben Van de Velde]

I think it only helps downstream users that depend on multiple libraries, and only if those all have tags for the same mathlib commits