Who will do the bignums release for 8.15?
should I do a github release for the rc?
yes, the idea now is that releases are done for "core" Coq projects once Coq reaches rc stage
but we should first have the RC1 release in the Coq opam archive (extra-dev
part)
why?
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)
I don't see any rcs in https://github.com/coq/coq/releases
did they get deleted?
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
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
please create and keep the GitHub releases of release candidates
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
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.
otherwise, we can't even begin doing testing for the Coq platform, which is what the whole RC process is meant to be about
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
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
I'm not doing bignums but I did https://github.com/coq/opam-coq-archive/pull/1974/files
thanks
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.
That being said, there is indeed no relation between the GitHub release and the opam release.
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.)
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.
Thanks!
BTW, I think we should also attach the PDF to the 8.14.1 release.
Unfortunately, the job artifact would have expired by now. Would it have not?
Good news. It did not expire.
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.
"Something went really wrong, and we can’t process that file."
So, no reference manual for 8.14.1.
I can try to do the upload if you give me the link to the PDF artifact on GitLab.
it attached fine for 15rc1
https://gitlab.com/coq/coq/-/jobs/1801642479/artifacts/download
Done. I think it works better when you have a good bandwidth.
I am on the 10GB backbone, so it cannot get any better than that...
(And I did try several times, they all ended with "something went terribly wrong".)
Weird
I had that until I unblocked some github domain which appeared in umatrix
@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.
sure I can do it
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.
done
@Karl Palmskog you might want to announce that, at least I'm waiting for it for equations's and metacoq's CI
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)
@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?
Sure will do asap
if you ping me somehow, I can/will take care of the opam package (in extra-dev
)
Noted, thanks
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
")
Is the plan to release 8.15 this year?
https://github.com/coq/coq/wiki/Release-Schedule-for-Coq-8.15
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
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.
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.
The only other package that we've added since is SerAPI, and indeed, this one might have been a mistake (for the base image).
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.
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.
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
8.14.2 PRs are automatically added to the Coq 8.15 project in principle.
Indeed, all the merged PRs in this milestone were backported already, except #14967 because it was merged before the v8.15 branch.
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).
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
IIRC
let's see how it goes with https://github.com/coq/coq/pull/15365
From the PR timeline, it seems like it is coqbot which added all of them to the project.
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?
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.
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
Forgive my wording, I guess "experimental" might be better. From what I gathered from what Emilio said, he considers SerAPI is an experiment.
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.
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...
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.
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.
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.
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"
We have ppx, we also have a lot of libraries that modern proof systems require such as json, etc....
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
And unless I'm wrong, we lack the right expertise/manpower to keep things moving at the rate we need
So the absolute priority for us should be to increase this kind of manpower
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