Goals: resolve(…; with, without) — ask whether some solution has a property

[StefanKarpinski]

Build plan, written as a handoff against main at d59bcd2. Roadmap item 2 (#64). Prior art exists and is a spec, not a patch — see below.

What a goal is

resolve(info, prob; with = "CUDA") and resolve(info, prob; without = "FillArrays"): ask whether some solution has a property, and what it costs.

The whole semantic difference between a goal and adding the package to prob.reqs is one sentence, from the prototype's own header:

prob's constraints are negotiable — a diagnosis may propose relaxing any of them — and the goal is the fixed ask.

So "drop requirement CUDA" can never appear as a fix. That is the point, and it is why a goal is not sugar for a requirement.

Why this needs care: goals are not preparation-safe

This is the part that makes goals more than plumbing, and the prototype got it right with a proof. Every relaxation query the resolver answers today runs on the prepared universe, and every one of them asks about optimal solutions — which is exactly what preparation preserves. A goal does not ask about optimal solutions. It asks whether the solution set contains one with a property.

Two of the preparation passes are therefore unsound for goals, and the prototype's theory page gives a counterexample for each:

Take A → B, B@3.1 → X, B@2.3 → ∅, no conflicts, R₀ = {A}. Reach seeds B@3.1 and nothing degrades it, so the filtered universe has only B@3.1 and every solution of it contains X. In D the solution {A@1, B@2.3} avoids it. So on the filtered universe the goal ¬X is unsatisfiable and on D it is satisfiable: not a worse answer, a wrong one.

Redundancy fails the same way in the other direction. If A@2 (better) depends on nothing and A@1 depends on X, then A@2 dominates A@1 and elimination deletes it — after which the goal "X present" is unsatisfiable, though {A@1, X} witnesses it in D.

Neither pass ever claimed to preserve non-optimal solutions. Both are behaving as proved.

What is goal-safe is the T1 half, and for a reason rather than by luck — the prototype states and proves it as Proposition G: arc consistency deletes only versions that occur in no solution at all (so they witness no goal), and interchangeability classes never merge across different dependency sets (so a package that avoids X can never hide inside a class whose representative needs it — that would be two rows differing in a dependency column).

Carry Proposition G and both counterexamples forward. They are the load-bearing content of this issue, and they were written against class space, so they should survive the port intact.

The prototype

archive/holdbacks-prototype, commit 1539af3 ("goals — one verb, and it answers the question you asked"): src/Goal.jl (139 lines), test/goals.jl (304 lines), theory in docs/src/theory/diagnostics.md, plus wiring in Resolve.jl, SAT.jl, FilterPkgs.jl and Closure.jl. ~1,067 lines.

Design worth keeping:

• Goal{P} — with :: Vector{Pair{P,Any}} (versions nothing for "any", else anything in answers for) and without :: Vector{P}. A bare version reads as the singleton set, so with = "DataFrames" => v"1.8.2" means what it looks like.
• prepare_goal_info — the goal sub-instance: collapsed and arc-consistent, but not reach- or redundancy-filtered.
• goal_reach_safe — a pure presence ask is safe to filter normally, because the caller has already made those packages requirements of the sub-instance and reachability keeps their prefix. Only version-naming and absence asks pay. Worth keeping: it means the common case does not lose the filter.
• goal_masks — versions a goal names by value must be kept out of the class collapse, since a class sibling is not the version that was asked for.
• In the instance a goal is a hard assumption, one selector-guarded clause per term, held on by every probe and absent from the fix enumeration — held on rather than asserted at level 0 so a conflict can be asked whether it needed the goal.

It cannot be ported. It targets src/Diagnose.jl, which #105 replaced with src/Diagnostics.jl and a clause vocabulary; Problem's labels mechanism it references was removed by #79; and its report wording predates the #105 verb table. Read it for structure, theory and edge cases; re-derive the strings. The same caveat that #52 spells out applies here.

Decisions to make

1. Where the goal enters. The prototype threads it through SAT(info, prob, goal) and a parallel goal_universe. Whether that shape survives class space and the current prepare_pkg_info is the first thing to work out.
2. What a failed goal returns. A Diagnosis shaped like an unsatisfiable resolve, with the goal in the heading and "drop the goal" absent from every menu? That is the natural reading of "the fixed ask", and it would inherit the proof checker.
3. Cost of the unfiltered sub-instance. Skipping reach and redundancy means a bigger instance for exactly the queries that need it. Measure it; if absence goals are expensive, that is worth knowing before Pkg leans on them.
4. issatisfiable parity. The prototype put with/without on both. Keep that.

Why it matters

#62 names goals as the mechanism for the presence half of pkg> why — "why is X here", "what would avoiding X cost". With #52 (holdbacks) covering the version half, these two are what pkg> why needs; neither exists today.

The pricing half is already portable: changes(sol₁, sol₂) from the toolkit prototype turns a feasible goal into "avoidable, but it costs you CSV 0.10.15 → 0.5.26". See the toolkit issue.

Verification

test/goals.jl (304 lines) is the scenario list to port. If decision (2) lands on "a Diagnosis", then test/proof_check.jl's lines_are_true verifies a failed goal's lines with no new checker, exactly as for holdbacks.

The oracle for the unfiltered sub-instance is the counterexample pair above: both must give the same answer on the sub-instance as on the unprepared universe.

---

🤖 Captured with Claude Code.