Stream: Coq devs & plugin devs

Topic: opam package for 8.15.0


view this post on Zulip Gaëtan Gilbert (Jan 13 2022 at 16:33):

for https://github.com/ocaml/opam-repository
Anyone up for doing this?

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:35):

I'm not up for it (can take anything from 1-3 days). But note that we can't merge the following PR until coq.8.15.0 is in opam-repository: https://github.com/coq/opam-coq-archive/pull/2029

So I don't understand why that PR was opened (now it will have to stay open for 1-3 days)

view this post on Zulip Gaëtan Gilbert (Jan 13 2022 at 16:36):

I didn't know that

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:37):

OK, the basic problem is that bignums only works with one version of Coq, and the released opam repo only assumes the Coq versions from opam-repository (at least by default)

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:37):

it's not a big deal to have the PR open, but just so you know

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:39):

ping @Emilio Jesús Gallego Arias @Paolo Giarrusso who have more resilience than I do in working with the opam-respository CI, maybe you could submit the coq.8.15.0 package?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 13 2022 at 16:39):

I won't sorry, not enough cycles

view this post on Zulip Emilio Jesús Gallego Arias (Jan 13 2022 at 16:41):

Note that dune-release could be used to automate this, but some more work is needed to polish and fix a few remaining issues

view this post on Zulip Emilio Jesús Gallego Arias (Jan 13 2022 at 16:41):

if anyone wants to help

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:42):

it automates the submission, sure, but it doesn't help when Alpine Linux on ARM32 fails

view this post on Zulip Karl Palmskog (Jan 13 2022 at 16:43):

OK if nobody picks it up by Sunday, I will bite the bullet and do the PR

view this post on Zulip Théo Zimmermann (Jan 13 2022 at 16:43):

@Ralf Jung also used to take care of this, before some other people got motivated and did it faster than he could.

view this post on Zulip Paolo Giarrusso (Jan 13 2022 at 18:17):

thanks for the ping, no promises but I could do it before Sunday

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 01:24):

On it, done the hard part https://github.com/coq/coq/pull/15050#issuecomment-1012665256

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 05:21):

well, the first hard part; and submitted https://github.com/ocaml/opam-repository/pull/20448.

Anybody knows if all those warnings in https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/fe35af70d269337e99d444fe9e597dde7dbe8d1a/variant/opam-2.0,distributions,ubuntu-18.04,coq.8.15.0 are normal?

- Warning: Cannot open directory _build_vo/default//lib/coq/../coq-core/plugins
- [cannot-open-dir,filesystem]

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 07:14):

No, that does not ring a bell. And the "out of memory" and "cancelled" (i.e., "timeout") messages are especially worrying. Coq 8.14 was looking a lot better: https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/2e6c9940b183bdc86ccbc1fec12ed7dd510fb5d1

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 07:40):

By the way, I notice that you did not submit coqide as part of your pull request. Is that on purpose?

view this post on Zulip Karl Palmskog (Jan 14 2022 at 08:56):

likely on purpose, since CoqIDE has a bad track record on the opam-repository CI

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 09:01):

What do you mean? If you look at the link I put, you will see that Coq+Coqide 8.14 was looking quite good. (A lot better than Coq 8.15 actually.)

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:03):

from what I remember, CoqIDE has had CI failures in every package going back to Coq 8.9

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:04):

even in your link, there are 10+ failures for CoqIDE (mostly related to lablgtk)

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 09:05):

Not "mostly", only. There isn't a single failure for Coqide itself.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:06):

doesn't really matter if it's CoqIDE itself or its dependencies, PR can still get stuck

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 09:09):

Why would it get stuck? A failure to build a dependency has never been a cause for blocking a PR on the Opam repository.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:10):

are you saying they will merge even when no CI job will succeed?

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:10):

in any case, we'd rather get coq out as quickly as possible (since CoqIDE is not in the Docker images)

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 09:13):

Why do you say no CI job will succeed? For 8.14, 260 jobs succeeded out of 300. (And 114 out of 130 for Coq 8.13.) So, 90% success is good enough, especially since all the failures happen in packages unrelated to the pull request.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:18):

if they really will consistently merge a package whose dependencies fail, then I should be able to submit and get merged a package that doesn't build at all (since it's only the deps that fail).

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:19):

Otherwise, I would prefer submitting packages that have as few fails as possible (either due to deps or for other reasons). CoqIDE is much lower priority to get out, since only a portion of Coq users actually use it.

view this post on Zulip Guillaume Melquiond (Jan 14 2022 at 09:19):

Did you miss the part where I said that 90% of the Coqide jobs succeeded?

