feat(pkg): solve all requested platforms together

[Alizter]

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.
• Credit: the cross-platform version-equality SAT encoding was proposed by @art-w in portable lock directories should pick the same version for cross-platform packages #13647.

Pre-feature tests

This change merges three independent draft test branches before applying the joint-solver implementation:

• test(pkg): cover a solvable portable platform set #16040 covers a solvable portable platform set.
• test(pkg): reproduce duplicate platform failures #16041 reproduces duplicate-platform failures.
• test(pkg): show avoid minimization is per-platform #16042 records per-platform avoid minimization.

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.
• 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.

Checks

• dune runtest test/blackbox-tests/test-cases/pkg/portable-lockdirs
• CI=true dune build @fmt @check

Closes #13647

[Alizter]

SAT solver benchmark

I benchmarked the stack against its pre-joint-solver baseline on the 10 real repositories used in the earlier LMDB benchmark: re, cohttp, jsoo, lsp, opam, irmin, mirage, eio, owl, and tezos.

As it currently stands, the joint solver has an approximately 2× slowdown in SAT-solving time. The geometric mean of the per-project new / baseline ratios is 2.013×. All 10 projects were slower; ratios ranged from 1.071× (Irmin) to 2.724× (opam).

Project	Baseline mean	Joint mean	Joint / baseline
re	65.7 ms	165.0 ms	2.511×
cohttp	402.4 ms	569.0 ms	1.414×
jsoo	27.1 ms	55.5 ms	2.047×
lsp	10.2 ms	21.1 ms	2.057×
opam	2.1 ms	5.7 ms	2.724×
irmin	166.7 ms	178.5 ms	1.071×
mirage	7.4 ms	16.2 ms	2.178×
eio	4.7 ms	12.3 ms	2.642×
owl	4.9 ms	11.6 ms	2.364×
tezos	18.3 ms	33.6 ms	1.839×

Method: baseline c58489c, joint-solver head ce68d06f, pinned opam repository and project revisions, 2 warmups plus 10 measured runs per project/revision, with versions interleaved. For each dune pkg lock, I summed the durations of all complete sat/solve trace events. This matters because the baseline normally emits four per-platform events while the joint solver emits one combined event.

The result measures time inside the SAT solver, not end-to-end lock-generation wall time. The reduced solve count is present, but the single combined solve currently costs more than the four baseline solves summed.

[Alizter]

Follow-up: end-to-end lock-generation time

An important clarification to the SAT-only results above: the joint solver is faster end-to-end, despite spending more time in the timed sat/solve section.

I reran baseline c58489c and joint-solver head ce68d06f on the same pinned inputs using fully source-built Dune binaries and measured complete dune pkg lock wall time. The joint implementation was faster on all 10 projects, with a geometric-mean 1.75× end-to-end speedup:

Project	Baseline lock time	Joint lock time	Speedup
re	0.473 s	0.243 s	1.95×
cohttp	0.947 s	0.546 s	1.73×
jsoo	0.411 s	0.248 s	1.66×
lsp	0.592 s	0.543 s	1.09×
opam	0.347 s	0.161 s	2.16×
irmin	1.116 s	0.717 s	1.56×
mirage	0.411 s	0.207 s	1.99×
eio	0.394 s	0.202 s	1.95×
owl	0.494 s	0.243 s	2.03×
tezos	0.681 s	0.416 s	1.64×

These were interleaved runs with one warmup and five measured observations per project/revision. The SAT regression is therefore real but does not translate into a user-visible lock-generation regression: the reduction in work outside the timed SAT section more than compensates for it.

[Alizter]

In a follow up change, we have the opportunity to share a lot of the traversal work that the combined solves do. This dramatically speeds up the solve times compared the cumulative solves. Therefore I don't think any of the performance differences highlighted here will be a serious issue.