feat(pkg): single solve for all platforms#14458
Draft
Alizter wants to merge 14 commits into
Draft
Conversation
Alizter
force-pushed
the
single-solve
branch
4 times, most recently
from
f3452d2 to
4a120fb
Compare
Introduce a new Sat trace category (opt-in via DUNE_TRACE=+sat, since the overhead is real and most users only want high-level solver visibility). Add cumulative num_decisions and num_conflicts counters to the SAT engine, plus Sat.stats and Sat.get_stats to expose them. The counters are incremented in run_solver's decision branch and conflict branch respectively; num_variables is reported as the length of the current problem's variable list. Emit a sat/solve complete event in opam_solver.do_solve around Sat.run_solver, carrying num_variables, num_decisions and num_conflicts in the args. With the event being a complete event (start + dur), the trace consumer can see how much SAT work each invocation did and how long it took, alongside the solver's structural metrics. Per-do_solve emission means callers that loop the solver (e.g. max_avoids tuning) produce one event per attempt, which is the right granularity for observing iterative-solver behaviour. Signed-off-by: Ali Caglayan <alizter@gmail.com>
Opt-in Sat tracing (via DUNE_TRACE=+sat) on the relevant dune pkg lock invocations in five existing solver tests, and dump each SAT invocation's args (num_variables, num_decisions, num_conflicts). This turns the tests into structural probes that surface SAT-engine work, not just pass/fail. - portable-lockdirs/portable-lockdirs-basic.t: 4 SAT runs at the current per-platform parallel baseline; small problem (no decisions). - portable-lockdirs/portable-lockdirs-platform-dependant-version.t: 4 SAT runs producing the divergent per-platform solution that will become a hard error once cross-platform version equality lands. - portable-lockdirs/portable-lockdirs-no-solution.t: failure path runs the iterative do_solve recursion (max_avoids tuning + diagnostics) producing 12 events with varying decision counts. - lockdir-load-dedup.t: zero SAT runs on a prebuilt-lockdir build path. - lock-directory-selection.t: one SAT run (per-invocation trace reset shows only the last pkg lock). Add a satSolveEvents jq helper in dune.jq that selects events in the sat category. Tests will surface refactor-by-refactor changes in solver work as the chain progresses. Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
…lving Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Prepares solver diagnostics for the multi-platform world where the same package appears once per platform: deduplicates dependency lists, roles, components, and impls by package name when rendering diagnostics. Also collapses the redundant VirtualImpl rendering on the single-platform side (visible in conflict-class.t: "foo&x" is no longer printed after "foo.dev x.dev" since the VirtualImpl has no new deps). Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Implement part 2 of art-w's plan from ocaml#13647: introduce somewhere:<pkg>:<ver> SAT variables and clauses ensuring that every platform that selects a package selects the same version. Replaces the post-solve version-conflicts check (which raised User_error on inconsistent selections) with a SAT-level constraint, so the solver itself searches for a consistent version rather than failing on the first inconsistent assignment. For each (Package_name, Package_version) appearing as an impl on any platform, a fresh "somewhere" SAT variable is added. Two kinds of clauses: 1. impl_var (name, version, platform) implies somewhere(name, version) 2. at_most_one(somewhere(name, *)) across versions of [name] The reverse implication is deliberately omitted, so platforms may still omit a package entirely (e.g. unix-only packages on Windows). Signed-off-by: Ali Caglayan <alizter@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Based on work done with @art-w earlier this year.