Diagnostics should explain steering surprises: why a resolve was held back to an older julia (or package) version

[StefanKarpinski]

Build plan. Rewritten 2026-09-09 as a handoff against main at d59bcd2. The comments below are history: the two 2026-08-17-and-earlier implementation sketches describe architectures that have since been replaced, and should be read for motivation only. This body is the current statement of what to build.

The problem

A user compat bound on a non-upgradable stdlib steers the julia choice: a julia version is compatible with exactly the stdlib versions it bundles, so a stale [compat] LinearAlgebra = "~1.10" quietly pins the whole toolchain to julia 1.10. The resolution is correct. Nothing says why.

Measured instance in the first comment below: a project with julia = "1.6" and LinearAlgebra = "~1.10" resolves julia to 1.10.11 rather than 1.12.6, and the only signal the user gets is a ⊼ character (bin/resolve.jl:774).

This is the last asymmetry in the diagnostics story. An unsatisfiable resolve now gets a machine-verified proof per conflict, complete coverage of the cheapest fixes, and a per-action answer for every fix it does not offer. A satisfiable but surprising resolve gets one character.

Scope note: the surprise only exists when resolving over julia versions. Pkg pins julia to the running version by default, where the same stale bound produces an ordinary unsatisfiable resolve. But #62 names holdbacks as the mechanism for the version half of pkg> why — "why is X at 1.2 and not 1.9" — which is not julia-specific and is a headline Pkg feature.

Prior art — a spec, not a patch

archive/holdbacks-prototype (commit c9e8b0c, "explain resolutions that succeeded and still surprised") is a complete prior implementation: src/Holdback.jl (361 lines), test/holdback.jl (230 lines), plus bin/resolve.jl wiring and docs. It settles a lot of design and is worth reading in full.

It cannot be ported. It targets src/Diagnose.jl and a Fact/UserCompat/Bound vocabulary that #105 replaced with clauses, and — the trap — its tests assert wording that has since been retired:

prototype asserts	current idiom
your compat restricts Stats to 10	your compat leaves Stats 10
julia 12 works with Stats only at 12	directed verbs read off the consequent: requires / constrains / leaves no version of

The symmetric "works with … only at" phrasing is exactly what #105 replaced, because a bound has no direction and which way it is said has to be chosen when printed (src/Diagnostics.jl:2154). Copy those assertions and you reintroduce two dead vocabularies. Take the prototype's structure and edge cases; re-derive every string.

Two sibling commits on the same branch are prior art for other roadmap items, not for this one: 1539af3 (goals) and 3993297 (the presentation toolkit and --explain). Same caveat applies to both.

What to build

For a package p that resolved at class rank r when a better rank exists:

1. Probe. Assume p at a better rank on the solved instance. Satisfiable → nothing to explain. Unsatisfiable → continue.
2. Blame. Take a held-fixed MUS over the selector vocabulary — sat_mus(satx, fixed, selectors), the same call reason_core makes at src/Diagnostics.jl:1649. The result names the responsible statements as clauses.
3. Render. Those clauses print through the existing clause_phrase / range_phrase path, so a holdback's lines read in the same idiom as a conflict's and no new sentence layer is needed.
4. Verify the fix. Re-resolve the relaxation on the universe already filtered for the query — licensed by Relaxation-stable filtering: a filtered universe serves every relaxation of its query #75's Theorem C, and the same route conflict fixes use. The witness is the optimal resolution under the fix, so it is as honest as an UNSAT fix's.

Everything in steps 1–4 exists and is tested. This is assembly, not new machinery.

Decisions to make first

None of these is settled, and each shapes the code:

1. Which packages get probed. julia always? every requirement resolved below its best? everything? behind a flag? A probe is a solve, so this is a cost decision as well as a UX one. The prototype's answer was max_probes = 8 with an explicit truncation line — see (4).
2. Output shape. Is a holdback Conflict-shaped — heading, Lines, a Fix with Actions — reusing action_phrase and printing inside the diagnosis? Or its own type printed beside it? The first buys the proof checker for free (see below); the second is easier to keep out of the unsatisfiable path.
3. Entry point. The prototype's was holdbacks(info, prob, sol, [pkgs]; by, max_probes). Does resolve surface them on success, or does a caller ask separately? Pkg integration checklist: conventions, API mapping, rollout #62 needs an answer to write Pkg code against.
4. Truncation honesty. The prototype printed (7 more packages resolved below their best version, not examined). That is the shape of footer drop "There may be more to say about some of these." #108 just removed, on State the whole theory of explaining an unsatisfiable resolve #104's principle that the page owes only what can be acted on. There is now a precedent, and it may cut against the prototype: consider recording the count on the returned value and printing nothing.

Verification — free, if the output is clause-shaped

test/proof_check.jl exports lines_are_true, chain_is_a_proof, proof_problems, claimed_lines and friends, and lines_are_true(sat, prob, clauses) is generic over clauses. If a holdback's lines are clauses over the same instance, they are proof-checked with no new checker: every line true of the universe the query left, and the claimed set contradictory.

That is a strong argument for decision (2) landing on "Conflict-shaped".

Harnesses to extend: test/proof_check.jl (the checker itself needs nothing), test/chain_coverage.jl (add holdback probes to the corpus loop), test/diagnostics.jl (report wording). The prototype's test/holdback.jl is the scenario list to port — STEERING and its siblings — with every occursin string rewritten.

