Stream: math-comp devs

Topic: 2.2.0 release

Pierre Roux (Jan 17 2024 at 08:52):

We are now starting the release process for mathcomp v2.2.0.
All pull requests targeted to this release have been merged.
This message grabs the lock on the master branch.

Pierre Roux (Jan 17 2024 at 09:23):

Release done, preparing the doc, OPAM and Nix packages.

Karl Palmskog (Jan 17 2024 at 09:33):

@Pierre Roux sorry, I probably wasn't clear enough. The ci-skip has to use the exact same version as the packages added (i.e., 2.2.0 in place of 1.19.0). So in https://github.com/coq/opam/pull/2901 you will probably want to cancel jobs and merge once character has been built.

Karl Palmskog (Jan 17 2024 at 09:35):

another consideration for future MathComp releases: maybe it's a good idea to upload an archive into the release, rather than using an autogenerated GitHub archive like https://github.com/math-comp/math-comp/archive/mathcomp-2.2.0.tar.gz - the issue is that GitHub no longer guarantees stability of the archive (its checksum may change over time). Enrico automatically uploads archives with his release automation, e.g., https://github.com/math-comp/hierarchy-builder/releases/download/v1.7.0/hierarchy-builder-1.7.0.tar.gz - this is best practices to me

Pierre Roux (Jan 17 2024 at 10:05):

Karl Palmskog said:

Pierre Roux sorry, I probably wasn't clear enough. The ci-skip has to use the exact same version as the packages added (i.e., 2.2.0 in place of 1.19.0). So in https://github.com/coq/opam/pull/2901 you will probably want to cancel jobs and merge once character has been built.

I did try to edit the message and relaunch everything but apparently it's not enough

Karl Palmskog (Jan 17 2024 at 10:16):

unfortunately not, it's a kind of one-shot thing

Karl Palmskog (Jun 29 2024 at 17:29):

from what I can tell, 2.2.0 works fine on 8.20+rc1.

Pierre Roux (Jun 29 2024 at 17:34):

Wonderful, I missed the fact that we already have a coq-elpi release (that was lightning fast)

Karl Palmskog (Jun 29 2024 at 17:39):

yes, Enrico did it yesterday

Karl Palmskog (Jun 29 2024 at 17:40):

and he said he would finally fix thecoq-elpi packages using a too-low OCaml lower bound, but time will tell... (PR always needs a bump)

Karl Palmskog (Jun 29 2024 at 17:45):

so with luck, not much in the MathComp world is broken except graph-theory, I think I will do a quick minor release there

Enrico Tassi (Jun 29 2024 at 20:50):

Thanks to the work of @Rodolphe Lepigre coq-elpi builds with dune, hence we can use ppx_optcomp to work on a single branch. So from now on a release for a coq rc is just a release like the others, and can be made in a day or so.

Karl Palmskog (Jun 30 2024 at 09:16):

unfortunately, coq-mathcomp-real-closed.2.0.0 doesn't work on 8.20:

Error: Notation "_ .1" is already defined at level 1 with arguments constr

Pierre Roux (Jun 30 2024 at 09:45):

Just released a 2.0.1

Last updated: Oct 13 2024 at 01:02 UTC