Christian Doczkal (Jun 18 2020 at 16:14): Christian Doczkal (Jun 18 2020 at 16:14):What's the proper way to specify version constraints for the "dev" opam packages? I have found various approaches within math-comp:
"coq-mathcomp-character" { (>= "1.10.0") | (= "dev") }"coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") | (= "dev") }"coq-mathcomp-algebra" { = "dev" }I ran across this when I tried to pin my locally checked out master branch of fourcolor in an opam switch for mathcomp-1.11.0. Presumably, for CI it is only relevant that "dev" is a valid dependency. I would say that, in particular for packages that are not automatically released alongside mathcomp (e.g., fourcolor), the scheme used by odd-order is the "right" one. Should I make a PR for fourcolor (the opam file in the repository also creates a package called "coq-mathcomp-fourcolor", which doesn't match the package name in OPAM.
Karl Palmskog (Jun 18 2020 at 16:20):I think the finmap one is the most reasonable if the plan is to do regular releases for the package. Leads to least problems with compatibility, allows advanced users to use pinned git repos straightforwardly, and follows "standard" for depending on Coq.
Karl Palmskog (Jun 18 2020 at 16:23):{ (>= "1.10.0") | (= "dev") } has redundancy since >= "1.10.0" already allows dev
Christian Doczkal (Jun 18 2020 at 16:27):Karl Palmskog said:
{ (>= "1.10.0") | (= "dev") }has redundancy since>= "1.10.0"already allowsdev
True, there is a redundancy, but I don't think it hurts to be explicit about the dev version, if only because it's a string and not a number sequence.
Christian Doczkal (Jun 18 2020 at 16:32):In any event, my main point is that { = "dev"} is unnecessarily restrictive for packages without regular releases. In this context, an explicit upper bound can cause just as much frustration following a release of mathcomp. Mind you, I'm not talking about released packages. There the upper bound can clearly be useful.
Karl Palmskog (Jun 18 2020 at 16:35):if = "dev" is too restrictive, and there is no plan to do regular releases, it may actually be a good idea to leave version dependency blank
Christian Doczkal (Jun 18 2020 at 16:37):I think there is no point in letting users try to pin a package in a context where compilation is known to fail.
Karl Palmskog (Jun 18 2020 at 16:47):but then you have to continually update your package definition, so why not just do regular releases and proper bounds? Blank version deps are in my mind a way to signal: caveat emptor, etc.
Christian Doczkal (Jun 18 2020 at 16:50):Well, fourcolor gets updated essentially only when there is a breaking change in mathcomp dev. At this point one could simply raise the lower bound to "current+1", because it's known not to work with any previous stable release.
Christian Doczkal (Jun 18 2020 at 16:55):If there is only a lower bound, there is no need to update all the time, but one can if one wants to. With an upper bound the dev package is uninstallable after every mathcomp release until the package maintainer has adapted the bounds.
Karl Palmskog (Jun 18 2020 at 16:57):so in conclusion I would then have for fully maintained projects:
"coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") | (= "dev") }
and for less maintained projects:
"coq-mathcomp-ssreflect" {>= "1.11.0"}
Yes, probably. But let's see what the mathcomp devs say.
Karl Palmskog (Jun 18 2020 at 16:59):potentially something like this could added into our mustache templates
Erik Martin-Dorel (Jun 30 2020 at 21:43):Hi @Christian Doczkal, FYI there have been a related discussion with @Cyril Cohen (about the best version constraints to choose for new opam releases of coq-mathcomp-ssreflect) in this recent Zulip stream:
Erik Martin-Dorel (Jun 30 2020 at 21:46):(FTR, the daily check that the latest mathcomp release is still compatible with coq.dev is now triggered by this line: https://github.com/math-comp/docker-mathcomp/blob/5ee324e28f5600392e00d9f84244f46e18dead11/images.yml#L31 )
Last updated: Oct 13 2024 at 01:02 UTC