Where things are

• src/Diagnostics.jl — the diagnosis layer; reason_core (1729) and the selector plumbing (1793) are the models to follow.
• src/UnsatCores.jl — sat_mus, including the held-fixed form (135).
• src/Clauses.jl — the clause algebra and the sentence layer.
• docs/src/theory/unsat-explanation.md — the contract a report owes. A holdback is subject to it.
• bin/resolve.jl — the ⊼ marker (774) is the current signal; the prototype added --explain and automatic julia explanation here.
• Docs target moved: the prototype wrote docs/src/diagnostics.md, which no longer exists. Docs are now index.md, api.md and theory/.

Definition of done

• Holdbacks are computed, blamed, rendered and fix-verified for the measured steering instance and for the prototype's scenario set.
• Every printed line passes lines_are_true against the instance the resolve ran on.
• The truncation decision from (4) is implemented and consistent with drop "There may be more to say about some of these." #108.
• bin/resolve.jl explains a held-back julia without being asked; the rest is behind a flag.
• docs/src/api.md documents whatever is public.

---

🤖 Rewritten as a handoff with Claude Code.

[StefanKarpinski]

Concrete measured instance of the surprise, from the #51 implementation (steering semantics now in place there):

Project with [compat] julia = "1.6", LinearAlgebra = "~1.10", JSON = "0.21", julia unbounded:

before:  julia 1.12.6      LinearAlgebra 1.12.0   (stdlib bound silently ignored)
now:     julia 1.10.11 ⊼   LinearAlgebra 1.10.11  (stdlib bound steers julia)

The stale ~1.10 entry overrides the project's own julia = "1.6" intent without a word — the ⊼ marker on the julia line is currently the only signal. Scope note: caret bounds (what pkg> compat generates) only push julia forward; only tilde/exact/range upper bounds can pull it backward, which bounds how often this bites in the wild. The diagnostic this issue asks for should name the responsible bound, e.g. "julia held back to 1.10.11 by your compat on LinearAlgebra (~1.10); relaxing it allows julia 1.12.6."

[StefanKarpinski]

Still open and still wanted; updating the implementation sketch, which was written against an architecture that has since been replaced.

What now exists that this can be built on (all merged): #71 class space, #72 the relaxation substrate, #75 relaxation-stable filtering, #76 answering a relaxation on the universe already filtered for the query, and #73 the UNSAT diagnosis itself (Diagnosis, conflicts, verified fixes).

The sketch above is out of date in one specific way. It says user constraints are "selector-guarded in the instance" and that the failed-assumption core over user-constraint selectors names the responsible constraints. That was #49's design. In class space a user constraint does not appear in the instance as a guarded clause at all — it empties classes, and the emptied classes are asserted as unit literals inside a deactivation frame. The diagnosis machinery correspondingly asks its questions as assumptions over per-package literals (with_classes_relaxed + with_emptied_packages in src/Diagnostics.jl), not over constraint selectors.

So the holdback probe translates to: for a package p resolved at class rank r, assume p at a better rank on the solved instance; if that is UNSAT, minimize over the same [req_lits; pkg_lits] vocabulary #73 already uses, and the resulting MUS names the requirements and emptied packages responsible. Verification reuses #73's route — resolve the relaxation on the universe already filtered for the query, which #75's Theorem C licenses.

That is a strictly easier build than the original sketch: the vocabulary, the minimizer, the frame discipline and the fix-verification path all exist and are tested.

Unchanged from the original: the honest observation that this surprise only exists when resolving over julia versions, and that deciding which packages merit a probe (julia always? every non-best requirement? behind a flag?) is a UX question rather than a solver one.

[StefanKarpinski]

Still unstarted on main (d59bcd2) — holdbacks exists only on an unmerged branch — but the 2026-08-17 sketch needs one more revision, because the diagnosis layer it was written against has since been rebuilt by #104/#105/#107.

What changed under it. That sketch says to minimize over the [req_lits; pkg_lits] vocabulary and take the MUS. The report is no longer built that way: #105 made the registry's own statements assumable via selector-instrumented instances, and the explanation is a set of clauses over Resolver.Clauses with an n-ary resolution rule, checked line-by-line against the instance the failed resolve ran on. A holdback story built on the old vocabulary would produce facts the current checker has no way to verify, and would print in a different idiom from every other report.

Restated for the current layer. For a package p resolved at class rank r: assume p at a better rank on the solved instance; if UNSAT, the held-fixed MUS over the selector vocabulary names the responsible statements directly as clauses, and they render through the same clause_phrase path as a conflict's lines. Verification is unchanged — resolve the relaxation on the universe already filtered for the query (#75, Theorem C).

This is easier than either previous sketch, not harder: the machinery a holdback needs is exactly the machinery a conflict already uses, and test/proof_check.jl would check a holdback's lines with no changes.

Unchanged. The surprise only exists when resolving over julia versions, which Pkg does not do by default; and which packages merit a probe (julia always? every non-best requirement? behind a flag?) is still a UX question, not a solver one.

Why it matters more than the "surprising resolve" framing suggests. #62 names holdbacks as the mechanism for the version half of pkg> why — "why is X at 1.2 and not 1.9". That is a headline Pkg feature, and it is blocked on this issue plus goals.

---

🤖 Triaged with Claude Code.