view this post on Zulip Karl Palmskog (Jan 14 2022 at 09:23):

if the Coq package has lower percentage than that, I'd still submit it separately, so I don't have to monitor hundreds of jobs and see if I pass some "threshold"

view this post on Zulip Gaëtan Gilbert (Jan 14 2022 at 12:01):

Anybody knows if all those warnings in https://opam.ci.ocaml.org/github/ocaml/opam-repository/commit/fe35af70d269337e99d444fe9e597dde7dbe8d1a/variant/opam-2.0,distributions,ubuntu-18.04,coq.8.15.0 are normal?

no
no idea why we don't get them in our CI, they can be reproduced with ./configure -prefix /usr; make on my machine (we do use configure -prefix in CI)

view this post on Zulip Gaëtan Gilbert (Jan 14 2022 at 12:01):

I guess if they're just warnings it doesn't matter

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 12:47):

Anyway, this MR was merged, they blamed even the OOM on cluster problems

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 12:49):

@Guillaume Melquiond I meant to send coqide separately, I certainly remember what @Karl Palmskog describes happened at least once

view this post on Zulip Karl Palmskog (Jan 14 2022 at 13:25):

@Emilio Jesús Gallego Arias now that coq.8.15.0 is merged (and will appear in some number of hours via opam update), should there be a 8.15.0+0.15.0 release of SerAPI? Or as an alternative, should we move 8.15+rc1+0.15.0 to the released Coq opam repo and use that in the Docker images?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 14 2022 at 13:38):

@Karl Palmskog what makes more sense? I was not expecting the opam package to appear today, but I can cook a quick release today or tomorrow.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 13:46):

A proper release of 8.15.0+0.15.0 tomorrow is the best option (and then coq.8.15.0 is near-guaranteed to have appeared via opam update). Going with the rc1 release was the backup option if you were busy...

view this post on Zulip Emilio Jesús Gallego Arias (Jan 14 2022 at 13:48):

Ok, will push a release as soon as SerAPI CI's can pick the 8.15 opam package

view this post on Zulip Karl Palmskog (Jan 14 2022 at 13:49):

to be honest I wish there was a minimum time (lower bound) between Coq point major releases of something like 4 months

view this post on Zulip Matthieu Sozeau (Jan 14 2022 at 14:32):

First time in history we've been asked to release less often, I believe :)

view this post on Zulip Matthieu Sozeau (Jan 14 2022 at 14:33):

But seriously. I agree

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:51):

That's because there's still too much friction with each release, right? This just means that we have failed at streamlining releases like we wanted. If we had finished things like the Dune migration and that Coq's RM could just run dune-release, there would be no reason to release less often, right?

view this post on Zulip Karl Palmskog (Jan 14 2022 at 14:53):

my view is that each Coq release takes chunks of people's time (not just Coq devs, but ecosystem/stakeholder), and if one release comes quickly after another one, then you will occupy more of everyone's time within a timeframe than what is feasible/reasonable

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:53):

Yes, that's precisely my point.

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:54):

Release often is a motto that you can only apply if releasing is cheap (for everyone).

view this post on Zulip Karl Palmskog (Jan 14 2022 at 14:55):

even if you have dune-release, what about all ecosystem projects and the Platform?

view this post on Zulip Karl Palmskog (Jan 14 2022 at 14:56):

we were just discussing in the MathComp fortnightly meeting how the MathComp ecosystem should handle Coq releases and the Platform. It's not a simple tooling issue there, but nontrivial decisions need to be made (about what and when to release)

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:58):

You are talking about point releases here. In principle, maintainers of Coq packages should have zero work when there is a new point release.

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:58):

The fact that SerAPI is explicit about the Coq point release (and thus requires a different rc and final release) is an anomaly IMHO.

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 14:59):

And it is not justified by anything rational.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 14:59):

OK, but consider major releases then, it was just three months since 8.14.0

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 15:00):

it was just three months since 8.14.0

This was an exceptional decision to account for an exceptional situation (the previous release had been significantly delayed). If you think this was a bad idea, then we could decide to not reiterate if this situation happens again.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 15:01):

yes, you can read the above as arguing for that there should be a minimum of 4 months between 8.X.0 and 8.X+1.0

view this post on Zulip Théo Zimmermann (Jan 14 2022 at 15:01):

That sounds pretty reasonable to me then.

view this post on Zulip Karl Palmskog (Jan 14 2022 at 15:02):

coq.8.15.0 shows up using opam update now, for the record.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 14 2022 at 15:33):

