Hi all, V8.16.0 has just been tagged.
In case you have something to do with the release, here is a link to the TODO list: https://github.com/coq/coq/issues/16085
This includes, but is not limited to:
I can do the opam repo submission tonight, unless someone else wants to do it. If nobody else claims the task, I will start with only the coq
package, and if it gets merged, I will do coqide
.
@Karl Palmskog thanks, I'll tick out that item on the list
I'll work on packaging it for Debian when I'll have a suitably tagged coq-hammer.
@Julien Puydt maybe https://github.com/lukaszcz/coqhammer/releases/tag/v1.3.2%2B8.16 ?
The usual tags for coq-hammer where of the form <version>-coq<coq_version> ; that one is <version>+<coq_version> ; changing version numbering makes things more difficult.
For example, I only saw this release because I went to check -- the automatic tools couldn't notify me as they should have!
ah, you might want to ask the CoqHammer author to make a new tag then (pointing to the new-but-unconventionally-named tag). We have other repos like that where there are several tags for a single commit to satisfy several naming schemes.
Who is in charge of the website? I've written https://github.com/coq/www/pull/201 as per the rules, but I don't know who's supposed to merge it
I did ask: https://github.com/lukaszcz/coqhammer/issues/143
@Pierre-Marie Pédrot we have a team of maintainers. I can review+merge now if you want
I assume somebody has to write a release post or something as well?
hmm, isn't this only for the Platform release?
I thought a courtesy message like "8.16.0 has been tagged, Platform project maintainers please test and release" in one or more forums was enough (since most people shouldn't care)
I've written such a post on discourse. The doc mentions coqdev but I think it's officially dead.
then according to CEP 52, I think that's it? I could be wrong.
the Platform release post is a different beast and works on a different level and schedule.
Just to double check: are there supposed to be a lot empty subsections at the top of https://coq.github.io/doc/v8.16/refman/changes.html (under "Unreleased changes" section)? Or will this be fixed by some automation? I see no such empty subsections in https://coq.github.io/doc/v8.15/refman/changes.html
You are looking at the documentation of the branch 8.16, which is in mode is_a_released_version = false
(contrarily to the tag 8.16.0). This does not happen for the branch 8.15, since no commit was ever pushed to switch back from is_a_released_version = true
to is_a_released_version = false
after tag 8.15.2. If Pierre-Marie had been a bit more lazy (that is, if he had waited for some actual changes on the branch), you would not yet see this "Unreleased changes" section.
OK, so if I'm reading it right it will sort itself out when some changes are pushed? (this is the changelog linked in the GitHub release for 8.16.0)
No, it will get worse as time goes by, since unreleased changes will be pushed to the branch.
You can use this stable link instead which does not contain the moving branch stuff: https://coq.inria.fr/distrib/V8.16.0/refman/
Pierre-Marie Pédrot said:
- ping Théo Zimmermann to switch the default version of the reference manual on the website.
Done: https://coq.inria.fr/refman/
ah, then someone should edit the release text to replace with this link here: https://github.com/coq/coq/releases/tag/V8.16.0
I should also do the Zenodo release. I'll put this on my todo list.
Ok, I checked 8.16.0 went well with everything Debian has, and I asked for permission before I upload 18 new package versions and trigger the re-build of 23 others. When they answer, I'll push the new packages, the build daemons will do their tricks and 41 packages will go forward! :+1:
Here is the bug report asking for permission.
@Julien Puydt : I will double check today if this matches the versions picked by the authors for Coq Platform.
@Michael Soegtrop If you have a suitable .csv, I can probably check faster -- I don't want to update this public page too soon, but I could re-generate it locally to have a look.
brace for CI impact: https://github.com/ocaml/opam-repository/pull/22066
you get a red CI flag if your reverse dependencies fail to work. That's a new one for me.
It has been the case for quite some time. But that is an issue only if your package is actually the cause of the failure. Here, the failure looks completely unrelated to Coq, but rather a random breakage of Frama-C.
that still doesn't make much sense to me. Some package that someone else made uses some internal API of your package, and doesn't add upper version bounds. When this doesn't work for a new version of your package, this is considered evidence against merging your package?
No, it just means that it is your job to fix the upper bounds.
of someone else's package? I can't control whether they put "my_stuff" {>= "1.0"}
Yes, of someone else's package. For example, if you look at https://github.com/ocaml/opam-repository/pull/21313/files, you will see that the maintainer of mlmpfr modified the why3 packages, and that is the usual process.
for high-profile packages where people know about each other, sure, you can set it up like that. Harder to see that up-front, just submitting a package PR leads to an obligation to potentially edit package bounds for hundreds of packages
if we did that for the Coq opam archive, it would probably be more the job of maintainers and automation to edit bounds.
Opam's repository has stricter requirements than ours, that is, when a user installs a package, it should succeed (or opam should complain about unsatisfiable constraints). Thus, no new/updated package should ever break an existing package. Obviously, testing reverse dependencies is no 100% foolproof, but it goes a long way toward that goal..
In Debian, packages enter in "unstable", and migrate to "testing" only when they don't break anything in there. And that restriction includes rdeps, so indeed a package five dependency levels from the package you work on can become your problem. That how we ensure we get a coherent distribution and not just a bunch of packages crammed together. That can indeed become pretty painful when the target maintainer doesn't move -- either because unresponsive or because another one of her/his package deps can't be updated...
@Julien Puydt : let me spend a day or two to update the (not yet released) preview to a beta - I hope everything is there now. I will then upload the .csv file.
I just did a run through all the Coq Platform package tag issues - it looks good, only one package is missing a tag (but I have a working commit - maybe good enough for a beta for just one package) and some packages are missing pick confirmations and/or public opam files. An open question is if I can fix elpi on Windows - there used to be weird build issues which are only reproducible in CI - not in local machines.
here is why I always submit the CoqIDE package separately:
4.10
coqide.8.16.0
lower-bounds (failed: Unbound module GtkData.StyleContext)
We have tons of Gtk errors showing in CI here.
any input on what the lower bound for lablgtk3-sourceview3
should be is appreciated...
looks like 3.1.2 is the minimum released version that works.
That seems consistent with the first item there: https://coq.inria.fr/distrib/V8.16.0/refman/changes.html#id120
sigh, this was not synchronized with the Coq opam archive core-dev
. I'll have to do some PRs.
@Julien Puydt : I attached a CSV and readMe file which should be very close to the final release. beta.csv beta.md
@Michael Soegtrop I'm a bit late on you there and there, but we're very near. You added a few things that weren't there before and I should probably try to package ; see here
@Julien Puydt : please note that I plan the following updates:
I will follow up on the packages where you are ahead with the authors.
One question: what does "+b1" mean?
For mathcomp-analysis, I'll wait until the transition to 8.16.0 is complete ; for serapi, coq-libhyps and coq-relation-algebra I think there are licensing issues so I don't package them.
The +b? is for a recompilation, so it's the same source package. Debian version numbers look like <upstream version>-<debian package number><+b? optional build number>
Julien Puydt said:
For mathcomp-analysis, I'll wait until the transition to 8.16.0 is complete
What do you mean? Analysis is compatible with Coq 8.16 since 0.5.2.
@Pierre Roux I mean that with the release of coq 8.16.0, 41 packages in Debian needed to be updated or recompiled, so I need things to clear up before I push something new in this set -- from 41 packages tuesday morning we're still 18 packages from being done. Notice it's very slow because some architectures lack the build-bot computing power to go faster...
Ok, so if I understand correctly, that's on Debian side and you don't need anything from Analysis developers.
@Pierre Roux Yes indeed, it's me waiting for an automated process before I package the new version. Or, well, more precisely before I upload it : the packaging itself already went smoothly.
very nice to have 40+ packages compatible with 8.16 almost from day 0 of tagging. Probably a first in Coq history.
how many were done during the rc period?
hard to count exactly, but maybe 25-30 or so? cursory count of PRs
some things were also tagged during the rc period, but not packaged in released
yet. Examples: UniCoq, Mtac2, CoqHammer
so 2/3 were done during rc. I think this is good, since that is what the rc period is for, really.
if we want more during rc, I think the only way is more proactiveness from Platform and opam repo maintainers (advertising, pinging, etc.). Not sure we have the spare cycles for that. I'd just be happy if we can keep the 25-30 packages rolling in for 8.17+rc1.
I think it is already good, I just wanted to check that the rc period was not "wasted" as the beta one was...
I'm not sure if we found a lot of bugs in Coq itself with the 8.16 rc? We did find a number of issues in packages with the rc, though, which is crucial for the Platform.
from opam repo point of view, >= 2 month RC was good, wasn't super stressed with adding plugin packages to extra-dev
and then moving to released
one item that might help though: some documentation (in the Coq repo?) for how to test your project with an RC in the recommended way: use core-dev
opam repo, pin the Coq version, add extra-dev
for your deps and possibly pin them, build as usual
That is exactly my point: we are not finding many bugs, so let's call it rc (and not beta) and have people start to port their code to the new version.
We did find some bugs, eg in the handling of paths... so the period was still good to have (and we did work on the doc)
As another example, a deprecation (of :>
syntax in typeclass declarations:https://github.com/coq/coq/pull/16237 ) appeared unfortunate and was abandoned between rc and 8.16.0.
I don't know why exactly, but Guillaume said that it was impossible to port coq-interval to rc, but it works fine in .0.
So the RC period is definitely worthwhile.
Karl Palmskog said:
I think the only way is more proactiveness from Platform
If you have suggestions to improve the "please pick/tag" issue creation, please let me know (it was a bit late this time cause I moved homes but well before the .0 release).
One thing I want to improve is to make a list of package owners and "at" address them in the issues - quite a fraction doesn't seem to get notified of the issues otherwise.
The meta issue is here btw.: (https://github.com/coq/platform/issues/274)
Otherwise I am quite happy with the process as is and also didn't get any negative feedback or suggestions for improvement from package maintainers.
we could perhaps link some documentation on testing-with-rc-best-practices in the Platform issues. That's probably all I can think of right now.
Yes, it doesn't seem to be obvious to many that one should use the preview Coq Platform (although I mention this in the issues). Some longer doc and a link might be better.
Michael Soegtrop said:
I don't know why exactly, but Guillaume said that it was impossible to port coq-interval to rc, but it works fine in .0.
So the RC period is definitely worthwhile.
probably https://github.com/coq/coq/issues/16406
Théo Zimmermann said:
I should also do the Zenodo release. I'll put this on my todo list.
Any updates on the zenodo release? :)
I had a big deadline today for which I focused all my attention, but I should be able to do this toward the end of the week. Would that be OK for you? If not, I may squeeze it sooner.
@Yannick Forster Done: https://zenodo.org/record/7313584
Last updated: Jun 08 2023 at 04:01 UTC