fix(pkg): make lock platform selection unambiguous - #16172
Draft
Alizter wants to merge 1 commit into
Draft
Conversation
Alizter
force-pushed
the
push-skuosxuzqvlw
branch
from
August 24, 2026 13:01
3e11b4b to
2c86465
Compare
Alizter
marked this pull request as ready for review
August 24, 2026 14:58
Alizter
force-pushed
the
push-skuosxuzqvlw
branch
from
August 24, 2026 15:02
2c86465 to
41c3196
Compare
Alizter
force-pushed
the
push-skuosxuzqvlw
branch
from
August 24, 2026 16:03
41c3196 to
c98b3b6
Compare
Alizter
marked this pull request as draft
August 24, 2026 16:26
Alizter
force-pushed
the
push-skuosxuzqvlw
branch
4 times, most recently
from
August 25, 2026 11:51
3027aa1 to
2019e18
Compare
Reject variable names that appear in more than one of solver_env, unset_solver_vars, and an explicitly configured solve_for_platforms environment. For valid lock stanzas, apply each context's solver_env and unset_solver_vars when selecting conditional package fields, computing package digests, and comparing dev-tool compiler packages instead of using only the host environment. Signed-off-by: Ali Caglayan <alizter@gmail.com>
3 tasks
Alizter
force-pushed
the
push-skuosxuzqvlw
branch
from
August 25, 2026 13:00
2019e18 to
2ed6491
Compare
Alizter
added a commit
that referenced
this pull request
Aug 26, 2026
## Summary - Build one SAT universe containing every requested platform instead of solving each platform independently. - Make roles, availability, conflict classes, and result extraction platform-aware. - Constrain every platform role for a package to select the same version, choosing an older common version when necessary and failing when no common version exists. - Resolve each platform's package formulas against only the packages selected on that platform, preserving platform-specific dependency alternatives. - Generate conditional lock-file data directly from the joint result and remove obsolete result-merging APIs. - Keep diagnostics origin-aware: repository pre-rejections are reported only for repository-backed roles, and failures affecting a subset of requested platforms retain their platform qualifiers. - Remove the unreachable warning path for non-boolean availability filters, which are treated as unavailable. - Credit: the cross-platform version-equality SAT encoding was proposed by @art-w in #13647. This branch is rebased on `main` after #16210 landed. It does not include #16172 or #16173. ## Landed preparation The following independent preparatory PRs have landed on `main`. ### Observability and solver invariants - #15923 adds the opt-in SAT trace category and `sat/solve` statistics. - #15961 records solve counts and statistics in the existing solver tests. - #15962 snapshots all-or-nothing failure, deduplicated manifest errors, and the legacy per-platform version divergence. - #15981 makes portable lock-directory generation all-or-nothing before changing the solver architecture. ### Per-platform semantics - #15998 preserves per-platform dependency-alternative selections. - #15999 preserves platform filters in local package constraints. - #16000 preserves platform-specific rejection reasons. - #16001 records legacy per-platform version selection. - #16002 covers extra files when platforms converge on a common version. - #16003 preserves the single-platform SAT problem size. - #16009 preserves legacy dependencies whose names overlap formula constructors. - #16010 preserves platform-local conflict-class diagnostics. ### Joint-solve edge cases - #16040 covers a solvable portable platform set. - #16041 reproduces duplicate-platform failures. - #16042 records per-platform avoid minimization. - #16057 preserves platform-specific alternatives selected for local package dependencies. - #16058 ignores malformed repository versions excluded by local constraints. - #16084 preserves post-dependency reachability independently for each platform. - #16210 records per-platform diagnostic behavior for one-of-many and two-of-four failures, platform-dependent pin availability, repository versions shadowed by pins, and non-boolean availability filters. ### Build and tool integration - #16167 snapshots host-platform package selection in build contexts. - #16168 covers dev-tool compiler-package relocking and lock reuse. - #16169 snapshots the former precedence between explicit `solve_for_platforms` entries and conflicting lock-stanza solver variables. ## Independent related fixes The following sibling PRs are based directly on `main` and are not dependencies of this PR: - #16172 rejects solver variables repeated across lock-stanza environment fields and honors valid lock-stanza environments during package builds. - #16173 compares project and dev-tool compiler packages semantically, avoiding unnecessary relocking while preserving same-version recipe-change detection. ## Review fixes - Compute post-solve reachability separately for every platform before taking the union, so a local package's macOS alternative is not dropped after its Linux alternative is visited first. - Keep versions rejected on every platform out of manifest loading, while retaining platform-local candidates needed by another platform. - Do not attach repository pre-rejections to local or pinned roles, whose repository versions are not candidates. - Preserve platform annotations whenever a failure affects fewer than all requested platforms, including identical failures on two of four platforms. - Report cross-platform version conflicts with the selected version and platform instead of an opaque SAT clause. - Rename and rewrite the no-common-version regression so its name and prose match the enforced invariant. - Remove the redundant platform-version extra-files regression at the commit where joint version equality makes it obsolete. - Avoid constructing a discarded non-portable platform input and remove the unreachable non-boolean availability warning. ## Checks - `dune runtest test/blackbox-tests/test-cases/pkg/portable-lockdirs` - `CI=true dune build @fmt @check` Closes #13647
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
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.
Description
Make the environment used for lock solving and package builds unambiguous.
When
solve_for_platformsis explicitly configured, variable names insolver_env,unset_solver_vars, and the requested platform environments must be pairwise disjoint. This applies to every variable name and rejects repeated identical values as well as conflicting values.For each dependency build context, use the selected lock stanza's effective
solver_envandunset_solver_varswhen selecting conditional package fields, computing package digests, and comparing dev-tool compiler packages instead of using only the host environment.Relationship to other package changes
This PR is based directly on
main. It is independent of the joint-platform solver in #15982 and the semantic compiler-package comparison in #16173; all three can be reviewed and landed independently.Regression coverage
solver_envpreviously ran the package's Linux build command; this PR makes it run the macOS command.solver_envandsolve_for_platformsoverlap precursor; that formerly accepted precedence is now rejected as ambiguous.unset_solver_varsandsolve_for_platforms.Checklist