Does this sound reasonable to everyone?
A good part of the period between the rc and the release will be impeded by the end of year. It might be worth moving both dates forward by one week, to give more time for people to update their packages before the release.
Sounds good to me @Gaëtan Gilbert , Guillaume's idea sounds good too.
I agree with pushing 8.19.0 one week forward, but I think most of the work with the rc is Platform related (releasing various plugins, updating opam bounds of released packages for 8.19). So would be best to keep 8.19+rc1 at 2023-12-11
it would be nice if we had a bunch of independent Coq project maintainers throwing themselves over the rc and testing and making releases, but the reality is that rc is mostly about Platform at this point (plugins, and testing if non-plugin Platform packages even need a release)
ok let's push the release a bit farther
are you going to use the pre-release opam version feature this time and put the rc in the OCaml opam repo?
I think the tag-related release automation is not set up for this currently
also beware the discrepancies that need to be accounted for between the "deployed" opam files and those in the Coq GitHub repo, see https://github.com/ocaml/opam-repository/pull/24378/commits
the release process still says
In particular, ensure that someone is working on providing an opam package (either in the main ocaml/opam-repository for standard releases or in the core-dev category of the coq/opam-coq-archive for preview releases.
FTR, I did not do it because of lack of time and one unresolved question.
If we make the rc depend on a beta-program-opt-in package, how is opam's CI going to test our package? The beta-program-opt-in package was supposed to be in which repo exactly?
per a call in March, this was supposed to be changed: https://github.com/coq/coq/wiki/Coq-Call-2023-03-08
My recalling is that the package was supposed to be in core-dev, but in that case their CI is just going to say coq.8.19+rc1 is not installabale anywhere...
Yes, thanks for the pointer. What I'm saying is that the plan does not work, since coq-beta
is in a repo not used by ocaml/opam-repository CI
that would just say "I can't satisfy coq's dependency, so I'm not compiling it".
why wouldn't we keep the rc in coq-opam-archive?
I don't care personally, but the choice affects stuff like vscoq-lang-server or serapi, which usually live in the main repo.
I think Emilio covers his arguments here: https://github.com/coq/opam/issues/2442
if we put coq in our repo, these also need to be there.
for the rc period, and then moved to another repo after the final
unfortunately the plan we came up with does not work either, so I did not apply it for coq 8.18
I'd just like the choice to be clear from the outset, it affects the community in quite a few ways
I think that the choice is secondary, we don't have a way to make it work I'm afraid.
Karl Palmskog said:
I think Emilio covers his arguments here: https://github.com/coq/opam/issues/2442
this doesn't suggest putting the rc in ocaml/opam unless I misunderstand
I can try to explain this better in a coq call if you want
@Gaëtan Gilbert : isn't this one or two months faster than the 6 months pace we want to achieve ?
it looks faster because the delays haven't happened yet
FTR I think there should have been a CEP and a prototype for this change.
Since this didn't happen yet, all the more reason to ask for it.
Enrico Tassi said:
Yes, thanks for the pointer. What I'm saying is that the plan does not work, since
coq-beta
is in a repo not used by ocaml/opam-repository CI
This plan should work, because ocaml/opam-repository is using Opam >= 2.1.0, so the dependency on coq-beta
will not trigger. (Whether we want to pollute ocaml/opam-repository with our release candidates is a whole different matter, and this is the question we have to answer.)
And obviously, this critically depends on whether the maintainers of the main Opam repository would actually agree on our dumping our release candidates on them.
But I thought the plan was to put our release candidates in our own Opam repository (but the released
one, not the core-dev
one). I don't remember we ever discussed putting them in the main Opam repository.
I believe the plan was to put them in the main opam repo. But the fact this is still so fuzzy to a lot of people should advocate for considering that we haven't really taken this decision yet (even though we actually did, during a Coq Call).
(Or is there a misunderstanding here, and the "main" from the call notes actually refer to our own "released" repository?)
The notes of this call are way too short to reflect the actual discussion that happened.
In fact, since https://github.com/coq/opam/issues/2442 says "packages willing to go to the main Opam repos can do so", and here "packages" mean "Coq user packages" (I think), then it seems that "main" indeed refers to our own "released" repository.
Nope, because Emilio's goal is to allow Coq-related packages to be in the official opam-repository (like SerAPI, coq-lsp, and vscoqtop already do). So that users do not need to add the coq-released repo.
So, then we really need a written agreement from the maintainers of the Opam repository, before we even consider it.
@Guillaume Melquiond I don't see why we need such agreement, that's news to me. Anyways I talked to them and the plan looked fine to them.
Packages that are mainly written in OCaml should be hosted in the OCaml opam repos, for the many reasons stated in the issue / call.
Moreover, that would solve a critical flaw in our release process.
Namely the fact that I have to release SerAPI twice, which scales poorly.
About rcs, note that already there are dozens of rc versions of packages in the main opam repos.
@Guillaume Melquiond are you saying that a package with avoid-version
is tested anyway by their CI?
I mean, if serapi
depends on coq-core >= X, where X is a an avoid-version, would they compile it?
If so, I think I got it wrong.
Emilio Jesús Gallego Arias said:
Guillaume Melquiond I don't see why we need such agreement, that's news to me. Anyways I talked to them and the plan looked fine to them.
Because that is not how the Opam repository works currently. Let us be factual. Just count how many release candidates there exist. Among the thousands of packages in the repository, only 6 projects have had release candidates. Among these 6, two are OCaml and Opam themselves. Two never did it again after their 1.0.0 release. One did not do it for its last 15 releases. So, that leaves only one user project that routinely dumps release candidates in the Opam repository, among the thousands that exist.
To stress my point, let us consider a case that you are well aware of: Dune. Three pull requests for pre-release versions of Dune 3.11.0 were submitted to the Opam repository but none of them got merged! In fact, the Opam repository does not contain any pre-release version of Dune whatsoever. Pull requests are just being used to exercise Opam's CI, but certainly not to make pre-release versions available to users.
And now you come and tell us that the maintainers of the Opam repository are perfectly fine with us dumping release candidates in the repository? Paint me doubtful.
@Guillaume Melquiond a few things:
Last updated: Oct 13 2024 at 01:02 UTC