Stream: Coq devs & plugin devs

Topic: Coq 8.15 RC1


view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 13:53):

Who will do the bignums release for 8.15?

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 13:58):

should I do a github release for the rc?

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:00):

yes, the idea now is that releases are done for "core" Coq projects once Coq reaches rc stage

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:03):

but we should first have the RC1 release in the Coq opam archive (extra-dev part)

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 14:23):

why?

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:25):

that's how the process has been done so far, and it means we can test rc-related packages properly in the opam archive (and by extension in the Coq platform)

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 14:26):

I don't see any rcs in https://github.com/coq/coq/releases
did they get deleted?

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:26):

if we can't test them [Coq packages for an RC] there [in the extra-dev Coq opam archive], then errors will be discovered much later for the RM

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:27):

apparently 8.14 rc1 release was deleted on GitHub (or was never marked as a GitHub release), but tag is still there at least: https://github.com/coq/coq/releases/tag/V8.14%2Brc1

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:27):

please create and keep the GitHub releases of release candidates

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 14:30):

I still don't understand what the github release has to do with opam
rc1 is already tagged, if there are problems that just means we get a rc2

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:33):

as a Coq opam archive maintainer, I ask that RMs commission someone to submit an opam package to extra-dev for an RC as soon as it is tagged.

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:33):

otherwise, we can't even begin doing testing for the Coq platform, which is what the whole RC process is meant to be about

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:37):

also, the whole point of doing a release or tag on GitHub for bignums is to enable creation of an opam package, as far as the Coq Platform is concerned

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:39):

also, let's be clear that I don't consider it an RM duty to do any opam packaging. Just give us a shout here or on the Platform stream and people can do it

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 14:40):

I'm not doing bignums but I did https://github.com/coq/opam-coq-archive/pull/1974/files

view this post on Zulip Karl Palmskog (Dec 07 2021 at 14:43):

thanks

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:02):

Guillaume was the first RM with the RC based release schedule. He didn't do a GitHub release for 8.14+rc1 but he also didn't do one for 8.14.1. IMHO, while it's somewhat OK to do just a tag for the RC (although this is kind of the point of GitHub "prereleases"), skipping a GitHub release for 8.14.1 was a mistake.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:02):

That being said, there is indeed no relation between the GitHub release and the opam release.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 15:38):

I see that you have published the prerelease. I suggest that you repeat the information from your Coqdev / Discourse post (The 8.15 release will not have any more changes other than bug fixes with low compatibility impact.)

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 15:43):

Théo Zimmermann said:

Guillaume was the first RM with the RC based release schedule. He didn't do a GitHub release for 8.14+rc1 but he also didn't do one for 8.14.1. IMHO, while it's somewhat OK to do just a tag for the RC (although this is kind of the point of GitHub "prereleases"), skipping a GitHub release for 8.14.1 was a mistake.

Sorry about that. I guess I was confused about the difference between tags and releases. In fact, I would not be surprised if the only reason there is an actual 8.14.0 release is because I had to attach the reference manual to the tag, thus causing a release. I will make a release for 8.14.1.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 16:24):

Thanks!

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 16:24):

BTW, I think we should also attach the PDF to the 8.14.1 release.

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:24):

Unfortunately, the job artifact would have expired by now. Would it have not?

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:30):

Good news. It did not expire.

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:46):

Unfortunately, GitHub times out before the file is successfully added to the release assets. I wonder if we are really meant to attach such huge files.

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:52):

"Something went really wrong, and we can’t process that file."
So, no reference manual for 8.14.1.

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 16:52):

I can try to do the upload if you give me the link to the PDF artifact on GitLab.

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 16:53):

it attached fine for 15rc1

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 16:55):

https://gitlab.com/coq/coq/-/jobs/1801642479/artifacts/download

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 17:15):

Done. I think it works better when you have a good bandwidth.

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 17:18):

I am on the 10GB backbone, so it cannot get any better than that...

view this post on Zulip Guillaume Melquiond (Dec 07 2021 at 17:19):

(And I did try several times, they all ended with "something went terribly wrong".)

view this post on Zulip Théo Zimmermann (Dec 07 2021 at 17:19):

Weird

view this post on Zulip Gaëtan Gilbert (Dec 07 2021 at 17:23):

I had that until I unblocked some github domain which appeared in umatrix

view this post on Zulip Karl Palmskog (Dec 08 2021 at 13:18):

