Stream: math-comp devs

Topic: dependency version constraints for dev packages


view this post on Zulip 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:

  1. odd-order: "coq-mathcomp-character" { (>= "1.10.0") | (= "dev") }
  2. finmap: "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") | (= "dev") }
  3. fourcolor: "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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 18 2020 at 16:23):

{ (>= "1.10.0") | (= "dev") } has redundancy since >= "1.10.0" already allows dev

view this post on Zulip Christian Doczkal (Jun 18 2020 at 16:27):

Karl Palmskog said:

{ (>= "1.10.0") | (= "dev") } has redundancy since >= "1.10.0" already allows dev

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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"}

view this post on Zulip Christian Doczkal (Jun 18 2020 at 16:59):

Yes, probably. But let's see what the mathcomp devs say.

view this post on Zulip Karl Palmskog (Jun 18 2020 at 16:59):

potentially something like this could added into our mustache templates

view this post on Zulip 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:

https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/MathComp.201.2E11.2E0.20OPAM.20packages.20Coq.20compatibility/near/200407648

view this post on Zulip 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: Mar 29 2024 at 05:40 UTC