Skip to content

Mitigate DNF explosion for depends field with disjoint disjunctions - #6831

Open
dra27 wants to merge 3 commits into
ocaml:masterfrom
dra27:less-dnf
Open

Mitigate DNF explosion for depends field with disjoint disjunctions#6831
dra27 wants to merge 3 commits into
ocaml:masterfrom
dra27:less-dnf

Conversation

@dra27

@dra27 dra27 commented Dec 8, 2025

Copy link
Copy Markdown
Member

I had a depends field enforcing an invariant for an little-known experimental branch of OCaml:

depends: [
  "conf-autoconf"         {build}
  "conf-which"            {build}
  "ocaml"                 {= "5.2.0" & post}
  "base-unix"             {post}
  "base-bigarray"         {post}
  "base-threads"          {post}
  "base-domains"          {post}
  "base-nnp"              {post}
  "ocaml-options-vanilla" {post}
  ("oxcaml-no-alcotest" {tpost} | "oxcaml-alcotest" {post})
  ("oxcaml-no-backoff" {post} | "oxcaml-backoff" {post})
  ("oxcaml-no-ctypes" {post} | "oxcaml-ctypes" {post})
  ("oxcaml-no-ctypes-foreign" {post} | "oxcaml-ctypes-foreign" {post})
  ("oxcaml-no-dot-merlin-reader" {post} | "oxcaml-dot-merlin-reader" {post})
  ("oxcaml-no-dune" {post} | "oxcaml-dune" {post})
  ("oxcaml-no-gen_js_api" {post} | "oxcaml-gen_js_api" {post})
  ("oxcaml-no-js_of_ocaml" {post} | "oxcaml-js_of_ocaml" {post})
  ("oxcaml-no-js_of_ocaml-compiler" {post} | "oxcaml-js_of_ocaml-compiler" {post})
  ("oxcaml-no-js_of_ocaml-ppx" {post} | "oxcaml-js_of_ocaml-ppx" {post})
  ("oxcaml-no-js_of_ocaml-toplevel" {post} | "oxcaml-js_of_ocaml-toplevel" {post})
  ("oxcaml-no-jsonrpc" {post} | "oxcaml-jsonrpc" {post})
  ("oxcaml-no-lsp" {post} | "oxcaml-lsp" {post})
  ("oxcaml-no-lwt_ppx" {post} | "oxcaml-lwt_ppx" {post})
  ("oxcaml-no-mdx" {post} | "oxcaml-mdx" {post})
  ("oxcaml-no-merlin" {post} | "oxcaml-merlin" {post})
  ("oxcaml-no-merlin-lib" {post} | "oxcaml-merlin-lib" {post})
  ("oxcaml-no-notty-community" {post} | "oxcaml-notty-community" {post})
  ("oxcaml-no-ocaml-compiler-libs" {post} | "oxcaml-ocaml-compiler-libs" {post})
  ("oxcaml-no-ocaml-index" {post} | "oxcaml-ocaml-index" {post})
  ("oxcaml-no-ocaml-lsp-server" {post} | "oxcaml-ocaml-lsp-server" {post})
  ("oxcaml-no-ocamlbuild" {post} | "oxcaml-ocamlbuild" {post})
  ("oxcaml-no-ocamlformat" {post} | "oxcaml-ocamlformat" {post})
  ("oxcaml-no-ocamlformat-lib" {post} | "oxcaml-ocamlformat-lib" {post})
  ("oxcaml-no-ojs" {post} | "oxcaml-ojs" {post})
  ("oxcaml-no-ppxlib" {post} | "oxcaml-ppxlib" {post})
  ("oxcaml-no-ppxlib_ast" {post} | "oxcaml-ppxlib_ast" {post})
  ("oxcaml-no-re" {post} | "oxcaml-re" {post})
  ("oxcaml-no-sedlex" {post} | "oxcaml-sedlex" {post})
  ("oxcaml-no-spawn" {post} | "oxcaml-spawn" {post})
  ("oxcaml-no-topkg" {post} | "oxcaml-topkg" {post})
  ("oxcaml-no-utop" {post} | "oxcaml-utop" {post})
  ("oxcaml-no-uutf" {post} | "oxcaml-uutf" {post})
  ("oxcaml-no-wasm_of_ocaml-compiler" {post} | "oxcaml-wasm_of_ocaml-compiler" {post})
  ("oxcaml-no-zarith" {post} | "oxcaml-zarith" {post})
]

opam switch create oxcaml ocaml-variants.5.2.0+ox completely falls over with this. The problem is the conversion to DNF which takes place in OpamFormula.packages.

While it's possible to re-encode this formula across more packages (which is the workaround I'm using), the conversion to DNF followed by filtering is sub-optimal.

The observation here is that in (X1 | X2) & (Y1 | Y2), there's no need to consider Y1 | Y2 if the atoms of Y1 | Y2 are distinct from the atoms of X1 | X2 combined (hopefully correctly) with the observation that if the entire sub-formula Y1 | Y2 doesn't refer to the specific package being filtered, then we don't need consider it when converting to DNF.

In example above, that means, say, that when considering which versions of the ocaml package to consider, all the disjunctions are eliminated, because the conversion to DNF cannot introduce formula of interest.

@dra27

dra27 commented Dec 8, 2025

Copy link
Copy Markdown
Member Author

(original code is in #2968)

@kit-ty-kate
kit-ty-kate self-requested a review December 8, 2025 13:47
@kit-ty-kate kit-ty-kate added this to the 2.6.0~alpha1 milestone Dec 8, 2025
@rjbou
rjbou self-requested a review December 8, 2025 13:47
dra27 and others added 3 commits July 14, 2026 21:38
A depends field of the form:

```
depends: [
  "foo"
  "bar"
  ("dep1" | "dep2")
  ("dep3" | "dep4")
]
```

is very large in DNF. However, when computing OpamFormula.packages, the
resulting formula will be reduced on a package-by-package basis. By
pre-processing the formula package-by-package, it's instead possible to
capitalise on this pattern and eliminate unrelated sub-formulae before
converting to DNF.
@kit-ty-kate

Copy link
Copy Markdown
Member

I've rebased it on master and added a factorisation in a separate commit because this code pattern is present elsewhere. I noticed it while looking at this part of the code the other day on a performance debugging stroll.

Now, while the code change looks reasonable, it isn't exactly trivial either and i'd like to have some tests to see what exactly blows up and if there are some performance regression when giving other types of formulas if any.
Sadly this does take time and i won't have time to do that in the remaining time before the 2.6.0~alpha1 release so i'm bumping that to the 2.7 milestone.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants