Roadmap: what is done, what is next, and what is waiting on evidence

[StefanKarpinski]

The agreed sequencing, kept here so the order lives somewhere findable. One-line rationale each; details in the linked issues.

Current as of main at a595e04 (2026-09-12).

Where this stands

The resolver and its diagnostics are complete. What is left is not core work: it is a cache, two query forms, and the mechanics of shipping.

• Resolve — layered descent over interchangeability classes, lexicographic optimality against a per-package preference order, relaxation-stable filtering. Done and heavily differential-tested.
• Explain a failure — a machine-verified proof per conflict, complete coverage of the cheapest fixes, blocked fixes answered individually. Done (State the whole theory of explaining an unsatisfiable resolve #104/Explain an unsatisfiable resolve by the book #105/Name a repeated conflict by what tells it apart #106/Cover the cheapest fixes by exact products, one conflict per leading menu #107).
• Explain a success — why a package landed below its best, and what to relax. Not started (Diagnostics should explain steering surprises: why a resolve was held back to an older julia (or package) version #52).
• Answer a hypothetical — "what if I had X", "what does avoiding X cost". Not started (goals).
• Be fast from cold — no cache exists, so a repeated resolve of the same closure re-parses it. Not started (T1 persistence: save/load/invalidate the universal registry cache (implementation plan) #55), and measured as a modest win rather than a critical one: a resolve is as lazy as Pkg's and touches 443–822 packages of ~14,000.

What is open, in full

Short enough now to list. Everything else is closed.

Umbrella	#62 Pkg integration · #64 this roadmap
Explaining a success	#52 holdbacks · #112 goals · #113 toolkit and --explain
Performance	#55 persistence — modest, and evidence-gated
Blocked	#63 multi-hop holdback stories, behind #52

The three explanation issues are one feature between them: pkg> why needs goals for presence answers and holdbacks for version answers, and the toolkit is how Pkg renders either in its own voice.

Done

Everything through #116. The load-bearing ones, newest first:

• Start the descent from the best class the query admits #115 — start the descent from the best class the query admits. Closes Constrained resolves: teach the descent to skip user-excluded versions #60. A constrained resolve no longer probes classes the query has already emptied; the instance also counts its own solves now, which is the instrument that issue had been asking for.
• Make bin/ resolve on Julia 1.13 #116 — Julia 1.13. bin/ resolves on it, with a manifest of its own and the stdlib check extended to cover it. The staleness guards from Fix stale stdlib snapshot, and notice the next one (#103) #110 did their job: the missing manifest was reported rather than silently falling back to 1.9's pins.
• Ask upstream for the release that would fix a conflict #114 — ask upstream for the release that would fix a conflict. A conflict may now name a maintainer request, under a bar high enough that the sentence is sendable as it stands: a hypothetical release modelled in place (Lemma 32), three qualification conditions, and a verified witness. Deliberately scoped to bounds meeting the user's own constraint — one release, one bound, one addressee — so it never judges which of two maintainers is at fault.
• Cover the cheapest fixes by exact products, one conflict per leading menu #107 — cover the cheapest fixes by exact products. Tree-driven factoring of the cheapest-repair family; each block covered by generalized rectangles, exactness and completeness asserted per report. Retired the cross-product residue.
• Explain an unsatisfiable resolve by the book #105 — explain an unsatisfiable resolve by the book. The diagnosis rebuilt on State the whole theory of explaining an unsatisfiable resolve #104's theory: every printed sentence is a named fix or a solver-decided fact, licensed coarsening for wide cores, blocked fixes answered per tempting action.
• State the whole theory of explaining an unsatisfiable resolve #104 — the whole theory of explaining an unsatisfiable resolve. One self-contained theory page, twenty-one numbered results with proofs. Settled the contract: reports owe machine-verified accuracy and a visible contradiction, not a hand-checkable derivation — which is why The unsatisfiability report must be a valid proof, and is not #100 closed as superseded rather than as four fixes.
• Name a repeated conflict by what tells it apart #106, End a conflict's story where its own facts are #98, Make a conflict read as a syllogism #96, Say why one package matters to another #86 — the report as an argument. A conflict reads as a syllogism, names why one package matters to another, ends where its own facts are, and is told apart from its repeats.
• Keep dominated versions beside the class that dominates them #90 — shadows. Dominated versions are kept beside the class that dominates them, so a report can speak about versions redundancy elimination removed. Also the premise Redundancy is conservative for relaxations' sake; shadows might let it be aggressive #91 is waiting on.
• Present minimal fixes as a factored product of independent choices #84, Diagnosis: present minimal fixes as a factored product of independent choices #83 — minimal fixes as a factored product of independent choices, replacing the product-of-all-conflicts menu that hit its cap in a quarter of failing queries.
• Test and document weak dependency semantics #82 — weak dependencies and extensions. Closes Weak dependencies and extensions: model them #61. This was the last parity gap with Pkg's closure other than persistence.
• One map, one constraint type #79, Rename the one-argument is_satisfiable to sat_solve #81 — the API surface settles. Constraints are one map keyed by kind (:compat, :pin, custom); issatisfiable is the exported spelling and sat_solve is the internal one-argument form.
• Diagnose an unsatisfiable resolve #73, Relaxation-stable filtering: a filtered universe serves every relaxation of its query #75, Answer a relaxation on the universe already filtered for the query #76 — diagnosis, and the filtering that makes it affordable. A universe filtered for a query answers every relaxation of it (Theorem C); the conservative filter is free (0.97–1.01× prepare); fix verification reuses the failed instance (3.0×).
• Index the package universe by interchangeability classes #71, Relaxation substrate: class activation as assumptions, and why a class is empty #72, MUS/MCS machinery: from exploratory to proper API #69 — class space and the relaxation substrate.
• Fix stale stdlib snapshot, and notice the next one (#103) #110, Make @alldeps mean both halves (#102) #111, Dedup identical ManifestEntry values across registries #101, Bound the scan for a package's chosen class #99, Document that interacts offset 0 is a real offset #94, Drop sat_disjoint_muses #93 — correctness and hygiene. Notably Fix stale stdlib snapshot, and notice the next one (#103) #110, which fixed a stale HistoricalStdlibVersions pin that had bin/resolve.jl resolving against a Julia 1.12 that never existed, and added the checks that catch the next one.

Next

The remaining feature work is one deliverable in three parts. pkg> why needs goals for presence answers and holdbacks for version answers, and the toolkit is how Pkg renders either in its own voice — so these are ordered by build cost, cheapest first, not by importance.

1. Diagnostics should explain steering surprises: why a resolve was held back to an older julia (or package) version #52 — holdbacks. Why a package resolved below its best, and what to relax to move it. The cheapest of the three: the machinery is exactly what a conflict already uses, the proof checker verifies a holdback's lines with no changes, and the archived prototype supplies a scenario list. Closes the last asymmetry — a failed resolve gets a verified proof, a surprising success gets one ⊼ character.
2. Goals: resolve(…; with, without) — ask whether some solution has a property #112 — goals. resolve(…; with = X, without = X). More expensive than holdbacks because it is not just a query: a goal asks whether some solution has a property rather than about optimal ones, so reachability and redundancy are unsound for it. Carries theory (Proposition G, plus a counterexample in each direction) that should survive the port intact.
3. Presentation toolkit: report() knobs, changes(), and --explain #113 — the presentation toolkit. report(io, d; knobs), changes(sol₁, sol₂), --explain, the guide section. Last because the structured surface is already public and documented, so Pkg can render its own reports today — and because every knob the prototype chose now aims at something that no longer exists. Best written against a real Pkg renderer.

Prior art for all three

archive/holdbacks-prototype is a pushed archive of a local branch that carried working prototypes of all three: holdbacks (c9e8b0c), goals (1539af3) and the toolkit plus --explain (3993297). Each is now captured as an issue with a build plan — #52, #112, #113 — and each issue names its own commit.

All three target src/Diagnose.jl and the Fact/UserCompat/Bound vocabulary that #105 replaced with clauses, and their tests assert wording that has since been retired: restricts for what is now leaves, and the symmetric "works with … only at" that directed verbs replaced. Read them for structure, theory and edge cases; re-derive every string.

They are not equally salvageable. Goals carries theory that should survive intact; holdbacks carries structure and a scenario list; the toolkit is mostly archaeology, since every knob it proposed aims at something main no longer has.

One thing found while capturing them: the prototype's upstream suggestions were never merged — but #114 has since shipped a better-founded version of the same idea, verified and narrowly scoped. What the prototype had that main still lacks is the knobs, not the feature.

Items 2 and 3 are what pkg> why needs. Presence answers come from goals, version answers from holdbacks; until both exist, why cannot be built on this.

Evidence-gated, not scheduled

• Diagnostics output-quality follow-ups: multi-hop holdback stories #63 — multi-hop holdback stories. Unreachable until holdbacks exist (Diagnostics should explain steering surprises: why a resolve was held back to an older julia (or package) version #52).
• T1 persistence: save/load/invalidate the universal registry cache (implementation plan) #55 — persistence. Demoted from first on the list above, after measuring what a resolve pays. It is not a parity gap — Pkg does not cache parsed registry data either, and bin/ uses Pkg's own lazy per-package parse — and the plan's headline numbers are whole-registry figures the normal path never touches. The cacheable work is 105–520 ms per query warm; the eager ~4 s of process setup is julia_versions.json and the stdlib tables, which are registry-independent and which a registry cache would not touch. Gated on separating work from JIT in that 4 s, which would also say whether the thing worth caching is the registry data at all.

Settled by measurement

Both of the measurements this section used to list have been taken, and they went opposite ways — which is the point of taking them.

• Constrained resolves: teach the descent to skip user-excluded versions #60 — kept, then fixed. The penalty survived class space and everything after it: 9.9× on JuMP, 1.9× on Makie, with the worst cases exactly where the constrained universe keeps the same class structure and the emptied classes stay in the ranking. Implemented in Start the descent from the best class the query admits #115.
• Redundancy is conservative for relaxations' sake; shadows might let it be aggressive #91 — closed. The aggressive i < j rule strikes zero extra classes over Rule A, across fifteen configurations including every package of a closure bounded below its unconstrained pick. Both rules were already in mark_necessary!, selected by one argument, so this cost a script rather than an implementation. A negative control confirms the harness detects a difference where one exists. The conservatism buys relaxation-stability for free.

Release

Worth stating plainly, because the mechanics have never been exercised: there are no tags, no GitHub releases, and Resolver is not registered in General. Project.toml says 0.2.0 and TagBot.yml is configured, but the path from here to an installable package has not been walked once.

Nothing in the code argues against releasing. CI is green across 1.9–1.13 plus nightly on four platforms, the suite includes registry-scale differential tests, and bin/resolve.jl has a production consumer in julia-downgrade-compat. The README's "experimental and research-stage" framing predates the diagnosis work and undersells what is here.

The one substantive question a release should settle is what is public. docs/src/api.md currently documents the diagnosis surface, the clause algebra and a block frankly labelled "Internals" (PkgInfo, prepare_pkg_info, exclusion_masks, find_reachable, …). Anything documented is something a user may reasonably pin to. Deciding which of those are 0.x-stable, and which should be marked as internal in a way that permits change, is cheaper before a release than after.

The Pkg test drive

Still not scheduled against a PR — but the calculus has changed. The unsatisfiable path is ready to review now: the API is stable, the reports are verified, the modelling conventions on #62 are settled.

JuliaLang/Pkg.jl#4738 targets the #30 API, three generations stale, and should be rewritten rather than rebased. KristofferC's feature-flag rollout — new resolver as default, old one retained — is unchanged and still right.

Principle behind the order

Structure before what is built on it; representation before persistence; performance and polish only where evidence points.

One addition, earned rather than assumed: where an issue's own text says "measure first", the measurement is the work item, and no successor is scheduled until the number exists. #60 and #91 were the test of it, and they went opposite ways — #60's penalty was real and got implemented, #91's payoff was exactly zero and got closed. Neither outcome was predictable from reading the issue, and #91's measurement in particular cost a script, because both rules turned out to be in the tree already.

#118 added a second lesson, cheaper than a measurement: check the premise before scheduling the gate. It was closed on 2026-09-15 without its measurement ever being run, because the mechanism it named was not the one at work — upstream fixes read PkgData.compat directly, so direction was never missing; what declines the registry-versus-registry case is a deliberate refusal to judge between two maintainers, which a direction bit does not resolve. The measurement would have counted the right rejections for the wrong reason.

---

🤖 Maintained with Claude Code.

[StefanKarpinski]

Update against main at 2480f3f.

Moved to done since this was written

• Diagnose an unsatisfiable resolve #73 — diagnose an unsatisfiable resolve. Merged. resolve returns a Diagnosis: independent conflicts, minimal fact chains, and a menu of fixes each verified by re-resolving.
• Relaxation-stable filtering: a filtered universe serves every relaxation of its query #75 — relaxation-stable filtering. This was the evidence-gated item below, and the evidence came in better than the question asked. The open number was whether a merged single-walk implementation lands near 1.0× prepare, against a prototype paying 2.3–3.6×. It lands at 0.97–1.01×, because the union with the prefix walk turned out to be unnecessary: the possibly-best walk provably contains the query's own prefix (Theorem D), so find_reachable was deleted rather than merged with anything. The conservative filter is free.
• Answer a relaxation on the universe already filtered for the query #76 — answer a relaxation on the universe already filtered for the query. Merged. Fix verification reuses the failed instance: 3.0× on the diagnosis path (0.377s vs 1.143s over 18 fixes, 7 queries).
• One map, one constraint type #79 — one map, one constraint type. Merged. A problem's constraints are a single Dict{Symbol,Constraint}; :compat and :pin are well-known kinds, anything else is custom. This removed the parallel labels mechanism, which changes the :requested convention in Pkg integration checklist: conventions, API mapping, rollout #62.
• resolve.jl: pass the target Julia version to the Pkg Context #80 — pass the target Julia version to the Pkg Context. Merged, with a regression test; manifest generation for a non-host Julia was broken and untested.

In flight: #81, renaming the one-argument is_satisfiable to sat_solve so no arity of that name can answer a staged question while looking like a total one.

Corrections to the lists below

• Constrained resolves: teach the descent to skip user-excluded versions #60 is not mooted. This roadmap says "likely mooted by class space … re-measure, then close". I re-measured: the penalty survives, 2.7× on Makie and 8.4× on DifferentialEquations, when the bounds actually exclude better versions. Numbers on Constrained resolves: teach the descent to skip user-excluded versions #60. It stays open.
• Diagnostics output-quality follow-ups: multi-hop holdback stories #63's item 3 (per-source fix granularity) is done, delivered by One map, one constraint type #79 + Diagnose an unsatisfiable resolve #73 rather than by the mark_necessary! column split it proposed. Items 1 and 2 stand.
• Diagnostic performance: directions beyond #57 #59 is closed as superseded — its whole frame was Diagnostics: goal-query resolve, verified fixes, and holdback analysis on the production SAT instance #57's per-probe closure sub-instances, which no longer exist. Its one surviving idea (goal-safe redundancy filtering) is preserved in the closing comment and belongs with item 2, goals.
• T1 persistence: save/load/invalidate the universal registry cache (implementation plan) #55's blocker is cleared (Provider crashes on compat entries naming non-dependencies (Python_jll 3.8.x → LibMPDec_jll) #54 closed and regression-tested), but its format question changed shape: Index the package universe by interchangeability classes #71 made class space the representation, so the open question is the on-disk form of a class-space artifact, not whether to store a derived classes field.
• Pkg integration checklist: conventions, API mapping, rollout #62's API mapping needs rewriting, as this roadmap already anticipated — details posted there.

Unrelated but worth recording

The Julia nightly - windows-latest - x64 CI job had been failing intermittently (~40% of runs) since #71 made it reachable. Root cause was upstream: picosat's enlarge() rebases pointers through a long, which is 32 bits on Windows x64, so a >2GB realloc move truncated the delta and corrupted every rebased pointer. Fixed in Yggdrasil (libpicosat 965.0.2); verified 6/15 crashes on the old build vs 0/15 on the new, interleaved on one runner. Nothing in this repo needed to change.

Order unchanged

The sequencing in the body still holds: conflict-level stories, then goals, then holdbacks (#52), then the presentation toolkit, then #61, then #55.

[StefanKarpinski]

Filed #83 for the diagnosis fix-menu restructure — per-conflict menus instead of the current product-of-all-conflicts menu, and a "may reveal more conflicts" sentence that is suppressed when we have actually ruled it out.

It belongs on the "Next" list. It is not the conflict-level stories item (#1 there, which is about why a conflict happened); it is about what the fix menu looks like once there is more than one conflict, which the measurements say is the normal case at realistic requirement counts — k > 1 in 85% of failing queries at ≤20 requirements, and the current menu hits its MAX_FIXES = 32 cap in a quarter of those.

Written as a handoff, including the two approaches that were tried and measured unsound or useless, so they are not re-proposed.

[StefanKarpinski]

Rewritten against main at d59bcd2. The previous revision was from 2026-08-18, before #84, #86, #90, #93, #94, #96, #98, #99, #101, #104, #105, #106, #107, #110 and #111.

What moved to done: the entire "conflict-level stories" item (#86 and the #104/#105 rebuild), and #61/weak deps via #82 — which was the last parity gap with Pkg's closure other than persistence.

What I reordered, and why. The old "Next" list ran conflict stories → goals → holdbacks → presentation toolkit → #61 → #55, with persistence last because the representation had to settle first. The representation has settled, so I promoted #55 to first: it is now the only parity gap left, and it is the one thing on the list that changes how the resolver feels — every resolve currently re-parses the registry, and julia-downgrade-compat pays that on every CI run.

I also downgraded the presentation toolkit from "largest remaining gap" to a convenience, and moved it last. The whole structured surface is public and documented now, so Pkg can render its own reports today; the report(io, d; knobs) layer would be better written against a real Pkg renderer than guessed at in advance.

Two things I added that were not tracked anywhere.

First, a release section, because the mechanics have never been exercised: no tags, no GitHub releases, and Resolver is not registered in General. Nothing in the code argues against releasing — but the path from here to an installable package has not been walked once, and that is worth knowing before it is on the critical path.

Second, the question a release ought to settle: docs/src/api.md documents the diagnosis surface, the clause algebra, and a block labelled "Internals" (PkgInfo, prepare_pkg_info, exclusion_masks, find_reachable). Anything documented is something someone may pin to. Deciding what is 0.x-stable is much cheaper before a release than after.

Issues triaged in the same pass: #100 and #108 closed; #52, #55, #60, #62, #63 and #91 updated with their status against current main.

---

🤖 Triaged with Claude Code.