As you may have seen in the discourse feed, habemus V8.16+rc1 estiquetam.
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.
The GitHub notification feed indicates that the tag was removed, but it is still there. What happened?
@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?
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.
Last time an rc tag was put there was some uncertainty about who should make the opam packages. It this settled now?
We also need to make sure docker images get out
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).
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.
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
Aha, I got busted. I hoped nobody would realize that I screwed up, but machines are omniscient and never forgive.
@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.
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.
Don't forget to ping @Matthieu Sozeau to get him started on the release summary for 8.16.0.
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/
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
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:
Are all of these real changes to the Coq build process?
Karl Palmskog said:
Are
coq-core
andcoq-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
Indeed, do not split the packages yet. However, the need for ocamlfind at runtime and the bump of zarith are real.
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?
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
Do we also need a SerAPI tag / pre-release?
if we follow the usual procedure for Docker images, then yes
Then let's ping @Emilio Jesús Gallego Arias as well.
I will take care of the SerAPI stuff asap
now that we have Coq universe maybe I keep it tracking master again
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
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
Just for planning purposes, when is Coq 8.16.0 expected?
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.
In any case, this should happen soon in August.
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
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.
@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.
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.
@Théo Zimmermann : sorry, I meant to say I do the preview this week (including the issues) and the beta as soon as possible.
Then our views are again not aligned. To me there is no difference between a preview and a beta Platform release.
FTR, CEP#52 only talked about beta releases, and in previous Coq Platform releases we have called "previews" the beta package picks.
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.
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.
@Pierre-Marie Pédrot : do you plan to do the 8.16.0 release soon?
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.)
but indeed, I'd like to get rid of 8.16.0 fast.
I think the changes PR is now ready. I'll be back to work next week.
Can somebody merge https://github.com/coq/coq/pull/16200? That's one of the last things to do before releasing 8.16.0.
Thanks @Théo Zimmermann.
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?
If nothing changed since a few months ago, you do it by hand on master
, then backport it to your branch.
There we go: https://github.com/coq/coq/pull/16386. Any kind soul to assign and merge when refman goes green?
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?
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)
there are 8.16 opam packages already though? I've pinged people around for the rc1.
yes, but 8.16.0 is different. Then one has to endure the endless gauntlet of the opam repo ci
Alpine Linux will/might interpret some build script differently and that will be the blocker
I see. That said, the todo list puts the harassing opam people after tagging, so I'll see then
Can't we run the CI on 8.16+rc1 already? The build script didn't change.
8.16+rc1 did not run the opam ci gauntlet
precisely, why can't we do this?
we can, but then that likely leads to even more trouble with testing and additional support requests
we don't have any control over the OCaml opam archive, a change can take days/weeks
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
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.
I never claimed the opam stuff was part of the RM TODO, it's part of the Platform release process basically
Ah, OK. Then I should be waiting for feedback from @Michael Soegtrop, right?
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)
right now we follow: https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md#detailed-design
@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.
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?
@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.
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.
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.
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
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.
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!
@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.
I know, I saw the reports -- and provided patches when I could
Now the two only hurdles to Coq 8.16 in Debian are coq-hammer and coq itself.
Anybody working on https://github.com/coq/coq/issues/16406? I consider this a blocker for 8.16.0.
this is the kind of nasty issues that are hard to track in a CI but very annoying in daily life
in particular I don't know if @Guillaume Melquiond 's proposed patch is correct and whether the issue also happens with vo as suggested
(ping @Enrico Tassi since this is findlib-related stuff)
Put it on the agenda for the next Coq Call if nobody has answered by tomorrow.
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.
(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.)
please discuss specifics in the issue as it's going to get confusing otherwise
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: May 28 2023 at 13:30 UTC