Stream: Coq devs & plugin devs

Topic: 8.16+rc1 is now public

Pierre-Marie Pédrot (Jun 01 2022 at 20:46):

As you may have seen in the discourse feed, habemus V8.16+rc1 estiquetam.

Pierre-Marie Pédrot (Jun 01 2022 at 20:47):

According to the doc, I need to synchronize with the platform people (@Michael Soegtrop ?) and chase package managers to get their stuff in time for the 8.16.0 release.

Théo Zimmermann (Jun 02 2022 at 07:28):

The GitHub notification feed indicates that the tag was removed, but it is still there. What happened?

Michael Soegtrop (Jun 02 2022 at 07:52):

@Pierre-Marie Pédrot : thanks, I will trigger a Coq Platform beta release then. I take care of triggering package managers (I have semi-automated scripts for creating issues for all Coq Platform packages).
What is the planned Coq release date? For Coq Platform - which should be 4..6 weeks after the Coq release, the current plan is "some time in September". Does this match your plans?

Théo Zimmermann (Jun 02 2022 at 07:58):

https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.16 indicates July for 8.16.0. So September sounds good. If we can, we should also make a beta release beforehand. Maybe as part of 2022.04.1 if most package maintainers react fast enough like last time.

Enrico Tassi (Jun 02 2022 at 08:17):

Last time an rc tag was put there was some uncertainty about who should make the opam packages. It this settled now?

Enrico Tassi (Jun 02 2022 at 08:18):

We also need to make sure docker images get out

Théo Zimmermann (Jun 02 2022 at 08:21):

There was a debate whether the RMs should be the ones to take care of opam packaging, but the process hasn't been changed, so this role is still left to volunteer community members (like @Karl Palmskog).

Théo Zimmermann (Jun 02 2022 at 08:22):

Docker images are also important. Usually @Erik Martin-Dorel takes care of them. He has been a bit overwhelmed with the end of the semester lately, so I don't know if he will be available to take care of this.

Gaëtan Gilbert (Jun 02 2022 at 08:45):

Théo Zimmermann said:

The GitHub notification feed indicates that the tag was removed, but it is still there. What happened?

the tag was put wrong so PMP deleted it and put it back
I don't know why there's no second "tha tag was put" notification

Pierre-Marie Pédrot (Jun 02 2022 at 08:47):

Aha, I got busted. I hoped nobody would realize that I screwed up, but machines are omniscient and never forgive.

Michael Soegtrop (Jun 02 2022 at 12:09):

@Théo Zimmermann : I don't want to hurry people too much, so I would separate the release for 8.15.2 and a beta release.

Théo Zimmermann (Jun 02 2022 at 12:10):

I know you don't like to hurry people. But our experience shows that even without telling people to hurry, they are usually quite reactive and most packages can be ready in just one week.

Théo Zimmermann (Jun 04 2022 at 11:46):

Don't forget to ping @Matthieu Sozeau to get him started on the release summary for 8.16.0.

Karl Palmskog (Jun 06 2022 at 13:17):

hi @Pierre-Marie Pédrot is there any obvious reason that the V8.16+rc1 tag is not a release (Pre release) on GitHub? I think we want all RCs to show up directly under https://github.com/coq/coq/releases/

Karl Palmskog (Jun 06 2022 at 13:21):

also, would be nice if someone from the core team (e.g., @Pierre-Marie Pédrot or @Emilio Jesús Gallego Arias) could advise how we are supposed to define the opam files for 8.16+rc1 (and later 8.16.0) for the opam repos. Are coq-core and coq-stdlib now supposed to used, or do I use the old approach like here: https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.15.1/opam

Karl Palmskog (Jun 06 2022 at 13:35):

to give examples of discrepancies between the official opam for 8.15.1 and for example coq-core.opam in the 8.16+rc1 tag:

• the tag requires Dune >= 2.5, while 8.15.1 requires Dune >= 2.5.1
• the tag requires ocamlfind >= 1.8.1 as a runtime dependency, while 8.15.1 requires any ocamlfind as a build dependency
• the tag requres zarith >= 1.11, while 8.15.1 requires zarith >= 1.10

Are all of these real changes to the Coq build process?

Pierre Roux (Jun 06 2022 at 14:42):

Karl Palmskog said:

Are coq-core and coq-stdlib now supposed to used, or do I use the old approach like here: https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.15.1/opam

From what I understand, this change was delayed to 8.17 to avoid merging a PR with major changes just before branching: https://github.com/coq/coq/pull/15560#issuecomment-1120886348

Théo Zimmermann (Jun 06 2022 at 16:07):

Indeed, do not split the packages yet. However, the need for ocamlfind at runtime and the bump of zarith are real.

Karl Palmskog (Jun 06 2022 at 18:20):

