Are there (documented?) best practices for publishing opam packages for Coq plugins? I am specifically interested in what version constraints I should be putting on the "coq" dependency in the opam file. Also, is it good practice in general to always include | = "dev"
for all the dependencies?
I think putting | = "dev"
is terrible in general for the released
repo, and for plugins it's even worse. Generally, one writes {>= "8.10" & < "8.11"}
and the like for plugins.
As somebody who works on master versions of basically everything I use I keep having to do --ignore-constraints-on=<long list of coq related packages>
to use opam at all. Maybe this could be solved by having a dev
version of plugins/libraries (outside of the released
repo) that has the | = "dev"
option for all its dependencies?
I'm all for having dev
versions in the coq-extra-dev
repo, and they can also be version-specific there if the author wants.
what I at least want to avoid is having released
be a general experimental playground where packages break left and right
IMHO one should indeed have several version in opam for different audience. There should be a release version and in my opinion the version dependencies given there should reflect exactly what has been actually tested. For Coq platform opam packages I usually put in a list of version equals for those versions it has been tested for, but this might be a bit too extreme. I think what Karl suggested - that is restricting it to exactly one minor version - is also OK. But if one plugin version spans several minor versions, I would give them explicitly to indicate that this really has been tested, or at least leave a not that this is so.
On top of that one needs a version which is much less restricted but offers no guarantees.
I agree completely with @Michael Soegtrop except that I think the "exactly one minor version" restriction only applies to plugins, which break much more often than anything else. For libraries, we have had many that successfully support many Coq versions (although I personally don't support including future versions as compatible when submitted to released
)
we do have a problem that some packages become "too restricted" over time, e.g., a library package might have a bound that prevents Coq 8.11, even though it actually works with 8.11. But this to me is part of the responsibilities of a maintainer. And if developers release new packages in reponse to new releases anyway (which they normally should), overrestriction almost never becomes an issue.
we do have a problem that some packages become "too restricted" over time, e.g., a library package might have a bound that prevents Coq 8.11, even though it actually works with 8.11. But this to me is part of the responsibilities of a maintainer. And if developers release new packages in reponse to new releases anyway (which they normally should), overrestriction almost never becomes an issue.
I think this should be solved in another way: automated CI and automated updates of opam files. I had the opposite issue in the past, that opam says certain things will work, and they didn't.
Btw.: for the Coq platform my plan is to make tested releases and to update all opam files as part of the platform release, so that these tests are reflected.
Overconstraining vs underconstraining has been a long standing issue in the opam ecosystem. I think there are interesting discussions about that on the OCaml Discourse.
Michael Soegtrop said:
Btw.: for the Coq platform my plan is to make tested releases and to update all opam files as part of the platform release, so that these tests are reflected.
this would be a huge improvement, but only solves the problem for a quite small fraction of all the packages we have on Coq's opam. I think we need more work on exploratory ci along the lines of Guillaume's coq-bench. Currently, coq-bench fully obeys all restrictions in packages, but there are ways of intelligently ignoring some constraints.
I think we need more work on exploratory ci along the lines of Guillaume's coq-bench. Currently, coq-bench fully obeys all restrictions in packages, but there are ways of intelligently ignoring some constraints.
I fully agree. Thanks for the link - intersting. Any idea why it stops at Coq 8.9.1? What I envision is something like this with automatic updates to opam.
You probably looked at the bench for the wrong version of OCaml.
Don't forget that Coq >= 8.10 requires OCaml >= 4.05
Last updated: Nov 29 2023 at 19:01 UTC