Dependency solver attempts to choose system-mingw dependency of ocaml-base-compiler on macos and linux

[gridbugs]

Solving on linux or macos with a dependency on (ocaml-base-compiler (= 5.2.0)) now gives the error:

Error: Unable to solve dependencies for the following lock directories:
Lock directory dune.lock:
Can't find all required versions.
Selected: ... ocaml-base-compiler.5.2.0 system-mingw
- system-mingw -> (problem)
    No usable implementations:
      system-mingw.1: Availability condition not satisfied

This seems to have been introduced when the ocaml packages in the opam repo gained native windows support in https://github.com/ocaml/opam-repository/commit/0b240d2960133fd3d8aa8f008d7aa79534caa3b9.

Repro: https://github.com/ocaml/dune/pull/10672

[gridbugs]

This happens because dune solves dependencies with the post variable set to false, so the following disjunction in ocaml-base-compiler's dependencies cannot be resolved:

(("arch-x86_64" {os = "win32" & arch = "x86_64"} & "system-mingw" &
    "mingw-w64-shims" {os-distribution = "cygwin" & build}) |
   ("arch-x86_32" {os = "win32"} & "ocaml-option-bytecode-only" &
    "system-mingw" &
    "mingw-w64-shims" {os-distribution = "cygwin" & build}) |
   "host-system-other" {os != "win32" & post})

[rgrinberg]

Anyway to talk to upstream about not using post for this? post dependencies don't really make sense in dune.

[gridbugs]

Yeh sure I'll chat with upstream. Can you elaborate a little on why post deps don't make sense in dune though. Is the idea that post deps in opam only make sense for executables that need a dep at runtime but not at compile time, and dune package management is only intended to install library dependencies (with the exception of the compiler, ocamlfind, ocamlbuild, and other build tools)?

[rgrinberg]

I don't recall the exact reasons, but I think it went something like this: all packages in dune need to define their dependencies explicitly. So there's no point to "install" a post dependency since it will not be available to anyone unless they explicitly ask for it. So if we have a package foo with a post dep bar, we can have two situations:

• a package depends on foo and bar - requires building bar with post = true
• a package depends on bar only - requires building bar with post = false

Or something along those lines. I could have misunderstood how post dependencies worked though. It would be good if you could revisit that.

[gridbugs]

I don't understand what you mean by "building bar with post = ...". The post variable is only relevant when computing the set of packages to install, not when building or installing individual packages.

However in this case I don't see why it's necessary. The host-system-other package has no dependencies.

The post variable is confusing to me as syntactically it looks like a variable in a dependency filter, but it's intended to be used to denote the relationship between two packages.

For dependency formulae without disjunctions or negations I can understand the intuition of treating post as a variable; it is true when computing the total set of packages to install, and false when computing the order in which to install packages. Without disjunctions or negations, changing post from true to false can only have the effect of reducing the set of dependencies.

But when there are disjunctions, as is the case here, I don't understand how post can be thought of as a variable that is set to true when computing dependencies and false when ordering them. If post is part of a disjunction then setting post to false can have the effect of adding additional dependencies, as the solver may choose a different "branch" of the disjunction in order to satisfy the dependency formula, and that branch may add dependencies on packages that weren't in the original set of dependencies computed when post was true.

A simplification of the above is considering the meaning of filtering a dependency on the negation of post. If a package depends on foo { ! post }, will foo be installed before the package? Will foo be installed at all?

@dra27 can you help clarify if/why post is needed in this case? Also can you help me understand how to think of post as a variable.

[dra27]

I agree post (and build) are confusing in the way they look as variables. Doing anything other than putting them as { post & rest-of-proposition } will have crazy-to-define semantics, I think! However, that's basically a bug in a package, if it does that.

I think the conception of what post is used for is slightly wrong - it's not intended as a convenience for installing packages after your own package. At least, they can be used for that kind of thing, but that's not what the core packages are doing - they're a key part of the constraint system.

In ocaml-base-compiler (and ocaml-variants, etc.), all of ocaml, base-*, host-* must be installed if ocaml-base-compiler is installed. The reason they must be installed, is that they be conflicted by other packages, and you obviously can't conflict something that's not installed. It's unusual that a package conflicts an ocaml version, rather than simply changing its depends, but there are examples of that already in opam-repository. It's definitely the case that packages can and should conflict base- (e.g. base-domains, base-nnp) and host- packages (e.g. conflicting host-system-msvc, etc.).