OK, 8.16+rc1 is packaged in the core-dev opam repo. But to get it in Docker images, we need Erik. However, maybe @Pierre Roux can make a Bignums release for 8.16 as preparation?

Karl Palmskog (Jun 06 2022 at 18:21):

we can at least test the release in the opam archive CI if it's put here: https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-bignums

Théo Zimmermann (Jun 06 2022 at 18:34):

Do we also need a SerAPI tag / pre-release?

Karl Palmskog (Jun 06 2022 at 18:41):

if we follow the usual procedure for Docker images, then yes

Théo Zimmermann (Jun 06 2022 at 18:42):

Then let's ping @Emilio Jesús Gallego Arias as well.

Emilio Jesús Gallego Arias (Jun 06 2022 at 19:02):

I will take care of the SerAPI stuff asap

Emilio Jesús Gallego Arias (Jun 06 2022 at 19:02):

now that we have Coq universe maybe I keep it tracking master again

Karl Palmskog (Jun 06 2022 at 19:45):

recall how it worked last time: https://github.com/coq/opam-coq-archive/tree/master/extra-dev/packages/coq-serapi/coq-serapi.8.15%2Brc1%2B0.15.0

Pierre Roux (Jun 07 2022 at 07:36):

Karl Palmskog said:

OK, 8.16+rc1 is packaged in the core-dev opam repo. But to get it in Docker images, we need Erik. However, maybe Pierre Roux can make a Bignums release for 8.16 as preparation?

Here it is: https://github.com/coq/opam-coq-archive/pull/2196

Paolo Giarrusso (Aug 06 2022 at 10:31):

Just for planning purposes, when is Coq 8.16.0 expected?

Pierre-Marie Pédrot (Aug 06 2022 at 10:33):

Good question. For me, that's mostly a matter of merging one PR and pushing a button, but I should first inquire from @Michael Soegtrop how the platform is going.

Pierre-Marie Pédrot (Aug 06 2022 at 10:33):

In any case, this should happen soon in August.

Karl Palmskog (Aug 06 2022 at 17:31):

here is a Platform progress bar of sorts (plugins that have tagged releases for 8.16): https://github.com/coq/opam-coq-archive/projects/3

Théo Zimmermann (Aug 07 2022 at 09:45):

IMHO you don't need to wait for the Platform to release 8.16.0. However, it would be good to know if there are any blockers preventing 8.16-compatible releases of Platform packages before tagging.

Michael Soegtrop (Aug 08 2022 at 07:43):

