add `and` constraints in depopts cnf

[avsm]

From a cl-mirage question about cohttp:

depends: [ "ocamlfind" "re" "uri" {>="1.3.2"} "ounit" ]
depopts: [ "async" {="108.00.02"} "lwt" {>="2.4.1"} "mirage-net" ]

However, cohttp requires Lwt AND SSL to be installed, or it fails (since SSL is not yet optional).

Is there any way to express this in the CNF? I tried:

Currently this not possible (as depopts are OR constraints only), but I guess I could add that in 0.8 if you open an issue for that :-)

depopts: [ "async" {="108.00.02"} ("lwt" {>="2.4.1"} "ssl") "mirage-net" ]

I think I will go with the following syntax:
depopts: [ "async" {="108.00.02"} ("lwt" {>="2.4.1"} & "ssl") "mirage-net" ]
as this is kind of dual with 'depends' where you express AND constraints, and use '|' for OR.

[samoht]

Translating any formluas into CNF in the depends field should be easy, however the depots field has a different semantics, so I'm not sure (yet) how to do that properly.

[samoht]

OK, I've done some digging in there, and it appears that it is not easy to change the semantics of depopts without too much changes in the solver. Indeed, if you want what appears in "depots" to force the installation of some packages in some cases (for instance, if you want "ssl" to install when "lwt" is already there), then you need either:

• to encode that constraints as a normal dependency and give it to the solver. The problem is that the solver is not very good in ensuring minimality, so you will almost end-up with all the optional packages installed (I've implemented something like that, and I was not very happy with the result)
• to add some of the depopts as normal dependency, and call the solver until we reach a fix point (I didn't manage to completely implement this bit, as I needed to modify the solver interface too much, thing that I'll like to avoid)

So finally, I've come up with a simpler solution:

• the semantics of depopts is unchanged: packages appearing here are not used to compute the packages to install/remove, but they are used to know when to recompile a package. I've allowed any kind of formula in there, for documentation purposes.
• I've added a way to easily compose opam variable in opam files: %{lwt+ssl:enable}% is enable iff %{lwt:enable}% and %{ssl:enable}% are bot enable.
• you can write any kind of formula in the depends field (which is automatically translated to CNF before giving it to the solver) so you can manually encode some complex depopts/depends problems if needed.

[avsm]

Ok, so if I understand this, for cohttp we keep lwt in depopts, and add %{lwt+ssl:enable} to prevent build breakage if ssl is not installed. Optionally, we could add ssl into depends unconditionally to avoid confusion. Is that right?

[samoht]

yes, you could either:

• keep depopts as "async" ("lwt" & "ssl") "mirage-net" and use --%{lwt+ssl:enable}%-lwt in the commands
• or write: depends: [ .... ("async" | ("lwt" "ssl") | "mirage-net")] in this case, the solver will try not to install unnecessary packages, but sometimes he fails.

[avsm]

ok...I'll make this change in a few days when 0.7.6 is out, as it breaks backwards compatibility with the repository format.

On 3 Oct 2012, at 12:43, Thomas Gazagnaire notifications@github.com wrote:

yes, you could either:

keep depopts as "async" ("lwt" & "ssl") "mirage-net" and use --%{lwt+ssl:enable}%-lwt in the commands or write: depends: [ .... ("async" | ("lwt" "ssl") | "mirage-net"] in this case, the solver will try not to install unnecessary packages, but sometimes he fails. — Reply to this email directly or view it on GitHub.

[rdicosmo]

We just had a little discussion here at Irill on this issue with Pietro and Ralf: the encoding into CUDF for the solver of the ("lwt" & "ssl") is doable by a simple manipulation of the CUDF document passed to the solver:

• create an artificial package "lwt+ssl" in the CUDF document with dependency depends: [ "lwt" "ssl" ]
• replace the dependency ("lwt" & "ssl") with a dependency on "lwt+ssl" wherever it occurs
• filter out the artificial package "lwt+ssl" from the solution returned by the solver

That's all :-)

In general you can extend this encoding to arbitrary CNF formulae containing & .

[samoht]

Hi Roberto. I'm not sure I understand how this will help.

The problem can be summarized as follow: I have 3 packages, A, B and C. A optionally depends on "B+C", which means the only "valid" universes are:

• A installed
• B installed
• C installed
• B &C installed
• A & B & C installed

Does your trick help to solve this ?

[rdicosmo]

Hi Thomas, yes, the encoding proposed above totally solves the issue. Let me say this again:

• you can keep the "&" at the surface syntax, so you can write A depopts: [ ( B & C ) ]

• when encoding into CUDF, do the following:

  • add a new fake package having as name something like "B+C", (make sure it does not conflict with an existing package name) and with dependency

  depends: [ B C ]

  • replace any instance of "B & C" in the surface syntax a single dependency on this new package "B+C"
  • call the solver
  • drop the fake package "B+C" from the solution

The only correct universes will be the ones you want.

The point of this encoding is that it is simple, does not take up much space, and does not require changing anything in the CUDF machinery (CUDF does not support arbitrary formulae in the dependencies, only CNF ones).

We can disuss this on a blackboard when you are in Paris :-)

[rdicosmo]

Let me add for clarity that the translated CUDF would be

package: A depopts: B+C

package: B+C depends: B, C

[rdicosmo]

Anyway, I suggest we discuss all the translation together at the first occasion.

[samoht]

Hum, I'm still not totally convinced. If you start with the universe: {B} then if you call the solver to install {A}, what constraint will cause either B to be uninstalled or C to be installed ?

[rdicosmo]

ok, I see what you mean, will be back on this later :-) Le 15 oct. 2012 18:12, "Thomas Gazagnaire" notifications@github.com a écrit :

