pkg: Use `filtered_formula` to represent dependencies by Leonidas-from-XIV · Pull Request #10918 · ocaml/dune

Leonidas-from-XIV · 2024-09-13T14:25:57Z

At the moment when an OPAM package in the local packages we only accept a list of Atoms, so if it has an disjunction in the dependencies we fail when loading as we attempt to parse the list of Atoms into a Dependency_set.t structure. This structure only supports a sequence of conjunctions (as that is the only syntax that dune-project files support at the moment).

This PR changes the internal representation of the dependencies to be OpamTypes.filtered_formula as when reading OPAM files this is what we get from the OPAM file parser. When we pass the data to the solver it is also OpamTpyes.filtered_formula that we have to encode back to. Thus I suggest keeping OpamTypes.filtered_formula as dependency specification and compute the information we need from it directly. The information is fairly limited as we only need one example package name for an error message and a hash of the dependencies.

The downside of this is that all existing dependency hashes change (see tests), as the representation of the package constraints the hash is calculated over is changing, but I consider this an acceptable compromise.

Fixes #10837

ElectreAAS

Some tests expectedly fail with hash incongruences, but some others fail with this:

-  File "x.opam", line 1, characters 0-0:
-  Error: Expected formula to be a conjunction of atoms but encountered non-atom
-  term 'a | b'
+  Error: Unable to solve dependencies for the following lock directories:
+  Lock directory dune.lock:
+  Can't find all required versions.
+  Selected: x.dev a
+  - a -> (problem)
+      No known implementations at all

Shouldn't these tests now pass with a proper build?

src/dune_pkg/local_package.ml

Leonidas-from-XIV · 2024-09-16T12:42:08Z

@ElectreAAS The failure you quoted makes sense, because the test in opam-file-errors.t does not define a package a or b. To merge this PR I think the best way would be to change it to to define a (and maybe b) and show that these are supported now. The other tests in the file can be deleted to as we don't convert filtered_formulas into dune conditions anymore, so the error case that this is exercising would not happen anymore.

The hash changes are an unfortumate side-effect as the non-local dependency set is calculated from a different representation and bar of implementing the OPAM filters into Dune's condition language and then hashing that there is no good way of preserving the previous hashes (or running a hybrid approach of encoding them one way if they can and another if they cannot be represented using dune-lang conditions). I don't think we guarantee that the hashes are stable between versions of Dune.

Leonidas-from-XIV · 2024-09-16T15:22:40Z

I've replaced the failing test with one that shows that disjunctions in opam files lead to valid lock directory solutions using either side of the disjunction.

ElectreAAS · 2024-09-17T14:59:33Z

Oh nice! Thanks for updating the test

src/dune_pkg/local_package.mli

rgrinberg · 2024-10-10T15:29:10Z

src/dune_pkg/opam_solver.ml

-          let deps =
-            List.map pkg.dependencies ~f:(fun (d : Package_dependency.t) -> d.name)
-          in
+          let deps = Local_package.For_solver.dependency_names pkg in


Isn't this wrong? You should not consider packages that haven't been selected for the reachability check. This would mean that you're including packages in the lock directory that are not needed for the actual build. This is a good thing to add a test for as well.

Yes, you're completely right, thanks for pointing this out. This code needs to be changed because it uses the input to the solver as the output instead of using the solution that the solver outputs.

I'll add a test that checks that dependencies that don't get picked by the solver don't end up in the lock directory.

I'm looking what the semantics of reachable is and according to #10814 it is about removing post dependencies (and also post-deps-solving.t is the only test failing if I comment out the reachability test).

Since this is basically about filtering the solver output via the possible deps from the input, how about still collecting all possible packages (since they are potentially reachable) except those that are post and using that for reachability?

That way packages that the solver is not picking will not be part of the lock dir (as the solution just does not contain them) and post packages won't be picked either (as they will be filtered out by the reachability check). This makes post a bit special but post is already a magic variable in opam.

Added a test showing an unnecessary post dependencies being eliminated.

how about still collecting all possible packages (since they are potentially reachable) except those that are post and using that for reachability?

I think it's just simpler to do this without any hacks. We've already resolved the or deps when writing the dependency list in the lock directory. Might as well just use that here instead of the formula

In particular, I'm thinking of just using this snippet to evaluate the formula:

Resolve_opam_formula.filtered_formula_to_package_names ~with_test:false (add_self_to_filter_env opam_package (Solver_env.to_env solver_env)) version_by_package_name what

