Skip to content

v1.15.0 — a leaner, cheaper Gate A at scale + decentralised-runner groundwork

Choose a tag to compare

View all tags
@cgbarlow cgbarlow released this 15 Jun 22:28
· 1119 commits to main since this release
v1.15.0
83d0381
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Headline: a leaner, cheaper Gate A at scale — plus groundwork for a decentralised runner — as proofs compound, Gate A is kept fast and memory-bounded instead of slowly OOM-ing: two more archive blocks (0003 and 0004, ADR-041) retire 58 proved goals and shrink the active library from 108 → 50 modules; archive validation switches to verify-on-ingest (git-blob provenance instead of a kernel re-replay, ADR-048) so archive PRs fit an 8 GB runner; push-to-main now kernel-replays incrementally with a daily full-replay backstop (ADR-048 Phase 2); the full-replay trigger narrows to olean-invalidating changes only; and a persistent Namespace .lake cache volume (ADR-046) removes the last constant per-job mathlib-restore cost. Soundness is unchanged throughout — every proof is still kernel-replayed once under its pinned toolchain. Alongside, ADR-049 lands the research + a Phase-0 conformance suite for a future decentralised CI runner, and the browser surfaces grow a proofs-over-time graph, a Top 5 view, and a shared home page.

Added

  • ADR-049 Phase-0 conformance suite (tools/gate_a/tests/test_decentralised_runner_conformance.py, #635) — locks the decentralised-runner soundness invariant: the central re-check feeds leanchecker only locally-derived modules (never a contributor artifact), an untrusted diff fails closed to a full re-check, and a changed module always drags its *Binding + reverse-import closure into scope.
  • ADR-049 research (#635) — a ranked options analysis (docs/proposals/decentralised-ci-runner-architecture.md) and ADR-049 (Proposed) recommending a tiered split: push the expensive lake build elaboration onto the contributor, keep a mandatory cheap central kernel re-check from canonical source as the sole load-bearing gate.
  • Leaderboard proofs-over-time view (#738) — a cumulative line graph of kernel-verified proofs by date, plus a shared Home · Leaderboard · Proof graph top nav and a new docs/index.html landing page.
  • Leaderboard Top 5 view — a three-tab switcher (Leaderboard · Top 5 · Proofs over time), README links from the home page, and small-screen tuning.
  • Persistent Namespace .lake cache volume (nscloud-cache-action, ADR-046) — mathlib oleans + the local build survive across jobs/runs, eliminating the ~2–3.5-min GitHub-cache mathlib restore paid on every job. Advisory: leanchecker still re-checks every olean.

Changed

  • Amended ADR-041: archive closed proof families only — a decomposition family (parent + subs + proofs + metadata) is archived as one atomic unit, and only when every member is proved.
  • Cut archive block 0003 (ADR-041) — retired 30 proved goals (whole trees + standalone) into packages/unsorry-archive-0003/; active library 108 → 78 modules.
  • Cut archive block 0004 (ADR-041) — retired 28 proved goals into packages/unsorry-archive-0004/; active library 78 → 50 modules.
  • Documented the archive-block cut as a repeatable runbook (SPEC-041-A §8/§9), including the "cut early and often, 40 is a ceiling not a goal" at-scale guidance.
  • Corrected the archive-cut runbook after 0003/0004: archive whole decomposition trees only (Gate B GB008/GB016 atomicity) and never regenerate generated docs in the cut (they race main's refresh bot).
  • Gate A push-to-main now replays incrementally (ADR-048 Phase 2) with a daily gate-a-full-replay.yml backstop; routine Gate A (proof PRs and push to main) routes to the 8 GB unsorry-1 runner. Soundness unchanged — every proof still kernel-replayed once.
  • Narrowed the Gate A full-replay trigger to olean-invalidating changes only (lean-toolchain, lakefile.*, lake-manifest.json), so gate/CI PRs no longer ride the memory-bound serial full replay that OOM-killed the 16 GB runner.
  • Gate A no longer rebuilds UnsorryLibrary in the audit/replay jobs on an exact-sha cache hit (ADR-045 amendment) — the audit job drops from ~535 s to ~320 s.
  • Adopted verify-on-ingest for archive validation (ADR-048) — archived proofs are checked byte-identical to the already-verified version (git-blob provenance) instead of re-running leanchecker, removing the archive-OOM class.

Fixed

  • gate-a-archive now runs on the 16 GB unsorry-2 runner (was routed to the 8 GB pool and OOM-killed, #764).
  • Archive-package replay now chunks at REPLAY_CHUNK_SIZE, bounding peak memory — fixes the exit-137 OOM on memory-bound runners (#764).
  • Archive-package validation runs in its own parallel gate-a-archive job (own headroom + swap + 120-min budget) instead of inside gate-a-prepare (#764).
  • Gate B's advisory AISP validator now runs on Node.js 24.

Full changelog: https://github.com/agenticsnz/unsorry/blob/main/CHANGELOG.md
Compare: v1.14.0...v1.15.0

Assets 2
Loading