From 472da326e54297a05cbdda9ec900cfd9ade70e23 Mon Sep 17 00:00:00 2001 From: David Allsopp Date: Mon, 8 Dec 2025 12:18:48 +0000 Subject: [PATCH 1/3] Don't compute dependency cone when not needed --- src/state/opamSwitchState.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/state/opamSwitchState.ml b/src/state/opamSwitchState.ml index 4ccf61d68f4..d2388ffaf42 100644 --- a/src/state/opamSwitchState.ml +++ b/src/state/opamSwitchState.ml @@ -1054,13 +1054,15 @@ let universe st OpamPackage.Map.find nv u_depopts ]) |> OpamFormula.packages st.packages in - let requested_deps = - OpamPackage.Set.fixpoint resolve_deps requested_allpkgs - in - requested_deps %% Lazy.force st.reinstall ++ - match reinstall with - | Some set -> set - | None -> OpamPackage.Set.empty + let reinstall = Option.value ~default:OpamPackage.Set.empty reinstall in + let lazy switch_reinstall = st.reinstall in + if OpamPackage.Set.is_empty switch_reinstall then + reinstall + else + let requested_deps = + OpamPackage.Set.fixpoint resolve_deps requested_allpkgs + in + requested_deps %% Lazy.force st.reinstall ++ reinstall in let missing_depexts = lazy ( From 7c77ae6d833cd847960181b97b7540b31645425b Mon Sep 17 00:00:00 2001 From: David Allsopp Date: Mon, 8 Dec 2025 12:19:04 +0000 Subject: [PATCH 2/3] Mitigate DNF in depends formula 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. --- master_changes.md | 1 + src/format/opamFormula.ml | 47 ++++++++++++++++++++++++++++++--------- 2 files changed, 38 insertions(+), 10 deletions(-) diff --git a/master_changes.md b/master_changes.md index 28d0eb9cb92..3ee4aa2ba3c 100644 --- a/master_changes.md +++ b/master_changes.md @@ -163,6 +163,7 @@ users) * Fix a rare potential GC corruption in `OpamStubs.uname` [#6880 @avsm @kit-ty-kate @andrew] * Fix a rare potential GC corruption in `OpamStubs.enumRegistry` on Windows [#6882 @kit-ty-kate] * Remove uses of `Stdlib.ignore` [#6481 @rjbou @kit-ty-kate] + * Mitigate potential exponential blow-up converting dependency formulae to DNF [#6831 @dra27] ## Internal: Unix diff --git a/src/format/opamFormula.ml b/src/format/opamFormula.ml index 9fc4827efc4..34abd32fd2d 100644 --- a/src/format/opamFormula.ml +++ b/src/format/opamFormula.ml @@ -412,22 +412,49 @@ let all_names f = OpamPackage.Name.Set.empty f let packages pkgset f = - let names = all_names f in - (* dnf allows us to transform the formula into a union of intervals, where - ignoring atoms for different package names works. *) - let dnf = dnf_of_formula f in OpamPackage.Name.Set.fold (fun name acc -> - (* Ignore conjunctions where [name] doesn't appear *) - let name_formula = - map (fun ((n, _) as a) -> if n = name then Atom a else Empty) dnf + let is_name (n, _cstr) = OpamPackage.Name.equal n name in + let formula_or_empty cond f = if cond then f else Empty in + (* Determine if nv could possibly part of the solution for [f]. This + means checking that either [v] satisfies the constraints on name. + This is done by converting [f] to DNF, which allows us to transform + the formula into a union of intervals, where ignoring atoms for + different package names works. We can then ignore conjunctions + where [name] doesn't appear. However, this function is typically + used on a dependency formula, which is most normally a large + conjunction. We capitalise on this with a peephole simplification, + observing that if we're testing for package name A in the formula + [X & Y], then we can ignore X if it doesn't contain A (and likewise + Y). This eliminates unrelated sub-formula from the top-level + conjunction, in particular it means that + [Dep1 & Dep2 & (Dep3 | Dep4) & (Dep5 | Dep6)] does not cause + trigger worst-case expansion for DNF. *) + let rec simplify_formula f = + match f with + | Empty -> Empty + | Atom atom -> + formula_or_empty (is_name atom) f + | Block b -> + formula_or_empty (exists is_name b) f + | Or(a, b) -> + formula_or_empty (exists is_name a || exists is_name b) f + | And(a, b) -> + let a = simplify_formula a in + let b = simplify_formula b in + make_and a b + in + let f = + f + |> simplify_formula + |> dnf_of_formula + |> map (fun a -> formula_or_empty (is_name a) (Atom a)) in OpamPackage.Set.union acc @@ OpamPackage.Set.filter (fun nv -> let v = OpamPackage.version nv in - eval (fun (_name, cstr) -> check_version_formula cstr v) - name_formula) + eval (fun (_name, cstr) -> check_version_formula cstr v) f) (OpamPackage.packages_of_name pkgset name)) - names OpamPackage.Set.empty + (all_names f) OpamPackage.Set.empty (* Convert a t an atom formula *) let to_atom_formula (t:t): atom formula = From 62822c314fbbea9e100125987fe5006eac22fe9d Mon Sep 17 00:00:00 2001 From: Kate Date: Tue, 14 Jul 2026 21:21:01 +0100 Subject: [PATCH 3/3] factorise OpamFormula.verify by moving the duplicated code to its own function --- src/format/opamFormula.ml | 81 +++++++++++++++++++-------------------- 1 file changed, 39 insertions(+), 42 deletions(-) diff --git a/src/format/opamFormula.ml b/src/format/opamFormula.ml index 34abd32fd2d..a5c5c12174b 100644 --- a/src/format/opamFormula.ml +++ b/src/format/opamFormula.ml @@ -396,15 +396,47 @@ let dnf_of_formula t = | And (x,y) -> mk_right (mk x) (mk y) in mk t -let verifies f nv = - let name_formula = - map (fun ((n, _) as a) -> if n = OpamPackage.name nv then Atom a else Empty) - (dnf_of_formula f) +let name_formula name f = + let is_name (n, _cstr) = OpamPackage.Name.equal n name in + let formula_or_empty cond f = if cond then f else Empty in + (* Determine if nv could possibly part of the solution for [f]. This + means checking that either [v] satisfies the constraints on name. + This is done by converting [f] to DNF, which allows us to transform + the formula into a union of intervals, where ignoring atoms for + different package names works. We can then ignore conjunctions + where [name] doesn't appear. However, this function is typically + used on a dependency formula, which is most normally a large + conjunction. We capitalise on this with a peephole simplification, + observing that if we're testing for package name A in the formula + [X & Y], then we can ignore X if it doesn't contain A (and likewise + Y). This eliminates unrelated sub-formula from the top-level + conjunction, in particular it means that + [Dep1 & Dep2 & (Dep3 | Dep4) & (Dep5 | Dep6)] does not cause + trigger worst-case expansion for DNF. *) + let rec simplify_formula f = + match f with + | Empty -> Empty + | Atom atom -> + formula_or_empty (is_name atom) f + | Block b -> + formula_or_empty (exists is_name b) f + | Or(a, b) -> + formula_or_empty (exists is_name a || exists is_name b) f + | And(a, b) -> + let a = simplify_formula a in + let b = simplify_formula b in + make_and a b in - name_formula <> Empty && + simplify_formula f + |> dnf_of_formula + |> map (fun a -> formula_or_empty (is_name a) (Atom a)) + +let verifies f nv = + let f = name_formula (OpamPackage.name nv) f in + f <> Empty && eval (fun (_name, cstr) -> check_version_formula cstr (OpamPackage.version nv)) - name_formula + f let all_names f = fold_left (fun acc (name, _) -> @@ -413,42 +445,7 @@ let all_names f = let packages pkgset f = OpamPackage.Name.Set.fold (fun name acc -> - let is_name (n, _cstr) = OpamPackage.Name.equal n name in - let formula_or_empty cond f = if cond then f else Empty in - (* Determine if nv could possibly part of the solution for [f]. This - means checking that either [v] satisfies the constraints on name. - This is done by converting [f] to DNF, which allows us to transform - the formula into a union of intervals, where ignoring atoms for - different package names works. We can then ignore conjunctions - where [name] doesn't appear. However, this function is typically - used on a dependency formula, which is most normally a large - conjunction. We capitalise on this with a peephole simplification, - observing that if we're testing for package name A in the formula - [X & Y], then we can ignore X if it doesn't contain A (and likewise - Y). This eliminates unrelated sub-formula from the top-level - conjunction, in particular it means that - [Dep1 & Dep2 & (Dep3 | Dep4) & (Dep5 | Dep6)] does not cause - trigger worst-case expansion for DNF. *) - let rec simplify_formula f = - match f with - | Empty -> Empty - | Atom atom -> - formula_or_empty (is_name atom) f - | Block b -> - formula_or_empty (exists is_name b) f - | Or(a, b) -> - formula_or_empty (exists is_name a || exists is_name b) f - | And(a, b) -> - let a = simplify_formula a in - let b = simplify_formula b in - make_and a b - in - let f = - f - |> simplify_formula - |> dnf_of_formula - |> map (fun a -> formula_or_empty (is_name a) (Atom a)) - in + let f = name_formula name f in OpamPackage.Set.union acc @@ OpamPackage.Set.filter (fun nv -> let v = OpamPackage.version nv in