Karl Palmskog (Oct 14 2021 at 17:17): Karl Palmskog (Oct 14 2021 at 17:17):Will we see the Coq 8.14.0 opam packages merged in the next two weeks? Make your bets now!
opam-ci — Failed - 22 jobs failed, lint: ok, 47 jobs skipped, 265 jobs passed
What you mean @Karl Palmskog ?
Emilio Jesús Gallego Arias (Oct 14 2021 at 20:10):It is not fair for me to bet tho
Karl Palmskog (Oct 14 2021 at 20:10):to my knowledge, every opam package for the last few Coq releases has gotten stuck in the opam-repo CI for at least several days, and it's looking like the same thing is happening this time: https://github.com/ocaml/opam-repository/pull/19773
Emilio Jesús Gallego Arias (Oct 14 2021 at 20:21):The package is ready, will be merged in a few hours I understand
Emilio Jesús Gallego Arias (Oct 14 2021 at 21:57):I'm a bit puzzled tho about the stuck info, unless I'm missing something:
are we talking about the same thing @Karl Palmskog ?
Paolo Giarrusso (Oct 14 2021 at 23:59):https://github.com/ocaml/opam-repository/pull/17619 for 8.12.1 took longer, and I still remember that, but you're right that seems the exception
Paolo Giarrusso (Oct 15 2021 at 00:06):Aah, the real deal was https://github.com/ocaml/opam-repository/pull/15017, where we needed to improve packaging for quite a few deps; the scare survived for a while https://github.com/ocaml/opam-repository/pull/15119 https://github.com/ocaml/opam-repository/pull/15127.
Karl Palmskog (Oct 16 2021 at 09:25):merge was almost two days ago, but still the package doesn't appear on the opam archive web repo... Have they completely frozen the current web archive?
Erik Martin-Dorel (Oct 16 2021 at 11:27):Hi all, yes it looks like they have a deployment issue: coq.8.14.0 is not visible here https://opam.ocaml.org/packages/coq/
I experienced the same issue with the merge of learn-ocaml.0.13.0 one week ago, see this answer from the maintainers for details and a workaround: https://github.com/ocaml/opam-repository/pull/19698#issuecomment-942371247
Erik Martin-Dorel (Oct 16 2021 at 11:28):So for the moment it's not possible to easily push a new version of coqorg/coq:8.14 that bumps 8.14+rc1 → 8.14.0
(unless we decide to override the official URL of the opam default repository in coqorg/base with this git-pinning workaround…)
Karl Palmskog (Oct 16 2021 at 11:56):@Erik Martin-Dorel I really think we should wait until the opam-repository deployment issue is settled to update the Docker image. We want to transfer Bignums release for 8.14 to released and a bunch of other packages as well in a controlled way.
Karl Palmskog (Oct 16 2021 at 11:57):we could also put the SerAPI "pre-release" for 8.14 in the released repo once 8.14.0 is out as normal, but I'm not sure Emilio wants that.
Théo Zimmermann (Oct 16 2021 at 13:08):No, I think Emilio would rather do a proper official release for 8.14.0.
Karl Palmskog (Oct 16 2021 at 13:13):right, and as things are looking right now, the whole cycle of getting 8.14.0 deployed and then SerAPI released+merged+deployed might take 7+ days, even if the GitHub release of SerAPI happens shortly after 8.14.0 is out.
Karl Palmskog (Oct 16 2021 at 22:36):seems like they managed to deploy the opam web now.
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):We can do a SerAPI release when you want folks
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):only constraint was to get 8.14 in the opam archive
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):when would you like it?
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:47):I'm still using SerAPI 8.13 as the main dev branch due to some issues which I'd like to have fixed in 8.13 too, but no problem in doing an 8.14 release
Karl Palmskog (Oct 17 2021 at 19:57):please do the official 8.14 SerAPI release ASAP, in our current setup Érik can't create the Docker image with 8.14.0 without it. There is no emergency, but obviously nice to get the Docker image out so we can begin testing more widely with the Coq release.
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:10):Ok I'll try to release tomorrow then
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:10):I'm confused tho, why the core docker image needs SerAPI?
Karl Palmskog (Oct 17 2021 at 20:11):as has been discussed before, we want to use the Docker image to run Alectryon (many have requested this), and SerAPI and its deps are by far the most time-consuming requirement of Alectryon to build
Karl Palmskog (Oct 17 2021 at 20:13):if you port Alectryon to PyCoq, I'm sure we can ship PyCoq instead
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):So now the base coq Docker image includes Alectryon?
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):Ah, I didn't know
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):but that's gonna make for a quite heavy 8.14 image
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):I was under the impression the Coq Docker image included just Coq
Karl Palmskog (Oct 17 2021 at 20:15):the decision was made to only include SerAPI, and then Alectryon is near-instantaneous to install on top
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:16):then there were flavors such as the one with math-comp, etc... @Erik Martin-Dorel
Karl Palmskog (Oct 17 2021 at 20:16):the Docker-Coq image has included Coq, Dune, and Bignums for a long time
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:16):I was not aware, thanks for the info
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:16):seems a bit risky to me tho
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):Dune and bignums are core key components, also bignums used to be part of Coq
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):and it is tested on the CI
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):however SerAPI is still kinda experimental software, so I dunno, doesn't seem to me a good idea to tie the base Coq image to it
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):it is not even in the CI
Karl Palmskog (Oct 17 2021 at 20:18):https://github.com/coq-community/docker-coq/issues/32
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:18):for 8.14 we are good, but I mean, it is very possible that 8.15 we could have some problems
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:19):I see, ups
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:19):Will release tomorrow, but IMHO it'd be safer to have alectryon on top of the core layer
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:19):at least until one of PyCoq or SerAPI land in Coq's CI
Karl Palmskog (Oct 17 2021 at 20:20):Alectryon has done very frequent releases (several in August, IIRC), so makes sense to me to have it be installed manually on top. We don't want to have to update the Docker Coq image unless there is a new Coq release.
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:22):I mean the base image for Alectryon
Karl Palmskog (Oct 17 2021 at 20:25):even though Alectryon and its dependencies are experimental, they are for sure an important driver of Coq use right now. For example, we did a release of the Hydras & Co. book this Friday, which uses a "hybrid" approach between literate and non-literate documentation generation
Karl Palmskog (Oct 17 2021 at 20:26):also, Coq-Elpi is using Alectryon for its tutorials
Karl Palmskog (Oct 17 2021 at 20:28):did SerAPI and its deps really increase the fatness of the Coq-Docker image that much? I would expect a couple of tens of MB, not more.
Erik Martin-Dorel (Oct 17 2021 at 20:29):Emilio Jesús Gallego Arias said:
then there were flavors such as the one with math-comp, etc... Erik Martin-Dorel
thanks Emilio for the ping; actually @Karl Palmskog already recalled the whole context (related to the discussion that took place in https://github.com/coq-community/docker-coq/issues/32) so I believe I've nothing to add :sweat_smile:
Karl Palmskog (Oct 17 2021 at 20:30):OK, so I think what Emilio means is that his ideal would be to have Alectryon directly on top of Coq, i.e., the coq package as dep, nothing more. I think this is going to take many engineering hours to achieve, and may not be worth the effort.
Erik Martin-Dorel (Oct 17 2021 at 20:33):Karl Palmskog said:
did SerAPI and its deps really increase the fatness of the Coq-Docker image that much? I would expect a couple of tens of MB, not more.
Good question; I didn't measure this at the time but my impression was the same as yours: a thin increase regarding size, but a significant time saved if SerAPI is prebuilt "upstream" in Docker-Coq.
Anyway I'll post more details here if I happen to re-find precise figures on this later on.
Erik Martin-Dorel (Oct 17 2021 at 20:39):Emilio Jesús Gallego Arias said:
it is not even in the CI
OK I see what you mean, but I now recall a comment related to this, by @Théo Zimmermann (maybe on GitHub or Zulip, I don't remember)… to sum up:
coq-serapi is part of coqorg/coq:8.* stable images, but not part of coqorg/coq:dev Karl Palmskog (Oct 17 2021 at 20:42):I think our conclusion in the last discussion on the CI topic was that the pure serialization part of SerAPI would ideally be added to Coq itself, and the protocol part of SerAPI would ideally be added to the CI (once the serialization stuff is upstreamed). Then there are some additional components of the current SerAPI that could be split off and only depend on Coq+serializers (not the protocol): https://github.com/ejgallego/coq-serapi/issues/252
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:00):I mean that it would be more convenient to have a coq:serapi image on its own
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:00):I recall the discussion, but I didn't realize that you were talking about adding serapi to be _base_ image
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:01):that means that now SerAPI release calendar is effectively tied to that one of coq
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:01):that seems too constraining to me, even if there are quite a few people with serapi repos access
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:01):not sure we are ready to commit to that
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:01):I'd say it'd be normal for SerAPI for Coq 8.XX to release a few weeks after Coq 8.xx itslef
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:02):anyways for 8.14 that's not a problem
Erik Martin-Dorel (Oct 17 2021 at 21:14):OK I fully understand… indeed I think it would be possible to uncouple the two releases for Coq 8.15+, so coqorg/coq:8.15.0 can be published a few weeks before the bigger image with SerAPI is published, as you suggest. This would definitely feasible with the current infrastructure. I just guess we'll need to discuss together a few points to plan this, when the preparation of the 8.15 release will be started (to agree e.g. on the naming convention for the bigger image and on what to do for the release candidate image 8.15+rc1…)
Karl Palmskog (Oct 17 2021 at 21:15):but the whole idea of introducing release candidates and then wait a few weeks for stable release was meant to be the period when people could safely do tags of libraries
Karl Palmskog (Oct 17 2021 at 21:16):what's the point of the RC period if we still have to wait until several weeks after the stable release?
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):Actually you got a point Karl
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):indeed, the Docker image could use the rc tag for serapi
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):right?
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):that seems fine indeed
Karl Palmskog (Oct 17 2021 at 21:18):we can use the SerAPI 8.14 tag for the 8.14.0 Coq-Docker image, yes. But then we have to move the SerAPI tag 8.14 package to the released repo
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:18):Yeah, that's a limitation of the current setup I'm afraid
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:18):it doesn't consider that some packages want to be in the main opam repos
Karl Palmskog (Oct 17 2021 at 21:20):so @Emilio Jesús Gallego Arias do you approve moving this package to the released Coq opam repo?
Karl Palmskog (Oct 17 2021 at 21:22):our goal here is to get a Docker image with Alectryon, so either a regular OCaml opam release or the 8.14+rc release in released is fine by me
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:22):I think that indeed, if you want to have serapi in the base image, using the rc tag is fine
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:22):not needed for 8.14 tho
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:23):The thing is that serapi really wants to live in the main opam repos for many reasons
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:23):in particular, to ensure that the whole ppx layer doesn't break it
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:23):I want to run OPAM QA to run on serapi packages
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):BTW https://github.com/ocaml/opam-repository/pull/19799
Erik Martin-Dorel (Oct 17 2021 at 21:24):but would it have been better to add coq-serapi 8.14+rc1+0.14.0 in the default opam-repository in the first place?
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):I didn't solve the {pinned} problem yet, sorry Karl
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):@Erik Martin-Dorel that's not possible as it needs Coq 8.14 in the main repos then
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):so that's another pitfall of the central opam-repository
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:25):it doesn't really support for beta software
Karl Palmskog (Oct 17 2021 at 21:25):uh, what implications does the {pinned} problem have for us right now? I don't think it will affect Alectryon etc.?
Karl Palmskog (Oct 17 2021 at 21:26):anyway, since now Emilio did the release and the package, I think we should wait for that in the Docker-Coq 8.14 image.
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:27):@Karl Palmskog that problem can make opam CI fail, no implications other than delaying the merge a bit, but I'm hoping opam 2.1 solved this
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:27):will amend the opam file anyways
Erik Martin-Dorel (Oct 17 2021 at 21:29):OK I see… but maybe a "solution" of these various constraints would have been this? (although it is heavier, and I'm not sure this works because we end up with two almost-identical copies of the same package in extra-dev and in opam-repository…):
8.14+rc1+0.14.0 in extra-dev with a strong constraint that requires exactly coq 8.14+rc1 Emilio Jesús Gallego Arias (Oct 17 2021 at 21:30):@Erik Martin-Dorel , step 2 is not really necessary, doing a serapi release from the tag is pretty easy, @Karl Palmskog or any other contributor can do it, it is just a dune-release command
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:30):it will take care of everything
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:31):with the current setup we are basically releasing the tags chosen for the rc1 as the final 8.14 versions
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:33):that seems fine to me
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:33):for serapi too
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:34):Right now Théo, Karl, Anton, Armaël, Clément, and Jason have access to coq-serapi so we should be good, we can add more people too
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:35):So instead of doing the PRs on coq-opam-archive as you do moving the stuff to released, someone needs to do:
dune-release tag $version
dune-release
OK! So I've just prepared a Docker-Coq PR that will update coqorg/coq:8.14 when coq-serapi for 8.14 goes live in opam-repository: https://github.com/coq-community/docker-coq/pull/37
Erik Martin-Dorel (Oct 17 2021 at 21:39):Emilio Jesús Gallego Arias said:
So instead of doing the PRs on coq-opam-archive as you do moving the stuff to released, someone needs to do:
dune-release tag $version dune-release
:+1: Maybe one of you could document this in https://github.com/coq/coq/blob/master/dev/doc/release-process.md or somewhere else?
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:46):Yes I will document it, it is a fully standard setup for opam-repos
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:46):I will document it in the SerAPI contributing guide
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:52):https://github.com/ejgallego/coq-serapi/commit/94dc9ecde5d2a2c2915aa3e038bdcd0d71b8b949
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:52):that should do it
Emilio Jesús Gallego Arias (Oct 17 2021 at 21:54):I have a small minor drawback on how I forward port changes to 8.13 to 8.14 for example, but that is an internal thing and should not concern you folks doing Docker or Coq Platform
Emilio Jesús Gallego Arias (Oct 17 2021 at 22:00):regular CI for coq-serapi passed on the opam repos, however there is this new "lower bounds" CI which is going to be lots of fun XD
Emilio Jesús Gallego Arias (Oct 17 2021 at 22:01):I've doing some lower bounds testing myself [informally] let's see what this yields
Emilio Jesús Gallego Arias (Oct 17 2021 at 22:02):It passed it seems :grinning_face_with_smiling_eyes: that was a long shooot
Last updated: Sep 23 2023 at 07:01 UTC