Your browser sucks, JavaScript disabled! Gunnar's console needs JavaScript and WebAssembly. Git over SSH on port 2222 does not.

nordisk/dwarves

dry-run.md

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:

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.

  1. Discover. Read the workspace descriptor: members, and any release = false held.

  2. 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-thing before dwarves' embed crates, before dwarves, before nornir.

  3. Gate A — static. Merge G_io (crates.io) with G_src (local source). Check: versions resolve (PubGrub; a conflict prints its derivation); every required feature Φ is exposed by the provider; no publish = false / unpublished normal|build dependency; no bare *; path-deps carry a version; acyclic after condensation. No compiler; milliseconds. A failure refuses here, before any build.

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

  5. 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 --execute to go further.

  6. Freeze + Verify (build last). On --rehearse/--execute the optional --ramp freeze 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-tests drops the test pass). It builds into the same target dir --execute reuses, warming the cache.

  7. Gate B — rehearsal (build last). On --rehearse/--execute, spin up a served Holger /sparring on 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:

    1. reconcile its Cargo.lock to the versions /sparring serves,
    2. cargo publish -p <crate> --registry sparring — a real build into the shared target,
    3. wait until /sparring serves it,
    4. record the shipped version for the next consumer.

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.

  1. Decision. Both gates green: a --verify/--rehearse dry-run stops here with a warm cache; --execute runs 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:

  1. Root Inclusion — every target crate is in R.
  2. Dependency Closure — for every active edge, the chosen provider version satisfies req.
  3. Version Uniqueness — one version per crate name.
  4. 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 errors that forged these: the Book of Errors.


← back to the Dwarves README