Release pseudocode (Rust)
Dwarves' release is an industrialisation of empirical programming knowledge and academia. The graph algorithms and version-solving are borrowed from the literature; the feature model and the rehearsal are forged here.
dwarves workspace-release is tiered, and it runs cheap-first, build-last. The DEFAULT dry-run plans only — it discovers the constellation, computes the deps-first order and ship-versions, runs the static Gate-A precheck, and emits the advisory graph analysis, then STOPS: no build, no cargo test, no branch, no mutation — sub-second. The two heavy build steps are opt-in and run last, only once every cheap gate is green:
--verifyadds the pre-publishcargo testsuite.--rehearseadds the Gate-B/sparringrehearsal (and, with--ramp, the branch freeze).--executeimplies both (a real publish always verifies + rehearses — safety is never weakened), then uploads.
Because the build is last, a plan or gate error never costs a wasted build — the cheap checks fail-fast first. And because a --verify/--rehearse dry-run builds into the same CARGO_TARGET_DIR (or repo target/) the real --execute reuses — never a throwaway temp — the dry-run warms the cache the subsequent --execute reuses. Gate A is static — milliseconds, no build. Gate B builds the whole cascade into a staged, local Holger. Nothing reaches crates.io until both gates are green.
fn workspace_release(path, execute, bump, verify, rehearse, members, include_held) {
// ── CHEAP: plan + static validation, no build (fail-fast) ──
let cst = discover(path); // members + held
let (active, held) = resolve_active_set(cst, members, include_held);
let graph = build_feature_graph(active); // G_src: nodes + version & feature edges
let order = kahn(condense(tarjan_scc(graph))); // deps-first, crate-level inside a cycle
gate_a(merge(probe_cratesio(graph), graph)); // static: versions + features resolve
let ship = ship_versions(active); // the bump-hoist
graph_analysis(order, ship); // advisory: diff + datalog + verification theorem
// ── PLAN-ONLY DEFAULT: no build flag ⇒ print the plan and STOP (no build, no branch) ──
if !execute && !verify && !rehearse { print_plan(order, ship); return }
// ── BUILD LAST — on a frozen snapshot, into the SHARED target (warms --execute's cache) ──
if rehearse || execute { freeze_ramp(active, ship); } // git branch + commit only — NOT a build
if verify || execute { verify_suite(active); } // cargo test — into the shared target
if rehearse || execute { gate_b(order, ship); } // rehearse into a served /sparring
if !execute { return } // dry-run: the cache is now warm for --execute
for crate in order { // deps-first
publish(crate);
wait_for_index(crate); // consumer waits for its dep
}
}
The tiered run, step by step
The cheap steps (1–5) run on every invocation and fail-fast. The heavy build steps (6–7) run last, and only when a build was requested (--verify / --rehearse / --execute) and every cheap gate is green.
-
Discover. Read the workspace descriptor: members, and any
release = falseheld. -
Order. Build the cross-repo dependency graph. Condense repo-level cycles with Tarjan's SCC into a DAG; sort it deps-first with Kahn, interleaved at crate granularity inside a cycle —
nornir-build-thingbefore dwarves' embed crates, beforedwarves, beforenornir. -
Gate A — static. Merge
G_io(crates.io) withG_src(local source). Check: versions resolve (PubGrub; a conflict prints its derivation); every required feature Φ is exposed by the provider; nopublish = false/ unpublishednormal|builddependency; no bare*; path-deps carry a version; acyclic after condensation. No compiler; milliseconds. A failure refuses here, before any build. -
Ship-versions + advisory analysis. Compute the bump-hoist (
ship_versions) and emit the advisory graph diff, the Datalog why-order / why-held inference, and the Verification-Theorem soundness verdict — all read-only, no build. -
Plan-only stop (the default). With no build flag, the deps-first plan + ship-version graph are printed and the run returns — no build, no
cargo test, no branch, no mutation. Add--verify,--rehearse, or--executeto go further. -
Freeze + Verify (build last). On
--rehearse/--executethe optional--rampfreeze cuts one release branch per member (git branch + commit + lock reconcile — not a build), so the build and publish run on an immutable snapshot a concurrent push to main can't disturb. Then, on--verify/--execute, the pre-publish verify suite runs per member:cargo test --release, the offline gates, preflight (--skip-testsdrops the test pass). It builds into the same target dir--executereuses, warming the cache. -
Gate B — rehearsal (build last). On
--rehearse/--execute, spin up a served Holger/sparringon loopback:/cache, a crates.io pull-through mirror for third-party deps, and/sparring, a writable registry where the cascade lands. crates.io is source-replaced onto the mirror, so the 17 repos resolve each other as if already published. For every crate, deps-first, in the real publish order:- reconcile its
Cargo.lockto the versions/sparringserves, cargo publish -p <crate> --registry sparring— a real build into the shared target,- wait until
/sparringserves it, - record the shipped version for the next consumer.
- reconcile its
Consumer lockfiles are snapshotted and restored; the rehearsal leaves no trace. One crate fails, the release refuses — the cargo error is printed, nothing is uploaded.
- Decision. Both gates green: a
--verify/--rehearsedry-run stops here with a warm cache;--executeruns the same cascade against crates.io, reusing the artifacts the dry-run built.
AI-free — 100% dwarven-forged
No model in the loop. Every decision is a deterministic Rust algorithm. crates.io is append-only, so nothing reaches it until both gates are green.
The formal model
Dwarves models the release as a feature-conditional dependency multi-graph, proven by two gates.
§1 The graph. G = (V, E), directed, multi-edge. A node is a crate v = (name, version, F(v), publishable): F(v) the features it declares, A(v) ⊆ F(v) the features active in a build. An edge is a dependency e = (u, v, req, Φ, kind, cond): req a semver interval, Φ ⊆ F(v) the features required on the provider, kind ∈ {normal, build, dev}, cond ⊆ F(u) the consumer features that activate an optional edge (∅ if unconditional).
§2 Feature activation — a least fixed-point. An edge is live when Active(e) ⟺ cond = ∅ ∨ cond ⊆ A(u). A feature activates an optional edge, which requires more features, which activate more edges — so the active set is solved globally. Iterate the monotone step T (each active edge adds its Φ and the provider's default features) to a fixed point. T is monotone on the powerset lattice; by Knaster–Tarski the least fixed point A* = lfp(T) is unique — the feature set cargo's resolver v2 builds with.
§3 A resolution R is valid iff four conditions hold. Three from the Package Calculus, the fourth from here:
- Root Inclusion — every target crate is in
R. - Dependency Closure — for every active edge, the chosen provider version satisfies
req. - Version Uniqueness — one version per crate name.
- Feature Availability —
Active(e) ⟹ Φ ⊆ F(v): the provider exposes every feature the edge requires.
§4 The Verification Theorem (Gate A). valid(R) ⟺ ∀ active e = (u, v, req, Φ, kind ∈ {normal, build}) : Vplan(v) ∈ req ∧ Φ ⊆ F(v @ Vplan(v)). Checked over the merged graph in memory, no compiler. dev edges are stripped on publish; they never constrain the order. A failed clause prints its PubGrub derivation: which requirement, which feature, which consumer.
§5 The two-graph merge — three proofs. G = G_io ⊕ G_src. Valid iff (a) resolvable — §4 holds over G (Gate A); (b) acyclic after Tarjan condensation — a Kahn order exists; (c) constructively valid — it builds and publishes the whole cascade into a throwaway registry (Gate B).
§6 The algorithm stack. Tarjan SCC O(V+E); condensation → DAG; Kahn topo O(V+E); MFAS (Eades greedy, advisory); PubGrub/CDCL for version SAT + explanations; Sugiyama for the diagrams.
Borrowed and forged
Borrowed from the literature: the graph algorithms — Tarjan, Kahn, condensation — and version-solving as SAT (EDOS→Mancoosi, PubGrub).
Forged here, where the literature stops:
- The Package Calculus is version-only: Root Inclusion, Dependency Closure, Version Uniqueness. It does not model features. The feature-conditional edge, the least-fixed-point activation, and the Feature-Availability condition are ours. The
holger-server-lib/onlinefailure needed them. - PubGrub solves versions, not features. It explains version conflicts; it cannot see a missing feature. Gate A checks features; Gate B builds.
- The lockfile literature (Gamage et al.) classifies lockfiles; it prescribes no rehearsal. Gate B is ours.
- MFAS is NP-hard — no exact polynomial form. The Eades greedy heuristic is advisory: which edge to break, never an automatic fix.
- Cross-language API/ABI compatibility has no unified theory. Per language:
cargo-semver-checks,revapi,libabigail. That edge is engineering.
The errors that forged these: the Book of Errors.
← back to the Dwarves README