In the seeming absence of Matthieu, could someone in core/Nantes make a tag of Equations for 8.18? This would make it possible to test more projects with 8.18+rc1.
I can make an opam package based on the tag, if that helps
At least @Pierre-Marie Pédrot has access to the repo, I think.
I've got access indeed. What's the exact tag that needs to be pushed?
Equations CI is pinned on 21a3306a7e13b3037d20492bfdb5da75463929fb in 8.18+rc1, so I guess this is the commit to tag?
and given the tag naming convention I expect it to be
@Karl Palmskog if this looks OK to you I can tag, waiting for your approval
ah, but we also need to update the opam file
or is it taken care downstream?
It's probably not critical to have an outdated in-repo opam file for the release, but maybe not a very good practice.
from what I gather the local opam file is only updated for real releases, not rc
Oh, but there should not be two Equations releases for 8.18 in fact.
In principle, per the Coq rc policy, the new Equations release should probably be the final one...
Even if some packages (like SerAPI) prefer to do two releases.
Since I'm not the official guy in charge of Equations I'd rather not perform a full-blown release
@Pierre-Marie Pédrot given that Enrico & Maxime should guarantee 8.18+rc1 compatibility transfers to 8.18.0, I don't think the tag should have the suffix
@Karl Palmskog note that there are already some beta tags in equations 1.3, e.g.
but from what I remember those refer to Equations betas, not Coq betas
(this is only 2 years old, I don't remember when we changed our processes)
this would make sense given the history
can't it just be called
v1.3-8.18? Given that Equations 1.3 is already out, and this is just that for 8.18?
The last 8.17 tag is called
v1.3-8.17 but the commit comment mentions 8.17+rc1 so probably no rc suffix needed
I'll take the great responsibility of performing a 8.18 release of Equations if this is urgent
(previous releases were just tweaking opam and ci files so this shouldn't be that hard)
would be great if you did, there is no huge urgency, but it would really help us with testing 8.18rc1
and again, all that's needed is a tag and I can take it from there with packaging
a tag is about as bad as an actual release because you're not supposed to overwrite it
but given the low amount of changes since the 8.17 release I think this is in my ballpark
I think we should weigh the not-so-dramatic consequences of a bad tag against the potentially big benefits of testing
and ideally, we establish a protocol with Matthieu for next time
ok, I'm on it
.opam file in the repo is really a minor detail these days, since for releases/tags the canonical opam file is in the Coq opam archive. Nevertheless, it can be useful to fix if it's not difficult.
the CI seems to fail, any expert around? https://github.com/mattam82/Coq-Equations/actions/runs/5892679408/job/15982514140?pr=558
is it just the hott package not being released for 8.18 yet?
that's exactly right, from what I can see. Usually @Ali Caglayan handles the hott releases, but I don't think we should wait for this for an Equations tag.
OK, I'll do like happened last time, i.e. deactivating the hott targets in the CI
I did a release for hott 8.18 and submitted opam archive PR
did you try it manually on 8.18+rc? If it's submitted to
released, CI can't check with
Last updated: Nov 29 2023 at 21:01 UTC