OR and AND combinators in dune-project dependencies

[cpitclaudel]

Desired Behavior

I use dune to generate a .opam file. Currently, dune's dependencies language is weaker than OPAM's. OPAM allows "coq-ltac2" | "coq" { >= "8.11~" } to specify that a package needs coq-ltac2 or coq >= 8.11, but dune-project isn't as flexible.

This flexibility is useful when a package is merged into another one, for example. In the concrete case above, coq-ltac2 requires coq < 8.11, and coq 8.11 includes the functionality formerly provided by coq-ltac2.

Related: https://github.com/coq/coq/issues/12367

[rgrinberg]

We could support this with a form like:

(or
 (pkg1 ..)
 (pkg2 ..)
 ..)

But that might be a bit annoying to parse if a package or existed:

(or (> 1.0))

Perhaps the form should be :or?

@jeremiedimino what do you think?

[ghost]

Is : forbidden in opam package names?

[cpitclaudel]

Is : forbidden in opam package names?

Yup: https://github.com/ocaml/opam/blob/e733be207f5c83bac929154ee6e5b51d2bd120c3/src/format/opamPackage.ml#L79

Btw, a good test case for this feature would be dune's own dune-project (https://github.com/ocaml/dune/blob/master/dune.opam.template)

[ghost]

Alright, we can go for :or then. It's unfortunate to have to use (:or ...) at toplevel and (or ...) inside the constraints thought. The second one seems better. Maybe we should redesign this a bit for (lang dune 3.x). In the meantime it will do.

[avsm]

I was hoping to avoid having to support OR for as long as possible, as it also puts quite a bit of strain on the opam solver.

@cpitclaudel, you can work around by making a coq-ltac2.system package available with a constraint of coq {>="8.11~"}. This would let you then unconditionally depend on coq-ltac2 without worrying about the version of Coq installed in each dune project that uses ltac2. We use this method in quite a few places in the opam-repository to avoid having lots of OR clauses peppered throughout libraries.

[cpitclaudel]

you can work around by making a coq-ltac2.system package available with a constraint of coq {>="8.11~"}. This would let you then unconditionally depend on coq-ltac2 without worrying about the version of Coq installed in each dune project that uses ltac2.

Thanks. @ppedrot, does that sound reasonable?