Stream: Coq users

Topic: opam-repository CI fail


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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 20:09):

What you mean @Karl Palmskog ?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 20:10):

It is not fair for me to bet tho

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 20:21):

The package is ready, will be merged in a few hours I understand

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

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

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Oct 16 2021 at 13:08):

No, I think Emilio would rather do a proper official release for 8.14.0.

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

view this post on Zulip Karl Palmskog (Oct 16 2021 at 22:36):

seems like they managed to deploy the opam web now.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):

We can do a SerAPI release when you want folks

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):

only constraint was to get 8.14 in the opam archive

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 19:46):

when would you like it?

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:10):

Ok I'll try to release tomorrow then

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:10):

I'm confused tho, why the core docker image needs SerAPI?

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

view this post on Zulip Karl Palmskog (Oct 17 2021 at 20:13):

if you port Alectryon to PyCoq, I'm sure we can ship PyCoq instead

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):

So now the base coq Docker image includes Alectryon?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):

Ah, I didn't know

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):

but that's gonna make for a quite heavy 8.14 image

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:15):

I was under the impression the Coq Docker image included just Coq

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

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

view this post on Zulip Karl Palmskog (Oct 17 2021 at 20:16):

the Docker-Coq image has included Coq, Dune, and Bignums for a long time

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:16):

I was not aware, thanks for the info

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:16):

seems a bit risky to me tho

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):

and it is tested on the CI

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:17):

it is not even in the CI

view this post on Zulip Karl Palmskog (Oct 17 2021 at 20:18):

https://github.com/coq-community/docker-coq/issues/32

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:19):

I see, ups

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:19):

at least until one of PyCoq or SerAPI land in Coq's CI

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:22):

I mean the base image for Alectryon

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

view this post on Zulip Karl Palmskog (Oct 17 2021 at 20:26):

also, Coq-Elpi is using Alectryon for its tutorials

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:01):

not sure we are ready to commit to that

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:02):

anyways for 8.14 that's not a problem

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):

Actually you got a point Karl

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):

indeed, the Docker image could use the rc tag for serapi

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):

right?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:17):

that seems fine indeed

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:18):

Yeah, that's a limitation of the current setup I'm afraid

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

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

https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-serapi/coq-serapi.8.14%2Brc1%2B0.14.0/opam

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:22):

not needed for 8.14 tho

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:23):

in particular, to ensure that the whole ppx layer doesn't break it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:23):

I want to run OPAM QA to run on serapi packages

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):

BTW https://github.com/ocaml/opam-repository/pull/19799

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):

I didn't solve the {pinned} problem yet, sorry Karl

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:24):

so that's another pitfall of the central opam-repository

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:25):

it doesn't really support for beta software

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:27):

will amend the opam file anyways

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:30):

it will take care of everything

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:33):

that seems fine to me

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:33):

for serapi too

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

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

view this post on Zulip Erik Martin-Dorel (Oct 17 2021 at 21:37):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:46):

I will document it in the SerAPI contributing guide

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:52):

https://github.com/ejgallego/coq-serapi/commit/94dc9ecde5d2a2c2915aa3e038bdcd0d71b8b949

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 21:52):

that should do it

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

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

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

view this post on Zulip 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: Mar 29 2024 at 11:01 UTC