The fact that SerAPI is explicit about the Coq point release (and thus requires a different rc and final release) is an anomaly IMHO.

It doesn't, the problem is that SerAPI lives in the main opam repository [which is the right place for it], and Coq rcs don't.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 14 2022 at 15:35):

Regarding the release process, I agree that it is not only a tooling problem, but for a starter we should fix our tooling problem which has lots of room to improve

view this post on Zulip Ralf Jung (Jan 14 2022 at 18:52):

Karl Palmskog said:

yes, you can read the above as arguing for that there should be a minimum of 4 months between 8.X.0 and 8.X+1.0

yeah I tend to agree -- there's a lot of bumping of dependencies and adjusting of CI configs happening in iris land for each major Coq release, and things like fixing or disabling whatever new warnings show up etc. this all adds up over around a dozen repositories.

view this post on Zulip Enrico Tassi (Jan 14 2022 at 19:23):

Théo Zimmermann said:

That's because there's still too much friction with each release, right? This just means that we have failed at streamlining releases like we wanted. If we had finished things like the Dune migration and that Coq's RM could just run dune-release, there would be no reason to release less often, right?

It is the ratio between friction and gain because of higher frequency which is unclear to me. If the gain is little, friction is always going to be too important.

view this post on Zulip Paolo Giarrusso (Jan 14 2022 at 20:23):

The gain is that we got the cool 8.15 bugfixes earlier, and IIUC it was still 6 months worth of bugfixes despite the delay... OTOH, in my company we'll probably end up skipping 8.14 altogether

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 00:42):

Now available: CoqIDE https://github.com/ocaml/opam-repository/pull/20456 and a new bug for it https://github.com/coq/coq/issues/15486

view this post on Zulip Enrico Tassi (Jan 15 2022 at 08:46):

Paolo Giarrusso said:

OTOH, in my company we'll probably end up skipping 8.14 altogether

That is kind of my point, if users end up skipping releases... can you elaborate why this may happen? No platform? No time? Blocking bug? Internal yearly cycle?

view this post on Zulip Théo Zimmermann (Jan 15 2022 at 09:13):

Enrico Tassi said:

Théo Zimmermann said:

That's because there's still too much friction with each release, right? This just means that we have failed at streamlining releases like we wanted. If we had finished things like the Dune migration and that Coq's RM could just run dune-release, there would be no reason to release less often, right?

It is the ratio between friction and gain because of higher frequency which is unclear to me. If the gain is little, friction is always going to be too important.

Here I was talking about bug fixes releases.

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 21:34):

can you elaborate why this may happen? No platform? No time? Blocking bug? Internal yearly cycle?

I imagine all of that "may" happen — from my POV, we knew the next release would come in 3 months, and internal updates have a nontrivial fixed cost.

view this post on Zulip Erik Martin-Dorel (Jan 15 2022 at 21:58):

Hi all! I've just seen this Zulip topic (BTW feel free to ping me as soon as the first PR is opened in the opam-repository :)

Thanks @Gaëtan Gilbert and @Karl Palmskog for taking care of https://github.com/coq/opam-coq-archive/pull/2029 for bignums.

As soon as the coq-serapi release for coq.8.15.0 will be in https://opam.ocaml.org/packages/coq-serapi/ ,
I'll merge the docker-coq PR that I've prepared: https://github.com/coq-community/docker-coq/pull/43 .

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 22:22):

@Emilio Jesús Gallego Arias since @Erik Martin-Dorel asked for the serapi package, I'm preparing the MR for the coq-serapi package (I'll check with you before merge), but you'll have to push the tag https://github.com/Blaisorblade/coq-serapi/tree/8.15.0+0.15.0 to your repo. I confirmed your code passes tests here just fine.

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 22:23):

(that tag is just the head of https://github.com/ejgallego/coq-serapi/pull/265)

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 22:39):

hm okay maybe not, looking at the dune-release workflow I might get in the way; I got as far as dune-release opam pkg but I'm not sure I can actually help

view this post on Zulip Emilio Jesús Gallego Arias (Jan 15 2022 at 22:48):

@Paolo Giarrusso thanks for the help, but I had actually tagged locally, the CI hadn't completed on time thus the reason I didn't manage to merge yesteday. Regarding the dune release workflow, if you have the correct setup as for the git repos upstream, a single dune-release invokation does work fine for SerAPI

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 22:49):

yeah but I realized it's quicker for you to do it yourself than to check what I did thanks to dune-release :-)

view this post on Zulip Karl Palmskog (Jan 15 2022 at 22:53):

