Please tag a new release with MC 2 support

[SnarkBoojum]

Debian will release a new stable version tomorrow after months of freeze. As the rolling release will start again, I'll want to update the Coq-related packages - there are two big new toys I would like to ship: coq 8.17 and MC2.

Can you tag a new release with MC2 ?

Thanks

[palmskog]

@SnarkBoojum for several years, we have worked to set up a project release process that is attuned to Coq and the Coq Platform's release process (CEP 52 is the official description).

In this approach, most projects will do releases when they are asked to by the Platform release manager, since it is then guaranteed to end up in the Platform release and tested for compatibility with other packages in the same release, etc. This doesn't preclude other releases that maintainers themselves want to do, like MathComp 2.0.0.

However, what you are asking now (and will probably ask of other related projects) are for releases/tags not related to the Coq Platform, but to an "alternative" distribution in Debian that seemingly does not follow the Coq Platform (the Platform is still using the MathComp 1.X series). If I do a release now, I have no guarantees that this release will work with Coq 8.18.0, and I may be forced to do a new, in effect unnecessary release when the 8.18 release candidate is out.

Hence, I think you should simply wait with the Debian packaging until Coq 8.18+rc1 is out, so maintainers don't have to waste time doing several releases. My bottom line is that I will wait with a release of RegLang for MC 2.0 until 8.18+rc1 is out.

cc: @Zimmi48

[SnarkBoojum]

I don't get your point. You seem basically annoyed because Debian isn't the Coq Platform. But neither is OpenSuse, Gentoo, Fedora or so many distributions the mind boggles... Each and every one of them picks the software it wants and which version of it, checks for coherence of the whole and ships on a regular basis -- with its own schedule. It works, and has since decades, with thousands of packages to keep in a herd.

Shipping too infrequently is a bad thing: that means many big changes at once. Then when ('if' would be unrealistic) things break there are many possible sources for the new issue and debugging becomes difficult. More milestones actually means less work.

In general upstreams decide internally when they have reached a milestone (new features, bug fixes, new/updated dependencies... sometimes just better translations) and simply tag a new release... and it's up to the distributions to decide what they do with it.

[palmskog]

It's fine by me that there exists other distributions like Debian. But in the Coq community, the Coq Platform is the distribution above all others, and we advise all other distributions to follow it. You are now asking for releases that are not needed for the Coq Platform, and to me it's wasted maintainer time to put out a release we are not guaranteed to be able to use in the Coq Platform. As I said, I will be happy to do a new release once Coq 8.18+rc1 is out, since this guarantees this release can be part of the next Platform release.

Coq itself is on a 6-month release schedule, and the Platform generally follows Coq's schedule with some lag. To me, this is often enough to release minor projects like RegLang for the general Coq community's purposes. The only scenario I can see changing this is if there is some bigger downstream Coq library that uses RegLang and is stuck due to some issue with RegLang. But I'm not aware of RegLang consumers beyond some of my private projects and Regexp Brzozowski.

[palmskog]

Release schedule for 8.18 is here: https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.18

[chdoc]

I agree with @palmskog. We make releases in time for the platform and let other platforms choose whatever version they want. Can we close this?

[palmskog]

@chdoc I think we can keep this issue open as a service, so anyone interested will know when the MC 2.0 compatible RegLang is out (when they subscribe to the issue and it gets closed).

[palmskog]

Coq 8.18+rc1 is now out, and I plan to do a release of RegLang (called 1.2 to match MC 2.0 and indicate changes vs. 1.1.X) as soon as MC 2.0 builds properly on 8.18+rc1. For example, we are waiting for LPCIC/coq-elpi#489

[palmskog]

Release for MathComp 2 done: https://github.com/coq-community/reglang/releases/tag/v1.2.0

Package is available on the Coq opam archive: coq-reglang.1.2.0