Hum, I'm still not totally convinced. If you start with the universe: {B} then if you call the solver to install {A}, what constraint will cause either B to be uninstalled or C to B installed ?

— Reply to this email directly or view it on GitHubhttps://github.com/OCamlPro/opam/issues/200#issuecomment-9450451.

[rdicosmo]

Hi Thomas, here is a more extensive discussion of this issue.

Looking at your last message, I think we misunderstood your requirement: we thought that, since you are compiling sources from scratch, the presence or absence of B and C together is only relevant when installing A, as that is the moment when you recompile A, and you link in the libraries from B and C; in this particular case the suggested translation was reasonable; but of course there are situation where you do dynamic linking etc., so opam must ensure at any time that A's runtime dependencies are satisied, and you need a more thorough translation (see better suggestion below). Anyway, it is possible that at some time you will need to add in opam the distinction between dependency and build-dependency found in Debian.

Since you really want to have either B and C or none of them together with A, it is necessary to encode somehow in A's dependencies the fact that B<=>C.

We suggest to consider taking full advantage of what CUDF solvers offer today; if you have access to MISC-competition compliant external solvers, like aspcud, p2cudf, mccs or packup, you may proceed as follows:

• encode the optional B & C in CUDF in two steps:
  • add the CNF encoding of B <=> C in the depends: field (this ensure either both of B and C will be there, or none)
  • add the B+C fake package to the optional dependencies, as suggested before; this should go in the recommends: field of the CUDF document
  • when calling the solver, you may specify a policy that minimizes or maximizes the number of recommends: that are satisfied, and the solver will find a solution for you (no need to do special tricks or fiddling with the universe for this)

In any case, some tracking work is needed to recompile A if one discovers that some of its optional dependencies have changed, but I imagine you do that already.

[samoht]

This should be fixed by the recent changes in the solver API.

Now, if depopts = d_1 | .. | d_n, then depends += d_i iff d_i contains a package wich is installed. So for instance if lwt is installed, then:

depends: [ "ocamlfind" "re" "uri" {>="1.3.2"} "ounit" ]
depopts: [ "async" {="108.00.02"} ("lwt" {>="2.4.1"} & "ssl") "mirage-net" ]

is rewritten as:

depends: [ "ocamlfind" "re" "uri" {>="1.3.2"} "ounit" "lwt" {>="2.4.1"} "ssl"]

[rdicosmo]

Unfortunately, this does not prevent the solver from returning a solution that violates a conjunctive depopt if no one of the conjunct is previously installed.