Gaëtan Gilbert (Dec 07 2021 at 13:53): Gaëtan Gilbert (Dec 07 2021 at 13:53):Who will do the bignums release for 8.15?
Gaëtan Gilbert (Dec 07 2021 at 13:58):should I do a github release for the rc?
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
Karl Palmskog (Dec 07 2021 at 14:03):but we should first have the RC1 release in the Coq opam archive (extra-dev part)
Gaëtan Gilbert (Dec 07 2021 at 14:23):why?
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)
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?
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
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
Karl Palmskog (Dec 07 2021 at 14:27):please create and keep the GitHub releases of release candidates
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
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.
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
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
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
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
Karl Palmskog (Dec 07 2021 at 14:43):thanks
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.
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.
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.)
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.
Théo Zimmermann (Dec 07 2021 at 16:24):Thanks!
Théo Zimmermann (Dec 07 2021 at 16:24):BTW, I think we should also attach the PDF to the 8.14.1 release.
Guillaume Melquiond (Dec 07 2021 at 16:24):Unfortunately, the job artifact would have expired by now. Would it have not?
Guillaume Melquiond (Dec 07 2021 at 16:30):Good news. It did not expire.
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.
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.
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.
Gaëtan Gilbert (Dec 07 2021 at 16:53):it attached fine for 15rc1
Guillaume Melquiond (Dec 07 2021 at 16:55):https://gitlab.com/coq/coq/-/jobs/1801642479/artifacts/download
Théo Zimmermann (Dec 07 2021 at 17:15):Done. I think it works better when you have a good bandwidth.
Guillaume Melquiond (Dec 07 2021 at 17:18):I am on the 10GB backbone, so it cannot get any better than that...
Guillaume Melquiond (Dec 07 2021 at 17:19):(And I did try several times, they all ended with "something went terribly wrong".)
Théo Zimmermann (Dec 07 2021 at 17:19):Weird
Gaëtan Gilbert (Dec 07 2021 at 17:23):I had that until I unblocked some github domain which appeared in umatrix
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.
Gaëtan Gilbert (Dec 08 2021 at 13:20):sure I can do it
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.
Gaëtan Gilbert (Dec 08 2021 at 13:23):done
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
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)
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?
Emilio Jesús Gallego Arias (Dec 10 2021 at 20:53):Sure will do asap
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)
Emilio Jesús Gallego Arias (Dec 10 2021 at 20:56):Noted, thanks
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")
Fabian Kunze (Dec 13 2021 at 15:58):Is the plan to release 8.15 this year?
Gaëtan Gilbert (Dec 13 2021 at 16:12):https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.15
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
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.
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.
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).
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.
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.
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
Théo Zimmermann (Dec 16 2021 at 13:18):8.14.2 PRs are automatically added to the Coq 8.15 project in principle.
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.
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).
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
Gaëtan Gilbert (Dec 16 2021 at 13:22):IIRC
Gaëtan Gilbert (Dec 16 2021 at 13:22):let's see how it goes with https://github.com/coq/coq/pull/15365
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.
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?
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.
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
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.
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.
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...
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.
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.
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.
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"
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....
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
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
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
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: Dec 07 2023 at 09:01 UTC