Stream: Coq devs & plugin devs

Topic: Equations tag for 8.18

view this post on Zulip Karl Palmskog (Aug 16 2023 at 18:49):

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.

view this post on Zulip Karl Palmskog (Aug 16 2023 at 18:52):

I can make an opam package based on the tag, if that helps

view this post on Zulip Théo Zimmermann (Aug 17 2023 at 14:40):

At least @Pierre-Marie Pédrot has access to the repo, I think.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:43):

I've got access indeed. What's the exact tag that needs to be pushed?

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:45):

Equations CI is pinned on 21a3306a7e13b3037d20492bfdb5da75463929fb in 8.18+rc1, so I guess this is the commit to tag?

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:46):

and given the tag naming convention I expect it to be v1.3-8.18+rc1

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:47):

@Karl Palmskog if this looks OK to you I can tag, waiting for your approval

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:50):

ah, but we also need to update the opam file

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:50):

or is it taken care downstream?

view this post on Zulip Théo Zimmermann (Aug 17 2023 at 14:54):

It's probably not critical to have an outdated in-repo opam file for the release, but maybe not a very good practice.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:55):

from what I gather the local opam file is only updated for real releases, not rc

view this post on Zulip Théo Zimmermann (Aug 17 2023 at 14:55):

Oh, but there should not be two Equations releases for 8.18 in fact.

view this post on Zulip Théo Zimmermann (Aug 17 2023 at 14:56):

In principle, per the Coq rc policy, the new Equations release should probably be the final one...

view this post on Zulip Théo Zimmermann (Aug 17 2023 at 14:56):

Even if some packages (like SerAPI) prefer to do two releases.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:56):

Since I'm not the official guy in charge of Equations I'd rather not perform a full-blown release

view this post on Zulip Karl Palmskog (Aug 17 2023 at 14:57):

@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 +rc1.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:57):

@Karl Palmskog note that there are already some beta tags in equations 1.3, e.g. v1.3-8.13beta2

view this post on Zulip Karl Palmskog (Aug 17 2023 at 14:58):

but from what I remember those refer to Equations betas, not Coq betas

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:58):

(this is only 2 years old, I don't remember when we changed our processes)

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 14:59):

this would make sense given the history

view this post on Zulip Karl Palmskog (Aug 17 2023 at 14:59):

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?

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:00):

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

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:01):

I'll take the great responsibility of performing a 8.18 release of Equations if this is urgent

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:01):

(previous releases were just tweaking opam and ci files so this shouldn't be that hard)

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:01):

would be great if you did, there is no huge urgency, but it would really help us with testing 8.18rc1

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:01):

and again, all that's needed is a tag and I can take it from there with packaging

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:02):

a tag is about as bad as an actual release because you're not supposed to overwrite it

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:03):

but given the low amount of changes since the 8.17 release I think this is in my ballpark

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:04):

I think we should weigh the not-so-dramatic consequences of a bad tag against the potentially big benefits of testing

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:04):

and ideally, we establish a protocol with Matthieu for next time

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:04):

ok, I'm on it

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:07):

an outdated .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.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:13):

the CI seems to fail, any expert around? https://github.com/mattam82/Coq-Equations/actions/runs/5892679408/job/15982514140?pr=558

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:13):

is it just the hott package not being released for 8.18 yet?

view this post on Zulip Karl Palmskog (Aug 17 2023 at 15:15):

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.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:15):

OK, I'll do like happened last time, i.e. deactivating the hott targets in the CI

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2023 at 15:24):

done

view this post on Zulip Ali Caglayan (Aug 19 2023 at 14:01):

I did a release for hott 8.18 and submitted opam archive PR

view this post on Zulip Karl Palmskog (Aug 19 2023 at 14:04):

did you try it manually on 8.18+rc? If it's submitted to released, CI can't check with 8.18+rc1

Last updated: Nov 29 2023 at 21:01 UTC