Pierre-Marie Pédrot (Sep 05 2022 at 11:44): Pierre-Marie Pédrot (Sep 05 2022 at 11:44):Hi all, V8.16.0 has just been tagged.
Pierre-Marie Pédrot (Sep 05 2022 at 11:45):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
Pierre-Marie Pédrot (Sep 05 2022 at 11:46):This includes, but is not limited to:
Pierre-Marie Pédrot (Sep 05 2022 at 11:46): Pierre-Marie Pédrot (Sep 05 2022 at 11:46): Pierre-Marie Pédrot (Sep 05 2022 at 11:47): Karl Palmskog (Sep 05 2022 at 11:47):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.
Pierre-Marie Pédrot (Sep 05 2022 at 11:47): Pierre-Marie Pédrot (Sep 05 2022 at 11:48):@Karl Palmskog thanks, I'll tick out that item on the list
Julien Puydt (Sep 05 2022 at 11:48):I'll work on packaging it for Debian when I'll have a suitably tagged coq-hammer.
Karl Palmskog (Sep 05 2022 at 11:48):@Julien Puydt maybe https://github.com/lukaszcz/coqhammer/releases/tag/v1.3.2%2B8.16 ?
Julien Puydt (Sep 05 2022 at 11:53):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!
Karl Palmskog (Sep 05 2022 at 11:58):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.
Pierre-Marie Pédrot (Sep 05 2022 at 12:10):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
Julien Puydt (Sep 05 2022 at 12:30):I did ask: https://github.com/lukaszcz/coqhammer/issues/143
Karl Palmskog (Sep 05 2022 at 12:56):@Pierre-Marie Pédrot we have a team of maintainers. I can review+merge now if you want
Pierre-Marie Pédrot (Sep 05 2022 at 12:58):I assume somebody has to write a release post or something as well?
Karl Palmskog (Sep 05 2022 at 13:20):hmm, isn't this only for the Platform release?
Karl Palmskog (Sep 05 2022 at 13:21):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)
Pierre-Marie Pédrot (Sep 05 2022 at 13:22):I've written such a post on discourse. The doc mentions coqdev but I think it's officially dead.
Karl Palmskog (Sep 05 2022 at 13:24):then according to CEP 52, I think that's it? I could be wrong.
Karl Palmskog (Sep 05 2022 at 13:25):the Platform release post is a different beast and works on a different level and schedule.
Karl Palmskog (Sep 05 2022 at 15:06):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
Guillaume Melquiond (Sep 05 2022 at 15:18):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.
Karl Palmskog (Sep 05 2022 at 15:23):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)
Guillaume Melquiond (Sep 05 2022 at 15:36):No, it will get worse as time goes by, since unreleased changes will be pushed to the branch.
Théo Zimmermann (Sep 05 2022 at 17:44):You can use this stable link instead which does not contain the moving branch stuff: https://coq.inria.fr/distrib/V8.16.0/refman/
Théo Zimmermann (Sep 05 2022 at 17:47):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/
Karl Palmskog (Sep 05 2022 at 17:47):ah, then someone should edit the release text to replace with this link here: https://github.com/coq/coq/releases/tag/V8.16.0
Théo Zimmermann (Sep 05 2022 at 17:48):I should also do the Zenodo release. I'll put this on my todo list.
Julien Puydt (Sep 06 2022 at 05:17):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:
Julien Puydt (Sep 06 2022 at 05:56):Here is the bug report asking for permission.
Michael Soegtrop (Sep 06 2022 at 06:36):@Julien Puydt : I will double check today if this matches the versions picked by the authors for Coq Platform.
Julien Puydt (Sep 06 2022 at 06:42):@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.
Karl Palmskog (Sep 06 2022 at 06:59):brace for CI impact: https://github.com/ocaml/opam-repository/pull/22066
Karl Palmskog (Sep 06 2022 at 08:13):you get a red CI flag if your reverse dependencies fail to work. That's a new one for me.
Guillaume Melquiond (Sep 06 2022 at 08:27):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.
Karl Palmskog (Sep 06 2022 at 08:29):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?
Guillaume Melquiond (Sep 06 2022 at 08:33):No, it just means that it is your job to fix the upper bounds.
Karl Palmskog (Sep 06 2022 at 08:34):of someone else's package? I can't control whether they put "my_stuff" {>= "1.0"}
Guillaume Melquiond (Sep 06 2022 at 08:35):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.
Karl Palmskog (Sep 06 2022 at 08:42):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
Karl Palmskog (Sep 06 2022 at 08:43):if we did that for the Coq opam archive, it would probably be more the job of maintainers and automation to edit bounds.
Guillaume Melquiond (Sep 06 2022 at 09:01):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..
Julien Puydt (Sep 06 2022 at 09:35):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...
Michael Soegtrop (Sep 06 2022 at 12:18):@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.
Michael Soegtrop (Sep 06 2022 at 16:39):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.
Karl Palmskog (Sep 06 2022 at 18:23):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.
Karl Palmskog (Sep 06 2022 at 18:25):any input on what the lower bound for lablgtk3-sourceview3 should be is appreciated...
Karl Palmskog (Sep 06 2022 at 18:57):looks like 3.1.2 is the minimum released version that works.
Pierre Roux (Sep 06 2022 at 19:48):That seems consistent with the first item there: https://coq.inria.fr/distrib/V8.16.0/refman/changes.html#id120
Karl Palmskog (Sep 06 2022 at 19:49):sigh, this was not synchronized with the Coq opam archive core-dev. I'll have to do some PRs.
Michael Soegtrop (Sep 07 2022 at 12:29):@Julien Puydt : I attached a CSV and readMe file which should be very close to the final release. beta.csv beta.md
Julien Puydt (Sep 07 2022 at 17:59):@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
Michael Soegtrop (Sep 07 2022 at 18:13):@Julien Puydt : please note that I plan the following updates:
Michael Soegtrop (Sep 07 2022 at 18:15):I will follow up on the packages where you are ahead with the authors.
One question: what does "+b1" mean?
Julien Puydt (Sep 07 2022 at 18:16):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>
Pierre Roux (Sep 07 2022 at 20:37):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.
Julien Puydt (Sep 08 2022 at 05:16):@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...
Pierre Roux (Sep 08 2022 at 06:39):Ok, so if I understand correctly, that's on Debian side and you don't need anything from Analysis developers.
Julien Puydt (Sep 08 2022 at 13:42):@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.
Karl Palmskog (Sep 09 2022 at 11:26):very nice to have 40+ packages compatible with 8.16 almost from day 0 of tagging. Probably a first in Coq history.
Enrico Tassi (Sep 09 2022 at 11:27):how many were done during the rc period?
Karl Palmskog (Sep 09 2022 at 11:29):hard to count exactly, but maybe 25-30 or so? cursory count of PRs
Karl Palmskog (Sep 09 2022 at 11:30):some things were also tagged during the rc period, but not packaged in released yet. Examples: UniCoq, Mtac2, CoqHammer
Enrico Tassi (Sep 09 2022 at 11:31):so 2/3 were done during rc. I think this is good, since that is what the rc period is for, really.
Karl Palmskog (Sep 09 2022 at 11:34):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.
Enrico Tassi (Sep 09 2022 at 11:35):I think it is already good, I just wanted to check that the rc period was not "wasted" as the beta one was...
Karl Palmskog (Sep 09 2022 at 11:36):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.
Karl Palmskog (Sep 09 2022 at 11:38):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
Karl Palmskog (Sep 09 2022 at 11:43):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
Enrico Tassi (Sep 09 2022 at 11:43):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.
Enrico Tassi (Sep 09 2022 at 11:44):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)
Pierre Roux (Sep 09 2022 at 12:51):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.
Michael Soegtrop (Sep 09 2022 at 15:05):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.
Michael Soegtrop (Sep 09 2022 at 15:08):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)
Michael Soegtrop (Sep 09 2022 at 15:10):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.
Karl Palmskog (Sep 09 2022 at 15:18):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.
Michael Soegtrop (Sep 09 2022 at 16:55):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.
Enrico Tassi (Sep 09 2022 at 20:43):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
Yannick Forster (Nov 07 2022 at 15:30):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? :)
Théo Zimmermann (Nov 07 2022 at 15:40):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.
Théo Zimmermann (Nov 11 2022 at 12:18):@Yannick Forster Done: https://zenodo.org/record/7313584
Last updated: Dec 06 2023 at 14:01 UTC