@Gaëtan Gilbert did you still plan to do a (8.15+rc1 tested) release of bignums on GitHub? I could take care of the opam package and related PR to opam archive if you do.

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 13:20):

sure I can do it

view this post on Zulip Karl Palmskog (Dec 08 2021 at 13:22):

thanks. For some context, bignums is a required part of the Docker images that we use heavily to test many Coq platform projects. We hope to set up 8.15 Docker images soon.

view this post on Zulip Gaëtan Gilbert (Dec 08 2021 at 13:23):

done

view this post on Zulip Matthieu Sozeau (Dec 10 2021 at 19:31):

@Karl Palmskog you might want to announce that, at least I'm waiting for it for equations's and metacoq's CI

view this post on Zulip Karl Palmskog (Dec 10 2021 at 20:46):

for the Docker images for 8.15+rc1 to come out, we need Emilio to do a pre-release (at least git tag) of SerAPI and Erik to run his scripts to set up the Docker Hub tag(s)

view this post on Zulip Karl Palmskog (Dec 10 2021 at 20:51):

@Emilio Jesús Gallego Arias any chance of a 8.15+rc1+0.15.0 SerAPI git tag for the Docker images in the near future?

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

Sure will do asap

view this post on Zulip Karl Palmskog (Dec 10 2021 at 20:55):

if you ping me somehow, I can/will take care of the opam package (in extra-dev)

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

Noted, thanks

view this post on Zulip Karl Palmskog (Dec 10 2021 at 20:57):

I think we have some happy users of Alectryon in CI, but probably this Docker image functionality should be advertised more widely ("here's how to deploy Alectryon proof movies to GitHub pages using Docker actions, for each commit to master")

view this post on Zulip Fabian Kunze (Dec 13 2021 at 15:58):

Is the plan to release 8.15 this year?

view this post on Zulip Gaëtan Gilbert (Dec 13 2021 at 16:12):

https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.15

view this post on Zulip Karl Palmskog (Dec 15 2021 at 15:36):

we should have everything ready for 8.15 Docker images now, including for MathComp 8.15 Docker images with 1.13.0. In particular SerAPI 0.15.0

view this post on Zulip Matthieu Sozeau (Dec 15 2021 at 15:47):

We discussed at the Coq Call the problem of syncing the docker images with releases of new packages for new branches. It seems it would be useful to have a base image with just the Coq release and another with additional packages, that would make the transition of CIs for projects like equations simpler, and putting less pressure the day after the rc release on preparing all packages.

view this post on Zulip Théo Zimmermann (Dec 16 2021 at 09:50):

Until recently, Bignums was the only additional package in the Docker image, and now @Erik Martin-Dorel, who takes care of preparing the Docker images, is also officially a maintainer of Bignums. So I don't think that this one is such a problem.

view this post on Zulip Théo Zimmermann (Dec 16 2021 at 09:50):

The only other package that we've added since is SerAPI, and indeed, this one might have been a mistake (for the base image).

view this post on Zulip Karl Palmskog (Dec 16 2021 at 09:57):

I think the argument for having SerAPI is clear - it takes significant time to install its dependencies, and it's a prerequisite of Alectryon which many people want to use (and depend on in CI). Nevertheless, I'm open to revisiting the decision of including SerAPI, if that's what Emilio and Erik think we should do.

view this post on Zulip Théo Zimmermann (Dec 16 2021 at 09:59):

My point is not that providing a Docker image with SerAPI is bad, but that delaying the Docker image that everyone needs to get their CI going because of SerAPI is bad.

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 12:04):

is there a nice workflow for checking for PRs to backport which were put in the 8.14.2 milestone? considering they don't appear in the 8.15 project

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

8.14.2 PRs are automatically added to the Coq 8.15 project in principle.

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

Indeed, all the merged PRs in this milestone were backported already, except #14967 because it was merged before the v8.15 branch.

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

It's not documented, but I had extended the project feature to be able to add PRs to multiple backport projects (see the 8.14.2 milestone description).

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 13:22):

Théo Zimmermann said:

Indeed, all the merged PRs in this milestone were backported already, except #14967 because it was merged before the v8.15 branch.

I did some manually though

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 13:22):

IIRC

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 13:22):

let's see how it goes with https://github.com/coq/coq/pull/15365

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

From the PR timeline, it seems like it is coqbot which added all of them to the project.

