Stream: Coq devs & plugin devs

Topic: 8.19 plan


view this post on Zulip Gaëtan Gilbert (Sep 26 2023 at 11:39):

Does this sound reasonable to everyone?

view this post on Zulip Guillaume Melquiond (Sep 26 2023 at 11:42):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 26 2023 at 11:46):

Sounds good to me @Gaëtan Gilbert , Guillaume's idea sounds good too.

view this post on Zulip Karl Palmskog (Sep 26 2023 at 19:35):

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

view this post on Zulip Karl Palmskog (Sep 26 2023 at 19:37):

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)

view this post on Zulip Gaëtan Gilbert (Sep 28 2023 at 11:40):

ok let's push the release a bit farther

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:42):

are you going to use the pre-release opam version feature this time and put the rc in the OCaml opam repo?

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:43):

I think the tag-related release automation is not set up for this currently

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:44):

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

view this post on Zulip Gaëtan Gilbert (Sep 28 2023 at 11:44):

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.

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:45):

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?

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:46):

per a call in March, this was supposed to be changed: https://github.com/coq/coq/wiki/Coq-Call-2023-03-08

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:46):

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...

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:47):

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

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:48):

that would just say "I can't satisfy coq's dependency, so I'm not compiling it".

view this post on Zulip Gaëtan Gilbert (Sep 28 2023 at 11:48):

why wouldn't we keep the rc in coq-opam-archive?

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:49):

I don't care personally, but the choice affects stuff like vscoq-lang-server or serapi, which usually live in the main repo.

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:49):

I think Emilio covers his arguments here: https://github.com/coq/opam/issues/2442

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:49):

if we put coq in our repo, these also need to be there.

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:49):

for the rc period, and then moved to another repo after the final

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:50):

unfortunately the plan we came up with does not work either, so I did not apply it for coq 8.18

view this post on Zulip Karl Palmskog (Sep 28 2023 at 11:50):

I'd just like the choice to be clear from the outset, it affects the community in quite a few ways

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:50):

I think that the choice is secondary, we don't have a way to make it work I'm afraid.

view this post on Zulip Gaëtan Gilbert (Sep 28 2023 at 11:51):

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

view this post on Zulip Enrico Tassi (Sep 28 2023 at 11:51):

I can try to explain this better in a coq call if you want

view this post on Zulip Michael Soegtrop (Sep 28 2023 at 11:51):

@Gaëtan Gilbert : isn't this one or two months faster than the 6 months pace we want to achieve ?

view this post on Zulip Gaëtan Gilbert (Sep 28 2023 at 11:53):

it looks faster because the delays haven't happened yet

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 17:43):

FTR I think there should have been a CEP and a prototype for this change.

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 17:44):

Since this didn't happen yet, all the more reason to ask for it.

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 17:49):

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.)

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 17:53):

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.

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 17:55):

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.

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 17:56):

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).

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 17:56):

(Or is there a misunderstanding here, and the "main" from the call notes actually refer to our own "released" repository?)

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 17:57):

The notes of this call are way too short to reflect the actual discussion that happened.

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 18:01):

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.

view this post on Zulip Théo Zimmermann (Sep 28 2023 at 18:02):

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.

view this post on Zulip Guillaume Melquiond (Sep 28 2023 at 18:04):

So, then we really need a written agreement from the maintainers of the Opam repository, before we even consider it.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2023 at 18:06):

@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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2023 at 18:08):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2023 at 18:08):

Namely the fact that I have to release SerAPI twice, which scales poorly.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 28 2023 at 18:09):

About rcs, note that already there are dozens of rc versions of packages in the main opam repos.

view this post on Zulip Enrico Tassi (Sep 28 2023 at 19:22):

@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.

view this post on Zulip Guillaume Melquiond (Sep 29 2023 at 05:28):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 29 2023 at 10:03):

@Guillaume Melquiond a few things:


Last updated: Apr 14 2024 at 11:02 UTC