I really don't understand the process implied by issues like this: https://github.com/coq-community/aac-tactics/issues/69
Basically, if I tag and something breaks between now and 8.13.0, this will make me look bad as a maintainer. Why would I not want to wait for a stable target like 8.13+beta1 to tag?
... and at least with 8.13+beta1, I would have the possibility of verifying commits to tag in local CI easily
The issue is not fully clear: it is fine if you don't tag now, but you should confirm whether the commit that is used in the Windows installer is OK. That's the most important point for 8.13+beta1.
but what does OK mean with a moving target like
v8.13? I don't know what fixes will be applied that could affect my project.
You can wait. I do check that the tags I have are not broken by PRs that I backport. Since I sent the message I did backport (mostly by mistake) only one PR that slighlty changed the ML API.
So, if the commit I gave does not work, it's my fault, not yours. See the streams of PR I made to repair Coq'CI so that I don't make I fool of myself more than needed ;-)
Also, the point of asking this question is mostly because some maintainers will push commits to master that are in a state that's unsuitable for a release, and they may not want us to pick this commit. But compatibility with 8.13 is really the RM problem, not yours.
OK, so then I will wait until 8.13+beta1 to confirm the commit.
In the past we worked with master in the beta and did the tagging for the release. It was not that rare that it took 6 weeks. I guess the goal here is to avoid this. In the near future this hen and egg problem will be gone with the Coq platform, so that there will be a Coq release (beta or .0), yo do a release of your library (also .beta and .0) and then comes the Coq platform release (again .beta and .0).
@Michael Soegtrop JFYI https://github.com/coq/coq/pull/13449 (it should probably be moved to the platform at some point)
Last updated: Dec 01 2023 at 06:01 UTC