So ocaml-base-compiler does indeed depend on those packages being installed. What it doesn't depend on is them being installed before it. That's where the post comes in - they are "morally" post dependencies, because they do not need to be installed before the package (this is somewhat related to Depends/Pre-Depends and the handling of circular dependencies in dpkg, which I believe was the inspiration for the feature and also where the name post came from). For opam, that also means that a change to those packages does not trigger a rebuild of the compiler (I realise that's not relevant to Dune).

There is of course a "technical" need for the post dependency on the ocaml package because that itself depends on ocaml-base-compiler. However, the host- packages are also going to be depending on the compiler when they get properly extended to Unix systems (for the same reason as the ocaml package does - they'll be probing the compiler to verify correct selection).

I'm therefore not keen on the idea of removing the post dependency upstream, even while it's largely only there for "moral" reasons - because that post-dependency is likely to become "technical" soon, and because if we remove the post dependency, it means that any future change to those packages impacts general opam users.

In terms of how it works for Dune, I can see why you've ended up defaulting post=false - presumably it quietly dealt with the ocaml-base-compiler / ocaml circular dependency, but when solving it really should be true. For example, when requesting ocaml-base-compiler.4.14.2 in an empty switch (i.e. from cold), the solver is called with post=true and its response is something like: base-bigarray.base, base-threads.base, base-unix.base, host-arch-x86_64.1, host-system-other.1, ocaml-base-compiler.4.14.2, ocaml-config.2, ocaml-options-vanilla.1, ocaml.4.14.2.

However, the solver only gives the desired state - it doesn't give any indication of how to get there. At this stage, given that host-system-other doesn't (yet) depend on ocaml-base-compiler, there'd actually be no issue with doing a normal dependency graph sort. The problem, obviously, is the circular dependency between ocaml-base-compiler.4.14.2 and ocaml.4.14.2. It's when converting from a solution to a series of concrete (opam calls them atomic) actions that the post dependencies should then be dropped.

You can see that in OpamSolver.resolve, for example:

• When it loads the universe (OpamSolver.load_cudf_universe), it's called with ~post:true
• That then proceeds on to OpamCudf.resolve which calls the solver (i.e. at this point, all packages were evaluated with post=true)
• Further down, when it works out the simple_universe and complete_universe (that distinction is a complexity Dune doesn't need, because it's always starting from empty) both the calls then to OpamSolver.load_cudf_universe (which is via a local function univ_gen) are called with ~post:false and it's those two universes which are then passed to OpamCudf.atomic_actions which is the function for converting a desired final state to a series of actual actions.

[gridbugs]

Regarding your last point, is the original dependency formula solved a second time with post=false? The formula from ocaml-base-compiler I pasted above doesn't have a solution on non-windows systems when post=false. Why isn't that a problem for opam?

Here's the formula again for convenience:

(("arch-x86_64" {os = "win32" & arch = "x86_64"} & "system-mingw" &
    "mingw-w64-shims" {os-distribution = "cygwin" & build}) |
   ("arch-x86_32" {os = "win32"} & "ocaml-option-bytecode-only" &
    "system-mingw" &
    "mingw-w64-shims" {os-distribution = "cygwin" & build}) |
   "host-system-other" {os != "win32" & post})

[dra27]

The second part is not a solve - at that point, a dependency graph is being constructed, so the formula is only evaluated to determine the edges of the graph - so that formula when reduced with post=false simply doesn't add any edges to the graph (because "system-mingw" isn't in the graph).

[rgrinberg]

Okay, given that we know that post isn't a true variable, that simplifies the implementation considerably. I think we can provide proper support by:

1. Solving with {post} set to true
2. Generating the lock dir and the dependency graph of packages with {post} set to false
3. Extracting dependencies that are {post} to their own field in package definitions
4. Any time a package depends on x, it will also depend on the post dependencies of x.

Does that sound right?

[dra27]

It does, yes

[gridbugs]

4. Any time a package depends on x, it will also depend on the post dependencies of x.

I don't think this is quite right.

Say you have a depends on b, and b post-depends on a. 4 implies that a would depend on the post dependencies of its dependency b, which means that a depends on a which is a dependency cycle (a cannot be installed before itself).

The cycle could be longer, such as if a depends on b, and b post-depends on c, and c depends on a. So now a must be installed before c, but c is a post dependency of b, so 4 implies that a should depend on c so c must be installed before a.

So it seems we need to weaken the constraint about when post dependencies of a package need to be installed. @dra27 would it be sufficient to guarantee that post deps are installed at some point during package installation? E.g. could we defer the installation of any post-deps to after all other packages have been installed? What guarantees (if any) does a package have about when the post dependencies of its dependencies are installed?

And in dune's case where packages are built in a sandbox and not generally available in the user's environment, if it's correct to defer installation of post dependencies until all other packages are built, it seems to me that it would also be correct to not install post dependencies at all.