view this post on Zulip Matthieu Sozeau (Dec 16 2021 at 13:28):

Karl Palmskog said:

I think the argument for having SerAPI is clear - it takes significant time to install its dependencies, and it's a prerequisite of Alectryon which many people want to use (and depend on in CI). Nevertheless, I'm open to revisiting the decision of including SerAPI, if that's what Emilio and Erik think we should do.

I think Emilio's point is that SerAPI is not really production-ready yet and he's the only one able to update it to new Coq versions, so we should not expect it to be ready the day the rc is release, until we get to the point where SerAPI or something of similar functionality is integrated in Coq itself. Can't one easily make a bare-bones image with just the latest Coq and a more featre-full one with SerAPI?

view this post on Zulip Karl Palmskog (Dec 16 2021 at 13:30):

I don't generate the images, we need input from @Erik Martin-Dorel for that. But my view is that there will be an explosion of images if we want to split like that.

view this post on Zulip Karl Palmskog (Dec 16 2021 at 13:32):

if we want to screen out things "not production ready", I think the whole opam archive and tooling would disappear. Then we would need dedicated near-full-time CI people like the regular OCaml one. So to me "production ready" is not the right level to put the discussion at

view this post on Zulip Matthieu Sozeau (Dec 16 2021 at 15:36):

Forgive my wording, I guess "experimental" might be better. From what I gathered from what Emilio said, he considers SerAPI is an experiment.

view this post on Zulip Théo Zimmermann (Dec 16 2021 at 15:52):

The problem is that it is an experiment that has become successful. And the problem with success is that you become a liability to your users. Emilio has promoted the use of SerAPI instead of the XML protocol for many years (e.g., this was what he recommended to use, but did not end up being used, for the async branch of Proof General). Now that SerAPI is taking off, these problems appear.

view this post on Zulip Karl Palmskog (Dec 16 2021 at 15:54):

right, so I think there should be a serious discussion of how something experimental can at least be reliably released with the "same" functionality during an RC phase so Alectryon can continue to work...

view this post on Zulip Karl Palmskog (Dec 16 2021 at 16:10):

for example, I view coq-dpdgraph as largely experimental, but it's incredibly useful if you do some hacking on top to generate graphs and visualize projects. And it can reliably release in RC phase and so on.

view this post on Zulip Karl Palmskog (Dec 16 2021 at 16:12):

Emilio and I had a discussion about SerAPI components and how they could be maintained: https://github.com/ejgallego/coq-serapi/issues/252

But this requires longer-term planning.

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

Indeed the main problem we have with SerAPI is developer time, it is indeed experimental software, but the main problem comes from the platform, as it relies on a complex ppx chain. The discussion in the call was more about "why it is not in Coq's CI", and indeed, the reason has less to do with its "experimental nature", but more with:

So overall, you make the numbers, and adding SerAPI to the CI makes little gain for us.

Emilio has promoted the use of SerAPI instead of the XML protocol for many years (e.g., this was what he recommended to use, but did not end up being used, for the async branch of Proof General).

Indeed if we go back to history, this is a good example of bad planning [as we doing now with the "document manager", which similarly to the XML branch of PG, will eventually be scrapped] ; what we proposed there was a bit different: the XML protocol had critical problems, and SerAPI was designed from Clément advice when doing elcoq . What we proposed was to base the work on the new protocol, and then include it in Coq.

This is similar to what I suggested in https://github.com/ProofGeneral/PG/issues/619 , and indeed we could have merged a little language server in Coq around 2017 if we had followed this path; but this kind of development requires a flexiblity that we don't enjoy today in the dev structure.

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

Trying to get back to a more on-topic discussion, the first issue we want to address is "what do we allow Coq to depend on"

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

We have ppx, we also have a lot of libraries that modern proof systems require such as json, etc....

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

Until very recently we simply couldn't even use ppx easily as our build system didn't support it, now the situation has changed, but still significant work seems required to me

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

And unless I'm wrong, we lack the right expertise/manpower to keep things moving at the rate we need

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

So the absolute priority for us should be to increase this kind of manpower

view this post on Zulip Gaëtan Gilbert (Dec 17 2021 at 10:01):

Gaëtan Gilbert said:

let's see how it goes with https://github.com/coq/coq/pull/15365

ok it is there
I guess I got paranoid previously


Last updated: Feb 05 2023 at 20:03 UTC