Gaëtan Gilbert (Jan 13 2022 at 16:33): Gaëtan Gilbert (Jan 13 2022 at 16:33):for https://github.com/ocaml/opam-repository
Anyone up for doing this?
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)
Gaëtan Gilbert (Jan 13 2022 at 16:36):I didn't know that
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)
Karl Palmskog (Jan 13 2022 at 16:37):it's not a big deal to have the PR open, but just so you know
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?
Emilio Jesús Gallego Arias (Jan 13 2022 at 16:39):I won't sorry, not enough cycles
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
Emilio Jesús Gallego Arias (Jan 13 2022 at 16:41):if anyone wants to help
Karl Palmskog (Jan 13 2022 at 16:42):it automates the submission, sure, but it doesn't help when Alpine Linux on ARM32 fails
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
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.
Paolo Giarrusso (Jan 13 2022 at 18:17):thanks for the ping, no promises but I could do it before Sunday
Paolo Giarrusso (Jan 14 2022 at 01:24):On it, done the hard part https://github.com/coq/coq/pull/15050#issuecomment-1012665256
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]
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
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?
Karl Palmskog (Jan 14 2022 at 08:56):likely on purpose, since CoqIDE has a bad track record on the opam-repository CI
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.)
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
Karl Palmskog (Jan 14 2022 at 09:04):even in your link, there are 10+ failures for CoqIDE (mostly related to lablgtk)
Guillaume Melquiond (Jan 14 2022 at 09:05):Not "mostly", only. There isn't a single failure for Coqide itself.
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
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.
Karl Palmskog (Jan 14 2022 at 09:10):are you saying they will merge even when no CI job will succeed?
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)
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.
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).
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.
Guillaume Melquiond (Jan 14 2022 at 09:19):Did you miss the part where I said that 90% of the Coqide jobs succeeded?
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"
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)
Gaëtan Gilbert (Jan 14 2022 at 12:01):I guess if they're just warnings it doesn't matter
Paolo Giarrusso (Jan 14 2022 at 12:47):Anyway, this MR was merged, they blamed even the OOM on cluster problems
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
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?
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.
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...
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
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
Matthieu Sozeau (Jan 14 2022 at 14:32):First time in history we've been asked to release less often, I believe :)
Matthieu Sozeau (Jan 14 2022 at 14:33):But seriously. I agree
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?
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
Théo Zimmermann (Jan 14 2022 at 14:53):Yes, that's precisely my point.
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).
Karl Palmskog (Jan 14 2022 at 14:55):even if you have dune-release, what about all ecosystem projects and the Platform?
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)
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.
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.
Théo Zimmermann (Jan 14 2022 at 14:59):And it is not justified by anything rational.
Karl Palmskog (Jan 14 2022 at 14:59):OK, but consider major releases then, it was just three months since 8.14.0
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.
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
Théo Zimmermann (Jan 14 2022 at 15:01):That sounds pretty reasonable to me then.
Karl Palmskog (Jan 14 2022 at 15:02):coq.8.15.0 shows up using opam update now, for the record.
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.
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
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.
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.
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
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
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?
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.
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.
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 .
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.
Paolo Giarrusso (Jan 15 2022 at 22:23):(that tag is just the head of https://github.com/ejgallego/coq-serapi/pull/265)
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
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
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 :-)
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
Karl Palmskog (Jan 15 2022 at 22:56):just documenting a release process would be nice (maybe joint for Bignums, Docker images)
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 :-)
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.
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
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:
And there are also additional info in the CEP 52:
https://github.com/coq/ceps/blob/master/text/052-platform-release-cycle.md
Erik Martin-Dorel (Jan 16 2022 at 13:34):Anyway, maybe these two documents may need a few minor updates? ↓
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.
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.
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).
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)?
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.
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)
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".
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.
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)
Karl Palmskog (Jan 16 2022 at 13:56):one option is to do new CEPXX which is a refinement of CEP52
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.
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.
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:
Erik Martin-Dorel (Jan 16 2022 at 14:05):WDYT?
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
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
Karl Palmskog (Jan 16 2022 at 14:10):could also be in the Coq Platform repo I guess
Erik Martin-Dorel (Jan 16 2022 at 14:10):Hmm… I'm not sure for the Coq platform repo
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?
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
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: Oct 13 2024 at 01:02 UTC