as I learned several years ago, the rest of us have orders of magnitude less productivity when it comes to SerAPI than Emilio, e.g., something that takes him 1 min might take me 1 hour. So I always double check when doing something. With that said, I think we could work on better release automation at the Hackathon

view this post on Zulip Karl Palmskog (Jan 15 2022 at 22:56):

just documenting a release process would be nice (maybe joint for Bignums, Docker images)

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 22:57):

sorry for the noise, it was just 5 extra minutes so I was fine with throwing that away if I did something wrong :-). Overall I got 4/5 such packaging MRs in this weekend :-)

view this post on Zulip Paolo Giarrusso (Jan 15 2022 at 23:00):

@Enrico Tassi since you ask re the platform, I don't literally use the platform at work yet, but all the existing maintenance means I must mostly merge existing opam files and open MRs; at most, I resync packages across released/extra-dev/upstream.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 11:53):

@Erik Martin-Dorel coq-serapi.8.15.0+0.15.0 is now out on the general opam archive, so you should have all you need for the 8.15.0-based Docker image now

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 13:34):

Karl Palmskog said:

just documenting a release process would be nice (maybe joint for Bignums, Docker images)

Just to mention, the release process is supposed to be already documented here:

https://github.com/coq/coq/blob/master/dev/doc/release-process.md#for-each-release-preview-final-patch-level

And there are also additional info in the CEP 52:

https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 13:34):

Anyway, maybe these two documents may need a few minor updates? ↓

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:34):

sure, the Coq release process is documented, but the Docker images, Bignums, and SerAPI are ecosystem projects.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:35):

and the Coq opam archive (and the general one) is in my view distinct from Coq itself as well and part of the ecosystem.

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 13:36):

Yes (albeit docker-coq is already mentioned in the coq release-process.md document, only coq-serapi is missing there).

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 13:36):

Anyway, would you be fine with the assumption to document everything in the CEP 52 (opening PRs to refine it)?

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:38):

hmm, I thought CEPs were standalone, one-off things? This would be expanding its scope quite a bit.

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 13:38):

Maybe… I don't know actually (Cc-ing @Théo Zimmermann in case he has a sharper viewpoint on this)

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:39):

it would be helpful to document how we handle opam packages in extra-dev during the rc1 phase. For example, if someone opens a PR that only supports rc1, and 8.X.0 is not out, it can't go in released, but we will put it in a "move later list".

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:43):

since Bignums is now an ecosystem project, I think it should not be handled in any way by the Coq RM. We have plenty of people who can set the tag and so on.

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:53):

there is also the extremely open task of relaxing opam package bounds once 8.X.0 is out (I generally do this at least for mathcomp core packages during the rc1 phase, but due to the CI setup, we don't test it properly, since those packages live in released)

view this post on Zulip Karl Palmskog (Jan 16 2022 at 13:56):

one option is to do new CEPXX which is a refinement of CEP52

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:01):

AFAIK, the two advantages of preparing a CEP vs. a mere wiki are that it was possible to discuss each line added, thanks to a PR discussion…
and that afterwards, it is easy to "name" the CEP with a number to refer people to this reference.

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:01):

But if we don't update them after the discussion converged, they can rust / become obsolete.
(Which can be totally fine for CEPs that are just "major discussions not possible in a Coq issue")
And there is the concern that CEPs can only be merged by the Coq dev team.

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:01):

So I wouldn't want to suggest that we always update the CEPs… which is more work, and maybe not the intended initial goal. Instead:

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:05):

WDYT?

view this post on Zulip Karl Palmskog (Jan 16 2022 at 14:07):

yeah, what we are trying to do is essentially build a contract-like living process document which includes multiple parties, not just Coq devs

view this post on Zulip Karl Palmskog (Jan 16 2022 at 14:08):

maybe a Markdown file in a separate repo in the coq-community org could work, wiki is more shaky due to lack of change management

view this post on Zulip Karl Palmskog (Jan 16 2022 at 14:10):

could also be in the Coq Platform repo I guess

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:10):

Hmm… I'm not sure for the Coq platform repo

view this post on Zulip Erik Martin-Dorel (Jan 16 2022 at 14:10):

But indeed, I think it would be worth it to also have the opinion of the whole Coq dev team on these ideas (related to the CEPs and to the need for some "contract-like living process documents", to borrow your term), maybe discussing this during a Coq call?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2022 at 19:49):

Something I managed with SerAPI is that the release process is 100% standard dune-release, so the general documentation still works for it

view this post on Zulip Emilio Jesús Gallego Arias (Jan 16 2022 at 19:50):

I am not sure what the status is for regular Coq packages


Last updated: Feb 06 2023 at 19:03 UTC