@Pierre-Marie Pédrot : I am a late (was moving homes and didn't manage to finish it before). I plan to do the beta release this week - need top review what came in meanwhile.

Théo Zimmermann (Aug 08 2022 at 07:51):

If I'm not mistaken, there were still no issues created in platform package repositories. I'd still strongly recommend opening these issues at least one week before the beta to give the chance to package authors that haven't yet released an 8.16-compatible version to do so to be included in the beta or to give their opinion about which version to include. (Even though during this vacation period, some will probably miss the issue completely.) Another question is whether there is any actual benefit to releasing the beta early August given that a lot of people will miss it given that they are on vacation. Maybe it should be made ready, but announced only on August 20th or so, when people start coming back from vacation. We might also have trouble getting Windows packages signed by Inria during this period.

Michael Soegtrop (Aug 08 2022 at 07:57):

@Théo Zimmermann : sorry, I meant to say I do the preview this week (including the issues) and the beta as soon as possible.

Théo Zimmermann (Aug 08 2022 at 07:57):

Then our views are again not aligned. To me there is no difference between a preview and a beta Platform release.

Théo Zimmermann (Aug 08 2022 at 07:59):

FTR, CEP#52 only talked about beta releases, and in previous Coq Platform releases we have called "previews" the beta package picks.

Théo Zimmermann (Aug 08 2022 at 07:59):

E.g.:

Preview Coq versions

• Coq 8.15.0 with a preliminary (beta) package collection - all packages already support Coq 8.15.0, but some packages might still be updated.

Pierre-Marie Pédrot (Aug 08 2022 at 10:23):

I realized that I haven't addressed @Karl Palmskog 's question from June 6th, since we still don't have a proper 8.16+rc1 release on github. I don't think it's critical, but I'll do that asap so that it appears before the 8.16.0 release in the timeline.

Michael Soegtrop (Aug 08 2022 at 10:27):

@Pierre-Marie Pédrot : do you plan to do the 8.16.0 release soon?

Pierre-Marie Pédrot (Aug 08 2022 at 10:29):

I don't have much time right now, but hopefully I'll be able to work on that by the end of the week. The only non-trivial step is to get https://github.com/coq/coq/pull/16200 merged. (btw ping @Matthieu Sozeau since there are unaddressed comments in that PR.)

Pierre-Marie Pédrot (Aug 08 2022 at 10:30):

but indeed, I'd like to get rid of 8.16.0 fast.

Matthieu Sozeau (Aug 11 2022 at 10:18):

I think the changes PR is now ready. I'll be back to work next week.

Pierre-Marie Pédrot (Aug 17 2022 at 13:15):

Can somebody merge https://github.com/coq/coq/pull/16200? That's one of the last things to do before releasing 8.16.0.

Pierre-Marie Pédrot (Aug 17 2022 at 13:35):

Thanks @Théo Zimmermann.

Pierre-Marie Pédrot (Aug 17 2022 at 13:35):

There are a few changelogs added between 8.16+rc1 and 8.16.0, is there a script to extract them and remove them somehow, or should I do this by hand?

Guillaume Melquiond (Aug 17 2022 at 13:38):

If nothing changed since a few months ago, you do it by hand on master, then backport it to your branch.

Pierre-Marie Pédrot (Aug 17 2022 at 13:46):

There we go: https://github.com/coq/coq/pull/16386. Any kind soul to assign and merge when refman goes green?

Pierre-Marie Pédrot (Aug 18 2022 at 10:21):

I am basically ready to release 8.16.0, up to waiting some CIs. @Michael Soegtrop do you have any remaining major issue that should deserve some postponing, or is it mostly fine?

Karl Palmskog (Aug 18 2022 at 12:18):

practical question: opam package is still up to volunteers, right @Pierre-Marie Pédrot? Will you flag up the tag on the Discourse and/or here? (I don't follow Coq repo)

Pierre-Marie Pédrot (Aug 18 2022 at 12:19):

there are 8.16 opam packages already though? I've pinged people around for the rc1.

Karl Palmskog (Aug 18 2022 at 12:20):

yes, but 8.16.0 is different. Then one has to endure the endless gauntlet of the opam repo ci

Karl Palmskog (Aug 18 2022 at 12:20):

Alpine Linux will/might interpret some build script differently and that will be the blocker

Pierre-Marie Pédrot (Aug 18 2022 at 12:20):

I see. That said, the todo list puts the harassing opam people after tagging, so I'll see then

Pierre-Marie Pédrot (Aug 18 2022 at 12:21):

Can't we run the CI on 8.16+rc1 already? The build script didn't change.

Karl Palmskog (Aug 18 2022 at 12:21):

8.16+rc1 did not run the opam ci gauntlet

Pierre-Marie Pédrot (Aug 18 2022 at 12:22):

precisely, why can't we do this?

Karl Palmskog (Aug 18 2022 at 12:22):

we can, but then that likely leads to even more trouble with testing and additional support requests

Karl Palmskog (Aug 18 2022 at 12:22):

we don't have any control over the OCaml opam archive, a change can take days/weeks

Karl Palmskog (Aug 18 2022 at 12:23):

for example, one will likely have to ask every user with trouble on 8.16 if they have 8.16+rc1 installed - right now only experts will have 8.16+rc1 installed

Pierre-Marie Pédrot (Aug 18 2022 at 12:23):

This seems like a flaw in the release process then. Reading the doc, the opam release is an afterthought, and in any case not the responsibility of the Coq RM.

Karl Palmskog (Aug 18 2022 at 12:24):

I never claimed the opam stuff was part of the RM TODO, it's part of the Platform release process basically

Pierre-Marie Pédrot (Aug 18 2022 at 12:24):

Ah, OK. Then I should be waiting for feedback from @Michael Soegtrop, right?

Karl Palmskog (Aug 18 2022 at 12:25):

if we want 8.1X+rcY to be part of "normal" Coq releases in opam, I think this should be discussed with both the Core Team and the Platform Team (and other parties)

Karl Palmskog (Aug 18 2022 at 12:26):

right now we follow: https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md#detailed-design

Michael Soegtrop (Aug 19 2022 at 07:38):

@Pierre-Marie Pédrot : I am still busy with the preview (which comes before the beta and is planned to be +rc1 based but I would use 8.16.0 if it is there). There is some work to be done for macOS installers to handle the findlib changes. More importantly I have strange build issues with elpi on Windows (happen reproducably in CI but not locally) - see the discussion in the Dune Zulip thread. I am a bit slow there days cause I am moving homes.

Michael Soegtrop (Aug 19 2022 at 07:39):

Regarding the 8.16.0 release: I didn't check as yet if coq-interval does work now.
@Guillaume Melquiond: does 8.16.0 as is work for you?

Karl Palmskog (Aug 22 2022 at 09:12):

@Pierre-Marie Pédrot so is 8.16.0 just waiting for feedback related to the Platform? At least my view is that 8.16.0 should not be held up by anything Platform related. In fact, releasing 8.16.0 is a prerequisite for doing a lot of necessary work related to the Platform, like putting 8.16 plugins in the released opam repo.

Pierre-Marie Pédrot (Aug 22 2022 at 11:26):

Indeed. I'd like to ensure that there are no major issues before tagging, but if nobody answers in a reasonable timeframe I'll just go ahead. 8.16.0 is just one push away.

Julien Puydt (Aug 22 2022 at 15:30):

I had a (deep) look of what Coq 8.16+rc1 would give on Debian. Quite a few packages would need an update, but for most of them it's either a new version or a trivial patch. Only three packages are still broken on my system: coq-hammer, coq-mtac2 and coq-interval.

Julien Puydt (Aug 22 2022 at 15:31):

Here is a rundown of all Coq-related packages in Debian:

$ ./test_libcoq_packages.py
Hauteur 1
        coq... ok
Hauteur 2
        aac-tactics... ok
        coq-bignums... ok
        coq-dpdgraph... ok
        coq-elpi... ok
        coq-ext-lib... ok
        coq-hammer... erreur!
        coq-hott... ok
        coq-iris... ok
        coq-menhirlib... ok
        coq-record-update... ok
        coq-reduction-effects... ok
        coq-stdpp... ok
        coq-unicoq... ok
        coq-unimath... ok
        flocq... ok
        ott... ok
        paramcoq... ok
        ssreflect... ok
Hauteur 3
        coq-deriving... ok
        coq-equations... ok
        coq-gappa... ok
        coq-hierarchy-builder... ok
        coq-math-classes... ok
        coq-mtac2... erreur!
        coqprime... ok
        coq-reglang... ok
        coq-simple-io... ok
        coquelicot... ok
        mathcomp-bigenough... ok
        mathcomp-finmap... ok
        mathcomp-zify... ok
Hauteur 4
        coq-corn... ok
        coq-extructures... ok
        coq-interval... erreur!
        coq-quickchick... ok
        mathcomp-algebra-tactics... ok
        mathcomp-analysis... ok
        mathcomp-multinomials... ok
        mathcomp-real-closed... ok
Hauteur 5
        coqeal... ok

Janno (Aug 22 2022 at 15:58):

coq-mtac2 hasn't really changed in a while so I am surprised to see it fail. Maybe it's because I haven't gotten around to creating a 8.16 branch and tag yet? Either way, I am happy to help fix this.

Julien Puydt (Aug 22 2022 at 16:03):

For mtac2, there seem to be issues with global constants not working exactly the same ; I took a few changes from the git repo which got me a little further, but indeed a new tag would help. Thanks!

Michael Soegtrop (Aug 23 2022 at 06:36):

@Julien Puydt : please have a look at (https://github.com/coq/platform/issues/274) - this is a meta issue were I track the package picks for the 8.16 Coq Platform. I create an issue for each package in Coq Platform and ask the maintainers which version they want in Coq Platform for 8.16 - the issue I linked above has links to all these issues.

Julien Puydt (Aug 23 2022 at 07:01):

I know, I saw the reports -- and provided patches when I could

Julien Puydt (Aug 29 2022 at 07:43):

Now the two only hurdles to Coq 8.16 in Debian are coq-hammer and coq itself.

Pierre-Marie Pédrot (Aug 29 2022 at 07:44):

Anybody working on https://github.com/coq/coq/issues/16406? I consider this a blocker for 8.16.0.

Pierre-Marie Pédrot (Aug 29 2022 at 07:44):

this is the kind of nasty issues that are hard to track in a CI but very annoying in daily life

Pierre-Marie Pédrot (Aug 29 2022 at 07:45):

in particular I don't know if @Guillaume Melquiond 's proposed patch is correct and whether the issue also happens with vo as suggested

Pierre-Marie Pédrot (Aug 29 2022 at 07:45):

(ping @Enrico Tassi since this is findlib-related stuff)

Théo Zimmermann (Aug 29 2022 at 08:20):

Put it on the agenda for the next Coq Call if nobody has answered by tomorrow.

Guillaume Melquiond (Aug 29 2022 at 11:33):

To add a bit of information, I tested and I can confirm that my proposed patch does solve the issue. But I don't know if it is correct or if a List.rev somewhere later should be used instead.

Guillaume Melquiond (Aug 29 2022 at 11:33):

(That said, List.rev is presumably a bad idea, because it would cause a right-to-left handling of -I, contrarily to the de facto standard set by gcc, ocamlc, etc.)

Gaëtan Gilbert (Aug 29 2022 at 11:34):

please discuss specifics in the issue as it's going to get confusing otherwise

Karl Palmskog (Sep 05 2022 at 11:18):

are there any big blockers now for 8.16.0? Or are we closer now that https://github.com/coq/coq/issues/16406 is closed?

Last updated: Nov 29 2023 at 04:01 UTC