We already do this for external packages. No reason why we can't do it for local packages for the reachability check. You might want to wait until #11022 is merged though, as I'm going to move this snippet somewhere where it can be shared.

Ah, I missed the comment. Ok, I'll try to evaluate the formula instead.

Looking at the documentation of filtered_formula_to_package_names makes me question whether this is the right thing to use:

Given a map associating package names with the version of that package in a solution, this function evaluates an OpamFormula.t to a concrete list of package names all contained in the solution with versions which satisfy the formula, or an error if the the version constraints or packages in the formula can't be satisfied with the packages in the solution. If the formula contains disjunctions (the | operator in opam) then there may be multiple sets of packages that satisfy the formula. In this case the choice of which set to return is made arbitrarily.

This sounds to me that if the solver chooses one side of the disjunction and filtered_formula_to_package_names the other, this will lead to all the solver-selected legitimate dependencies being filtered out. Or, if I pass in the result from the solver as the package name map, the function will fail to find a solution.

This sounds to me that if the solver chooses one side of the disjunction and filtered_formula_to_package_names the other, this will lead to all the solver-selected legitimate dependencies being filtered out. Or, if I pass in the result from the solver as the package name map, the function will fail to find a solution.

If this is an issue, then it's already present with packages from opam repository. Working around it for local packages defined using the opam syntax is going to be an insufficient work around anyway.

But I think this isn't a huge issue. Rephrased less pessimistically, it tell us that solver can find at least one way to satisfy the disjunction. If there's only one way, we will find it. If there's more than one way, we will pick some arbitrary way - but it will still satisfy the formula. We're only planning to execute one build plan using this solution, so we indeed need only one solution.

I agree that It's rather unsatisfying that we can't tell the user there's more than one solution. I would really prefer to tell the user to write more constraints so that we don't have to choose things arbitrarily. But in the end, only one build plan is executed, and therefore only one side of any disjunction needs to be reachable.

rgrinberg · 2024-10-10T15:31:00Z

Looked over the approach again. I agree that emitting a dependency that wasn't selected for the hash check as an example isn't so bad. It's also an improvement to have the dependency hash reflect the formula. There's an issue introduced to the reachability check though. That one should most definitely only consider effective dependency sets. Doing otherwise would include useless packages in the lock dir

Leonidas-from-XIV · 2024-10-17T15:35:43Z

That one should most definitely only consider effective dependency sets. Doing otherwise would include useless packages in the lock dir

In my tests this seems to work, as the reachability is tested by filtering over a solver solution, so if the solver doesn't pick it, it isn't ever checked for reachability. That works even in the presence of post dependencies, the post dependency tests all pass.

rgrinberg · 2024-10-20T21:53:30Z

src/dune_pkg/dependency_formula.ml

+    Dune_sexp.List [ Dune_sexp.atom "or"; l; r ]
+;;
+
+let rec to_sexp v =


A bit of a shakem to introduce this much boilerplate. I just noticed we have some converters in Opam_dyn. How about we try using that instead of the sexp?

That works too, I've replaced it with converting to Dyn.t and hashing that. I currently hash it via to_string but maybe a nicer solution would be using Dyn.hash and converting the int into a hex digest?

The `Dependency_set.t` representation can't deal with disjunctions but in most cases that is not even necessary as the set gets turned into a `filtered_formula` again. Thus it might be easier to keep the original representation and implement the necessary dependency set functionality on top of that. Signed-off-by: Marek Kubica <marek@tarides.com>

Signed-off-by: Marek Kubica <marek@tarides.com>

Signed-off-by: Rudi Grinberg <me@rgrinberg.com> Signed-off-by: Marek Kubica <marek@tarides.com>

Signed-off-by: Marek Kubica <marek@tarides.com>

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg · 2024-11-03T18:05:55Z

LGTM. I just replaced the recursion with some existing opam library functions.

Leonidas-from-XIV added the package management label Sep 13, 2024

Leonidas-from-XIV requested review from ElectreAAS, gridbugs and rgrinberg September 13, 2024 14:25

ElectreAAS reviewed Sep 13, 2024

View reviewed changes

rgrinberg reviewed Sep 16, 2024

View reviewed changes

src/dune_pkg/local_package.ml Outdated Show resolved Hide resolved

rgrinberg reviewed Sep 16, 2024

View reviewed changes

src/dune_pkg/local_package.ml Outdated Show resolved Hide resolved

rgrinberg requested changes Sep 16, 2024

View reviewed changes

