Long term policy for handling opam packages · Coq Platform devs & users

I am about to start adding a bunch of new packages to Coq platform. Historically in about half of the cases this means I need to fix the opam package in some way - either platform specific stuff or package version incompatibility issues. Currently I do this by first adding a local opam patch to Coq Platform, push it upstream and remove it locally again. Sometimes the opam packages have dependencies so that this process can take quite some time - also because I do not always have time to take care of this and trigger the next action after something has been merged.

The main downside of this is that although I do spend quite some time on this, I so far didn't manage to create a Coq Platform opam package, because this would mean I have no local opam patches remaining. Right now I create new local patches at about the same rate as I push them upstream.

To give an example: remake (the tool e.g. @Guillaume Melquiond uses to build most of his projects) didn't compile with XCode 12. As is, I need 6 PRs for each of the affected projects, the add local, push upstream and remove local PR for adding an opam level patch and at least on Coq Platform master another round of 3 PRs to remove the opam level patch again after Guillaume added the fix in his projects. Multiplied by a few projects and 2 Coq platform branches this is a lot of PRs, which need to be properly orchestrated so that nothing breaks temporarily. On top comes creating issues for the affected projects, but this is usually the least effort.

1.) Continue with the above procedure: local patch, push upstream, remove local - as I said the main downside might be that it will take long until we have a Coq Platform opam package.
2.) Make batch PRs to the Coq opam repo for dependent requests. In the past I didn't do this because some changes need discussion / awareness of stakeholders / maintainers and if a PR gets too large this does not really work. This might or might not get better in the future.
3.) Relax a bit on the review policy for the coq opam repo (actually I don't know what it is), say that at least for those PRs which do not need discussions - e.g. platform specific fixes like the discussed XCode fix - I merge my own PRs to the Coq opam repo (for which I would need write rights). Then I could avoid making Coq Platform local patches for this.
4.) At least in more active phases have a fixed schedule for PR review and merge
5.) Other ideas

I guess we also can have a different policy for dev and released. dev was called by @Karl Palmskog "Wild West", so I guess not many people care. Released should be different, but here we should also consider that fixing e.g. new system incompatibilities (like the XCode 12 issue) quickly is part of the user perceived quality.

Karl Palmskog (Jan 31 2021 at 13:03):

fine by me if Michael gets merge rights for the Coq opam repo (ping @Enrico Tassi )

Karl Palmskog (Jan 31 2021 at 13:10):

there is no official review policy for the Coq opam repo to my knowledge, but between maintainers there are conventions like "passing CI unless there is some unrelated issue causing failures [see: Dune and Hierarchy Builder on pyrolyse]"

Michael Soegtrop (Jan 31 2021 at 14:34):

@Karl Palmskog : is it common practice to merge someones own PRs on coq opam release? It would help me if we could agree on that the following cases may be "self merge without review" (assuming CI passes):

In all other cases, as far as I can see now, a usual review + someone else merges process should be fine.

Karl Palmskog (Jan 31 2021 at 14:42):

@Michael Soegtrop I self-merge from time to time, but only when it is uncontroversial. For a controversial package, I would request a review like in Coq itself.

Karl Palmskog (Jan 31 2021 at 14:44):

the key for the opam repo is high velocity, in my view. We can always correct packages later. When fixing a package with some other maintainer, unless it is a big change, I think it's OK to just cc the maintainer and self merge (perhaps after some time period like a day, so the maintainer has the opportunity to veto)

Michael Soegtrop (Jan 31 2021 at 16:48):

@Karl Palmskog : I would say we agree : self merge of opam packages is OK if one can expect it to be not controversial and speed is of some importance.

Enrico Tassi (Jan 31 2021 at 17:14):

If I had to write "the rules" I would separate the "update and existing package/a new version" case from the "new package" one. For the former, things should be about speed of merge, I agree with Karl. It may still make sense to look a bit more carefully at new packages, Coq users are not necessarily opam experts.

Karl Palmskog (Jan 31 2021 at 17:19):

one high-priority issue we need to be aware of is what happened to MetaCoq. Their new version number was ordered before the one for their previous release. This led to all kinds of havoc, e.g., that some users were prompted to install old Coq versions.

Enrico Tassi (Jan 31 2021 at 17:40):

Hum, metacoq does not depend on a single Coq version? It seems odd, since it contains ML code.

Enrico Tassi (Jan 31 2021 at 17:42):

depends: [
  "ocaml" {>= "4.07.1" & < "4.12~"}
  "coq" { >= "8.12~" & < "8.13~" }
  "coq-metacoq-template" {= version}
  "coq-metacoq-pcuic" {= version}
  "coq-metacoq-safechecker" {= version}
  "coq-metacoq-erasure" {= version}
  "coq-metacoq-translations" {= version}
]

Guillaume Melquiond (Jan 31 2021 at 19:51):

I think Karl is referring to the fact that the versions were 1.0~alpha2+8.10 and 1.0~alpha+8.8, so the version of MetaCoq for Coq 8.8 was considered more recent than the later version for Coq 8.10, thus breaking user installations. So, he had to quickly rename 1.0~alpha+8.8 into 1.0~alpha1+8.8 to solve the breakage.

Karl Palmskog (Jan 31 2021 at 21:35):

yes, they first had *-alpha+XX, then they did *-alpha2+XX (and we renamed the first to *-alpha1+XX). Users definitely need help to detect problems like that.

Stream: Coq Platform devs & users

Topic: Long term policy for handling opam packages

Michael Soegtrop (Jan 31 2021 at 09:59):