Stream: Coq devs & plugin devs

Topic: 8.16.0 released


view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:44):

Hi all, V8.16.0 has just been tagged.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:46):

This includes, but is not limited to:

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:46):

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:46):

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:47):

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:47):

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 11:48):

@Karl Palmskog thanks, I'll tick out that item on the list

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 05 2022 at 11:48):

@Julien Puydt maybe https://github.com/lukaszcz/coqhammer/releases/tag/v1.3.2%2B8.16 ?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julien Puydt (Sep 05 2022 at 12:30):

I did ask: https://github.com/lukaszcz/coqhammer/issues/143

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2022 at 12:58):

I assume somebody has to write a release post or something as well?

view this post on Zulip Karl Palmskog (Sep 05 2022 at 13:20):

hmm, isn't this only for the Platform release?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 05 2022 at 13:24):

then according to CEP 52, I think that's it? I could be wrong.

view this post on Zulip Karl Palmskog (Sep 05 2022 at 13:25):

the Platform release post is a different beast and works on a different level and schedule.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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/

view this post on Zulip Théo Zimmermann (Sep 05 2022 at 17:47):

Pierre-Marie Pédrot said:

Done: https://coq.inria.fr/refman/

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Sep 05 2022 at 17:48):

I should also do the Zenodo release. I'll put this on my todo list.

view this post on Zulip 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:

view this post on Zulip Julien Puydt (Sep 06 2022 at 05:56):

Here is the bug report asking for permission.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 06 2022 at 06:59):

brace for CI impact: https://github.com/ocaml/opam-repository/pull/22066

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Sep 06 2022 at 08:33):

No, it just means that it is your job to fix the upper bounds.

view this post on Zulip Karl Palmskog (Sep 06 2022 at 08:34):

of someone else's package? I can't control whether they put "my_stuff" {>= "1.0"}

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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..

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Sep 06 2022 at 18:25):

any input on what the lower bound for lablgtk3-sourceview3 should be is appreciated...

view this post on Zulip Karl Palmskog (Sep 06 2022 at 18:57):

looks like 3.1.2 is the minimum released version that works.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 18:13):

@Julien Puydt : please note that I plan the following updates:

view this post on Zulip 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?

view this post on Zulip 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>

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Sep 09 2022 at 11:27):

how many were done during the rc period?

view this post on Zulip Karl Palmskog (Sep 09 2022 at 11:29):

hard to count exactly, but maybe 25-30 or so? cursory count of PRs

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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? :)

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 11 2022 at 12:18):

@Yannick Forster Done: https://zenodo.org/record/7313584


Last updated: Feb 02 2023 at 13:03 UTC