src/dune_pkg/local_package.ml Outdated Show resolved Hide resolved

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch from 3183e7e to 31229fb Compare September 16, 2024 13:10

Leonidas-from-XIV mentioned this pull request Sep 26, 2024

pkg: Failure on non-atoms in depends fields #10956

Closed

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch from b3969c7 to 5728b11 Compare October 10, 2024 13:25

rgrinberg reviewed Oct 10, 2024

View reviewed changes

src/dune_pkg/local_package.mli Outdated Show resolved Hide resolved

rgrinberg requested changes Oct 10, 2024

View reviewed changes

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch 2 times, most recently from 48312d3 to 6848f33 Compare October 17, 2024 15:06

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch from 8b2c551 to 4cfe9e4 Compare October 17, 2024 15:37

rgrinberg reviewed Oct 20, 2024

View reviewed changes

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch from 8c479b4 to 64ba323 Compare October 22, 2024 13:21

Leonidas-from-XIV force-pushed the filtered-formula-passthrough branch from ac42c54 to 408bd26 Compare November 1, 2024 15:37

Leonidas-from-XIV added 6 commits November 3, 2024 17:27

Remove unused Dependency_set

91e4293

Signed-off-by: Marek Kubica <marek@tarides.com>

Add a test showing that the disjunction in OPAM files is supported now

58b6ec5

Signed-off-by: Marek Kubica <marek@tarides.com>

Move filtered_formula into our own module

ad75b38

Signed-off-by: Marek Kubica <marek@tarides.com>

Determine the hash from the Sexp

c2e7c5d

Signed-off-by: Marek Kubica <marek@tarides.com>

Move reachability into the formula

d207526

Signed-off-by: Marek Kubica <marek@tarides.com>

Leonidas-from-XIV and others added 12 commits November 3, 2024 17:27

Add test for dependency formula changes

0ffe7f8

Signed-off-by: Marek Kubica <marek@tarides.com>

Clean up the awkward API

35b285d

Signed-off-by: Marek Kubica <marek@tarides.com>

Promote expected hash changes

1ec3f47

Signed-off-by: Marek Kubica <marek@tarides.com>

Update the test wording and show the difference

0ce2372

Signed-off-by: Marek Kubica <marek@tarides.com>

test(pkg): demonstrate unreachable packages being included

df39a55

Signed-off-by: Rudi Grinberg <me@rgrinberg.com> Signed-off-by: Marek Kubica <marek@tarides.com>

Do not include post dependencies in reachable packages

8e660c4

Signed-off-by: Marek Kubica <marek@tarides.com>

Replace sexp by dyn

8126edb

Signed-off-by: Marek Kubica <marek@tarides.com>

Promote expected hash changes

6502ef4

Signed-off-by: Marek Kubica <marek@tarides.com>

post deps are excluded now

22b2e7c

Signed-off-by: Marek Kubica <marek@tarides.com>

Simplify

222a27f

Signed-off-by: Marek Kubica <marek@tarides.com>

Use Resolve_opam_formula to determine dependencies

4c0018e

Signed-off-by: Marek Kubica <marek@tarides.com>

_

35a71e5

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg force-pushed the filtered-formula-passthrough branch from 24f3a62 to 440d328 Compare November 3, 2024 17:28

_

ce95b47

Signed-off-by: Rudi Grinberg <me@rgrinberg.com>

rgrinberg force-pushed the filtered-formula-passthrough branch from 972e02d to ce95b47 Compare November 3, 2024 17:44

rgrinberg merged commit b409963 into ocaml:main Nov 3, 2024

maiste mentioned this pull request Nov 4, 2024

dune dependency error with dune pkg lock #11096

Closed

Leonidas-from-XIV mentioned this pull request Nov 4, 2024

fix(pkg): handle nested [Or] in depopts #11090

Merged

Leonidas-from-XIV deleted the filtered-formula-passthrough branch November 4, 2024 16:08

Conversation

Leonidas-from-XIV commented Sep 13, 2024

Uh oh!

ElectreAAS left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Leonidas-from-XIV commented Sep 16, 2024

Uh oh!

Leonidas-from-XIV commented Sep 16, 2024

Uh oh!

ElectreAAS commented Sep 17, 2024

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rgrinberg Oct 22, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rgrinberg commented Oct 10, 2024

Uh oh!

Leonidas-from-XIV commented Oct 17, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rgrinberg commented Nov 3, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

rgrinberg Oct 22, 2024 •

edited

Loading