Janno (Jun 04 2020 at 13:29): Janno (Jun 04 2020 at 13:29):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?
Karl Palmskog (Jun 04 2020 at 14:09):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.
Janno (Jun 04 2020 at 14:26):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?
Karl Palmskog (Jun 04 2020 at 14:41):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.
Karl Palmskog (Jun 04 2020 at 14:49):what I at least want to avoid is having released be a general experimental playground where packages break left and right
Michael Soegtrop (Jun 04 2020 at 15:09):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.
Karl Palmskog (Jun 04 2020 at 15:17):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)
Karl Palmskog (Jun 04 2020 at 15:23):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.
Michael Soegtrop (Jun 04 2020 at 15:31):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.
Michael Soegtrop (Jun 04 2020 at 15:32):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.
Théo Zimmermann (Jun 04 2020 at 15:39):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.
Karl Palmskog (Jun 04 2020 at 15:58):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.
Michael Soegtrop (Jun 04 2020 at 21:24):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.
Théo Zimmermann (Jun 04 2020 at 21:35):You probably looked at the bench for the wrong version of OCaml.
Théo Zimmermann (Jun 04 2020 at 21:35):Don't forget that Coq >= 8.10 requires OCaml >= 4.05
Last updated: Jun 05 2023 at 10:01 UTC