# ADR-045: Persistent Library Build Cache for Gate A

| Field | Value |
|-------|-------|
| **Decision ID** | ADR-045 |
| **Initiative** | unsorry — Gate A performance |
| **Proposed By** | unsorry maintainers |
| **Date** | 2026-06-15 |
| **Status** | Accepted |

## Context

Gate A's three Lean jobs — `gate-a-prepare`, `gate-a-audit`, `gate-a-replay` — each check out a
fresh tree and each run `lake build UnsorryLibrary --wfail` before their own step (cheap
checks, axiom audit, kernel replay). mathlib arrives fast as a binary olean cache
(`lean-action`'s `use-github-cache`, ~1 min), but the **local `UnsorryLibrary` oleans are not
persisted across runs**, so the library is recompiled from scratch every job.

Measured on a representative prove PR (run 27512269673):

- `gate-a-prepare` library build: **~21 min** (`21:16:37 → 21:37:36`).
- `gate-a-replay` library build: **~16 min** (`22:04:39 → 22:21:08`).
- `gate-a-audit` does the identical build before its (already-incremental, ADR-033) audit.

So a one-proof change pays a full cold library compile **three times** per gate-a run, while the
axiom audit and kernel replay — the actually-authoritative steps — are already incremental and
fast. The build is the long pole and it is pure waste: the unchanged modules are byte-identical
to `main`.

## WH(Y) Decision Statement

**In the context of** a Gate A whose three jobs each cold-build the whole `UnsorryLibrary`
(~16-21 min apiece) on every run because only mathlib — not the local oleans — is cached, while
the audit and replay are already incremental,
**facing** the fact that this triples the dominant cost of every prove PR for no soundness
benefit (the unchanged modules are identical to main and were already verified there),
**we decided for** caching the repository-local Lake build directory **`.lake/build`** with
`actions/cache` (the GitHub Actions cache protocol, which the Namespace runners already back
with high-performance storage — proven by `lean-action`'s working mathlib cache): a key of
`lake-build-<os>-hashFiles(lean-toolchain, lake-manifest.json, lakefile.toml)-<sha>` with a
`restore-keys` prefix dropping the sha, added to all three jobs — so a new commit restores the
most recent oleans and `lake build` recompiles only the changed modules, and within one run
`gate-a-prepare` saves under the commit sha while `gate-a-audit`/`gate-a-replay` (which `need`
prepare) restore that exact key, building the library **once per run instead of three times**,
**and neglected** Namespace-native caching (`nsc artifact`, cache volumes) — rejected for this
PR: `actions/cache` is portable, is the same mechanism already in use, and what we cache
(`.lake/build`, the local oleans — not mathlib) is small enough that raw cache throughput is not
the bottleneck; a Namespace cache volume in the runner profile is a cleaner *follow-up* the
maintainer can layer on outside the repo — and caching mathlib here (already handled by
`lean-action`) or restructuring the three jobs into one build + two artifact-consumers (larger
change; the cache already gives the build-once benefit),
**to achieve** Gate A library builds dropping from ~16-21 min × 3 to one incremental build of
the changed module(s) — minutes, not the better part of an hour — on every prove PR and on
re-runs of a cancelled run,
**accepting that** the cache is keyed advisory state, not trust-bearing: it is invalidated by
any toolchain / mathlib / lakefile change (forcing a full cold rebuild), and the soundness
guarantees are unchanged — Lake's content-hash traces recompile any module whose source
changed (the same incrementality the project already trusts for local `lake build`), the
authoritative axiom audit and `leanchecker` kernel replay still run, and the kernel replay
validates an olean's proof term against the kernel whether the olean was just built or restored;
every olean that reaches `main` is kernel-replayed by the **full** post-merge replay (push to
`main` runs with no BASE_SHA), so a stale or poisoned cache can never produce a false PASS.

## Soundness argument (explicit)

1. **Incrementality is Lake's, not ours.** Restoring `.lake/build` and running `lake build`
   triggers Lake's standard trace check: any source file whose content hash differs from the
   cached trace is recompiled. This is identical to a local incremental build across a `git
   checkout` — already trusted throughout the project.
2. **The authoritative checks are untouched.** `--wfail` build, axiom audit (ADR-006/011), and
   `leanchecker` kernel replay (ADR-033) all still run. Replay kernel-checks olean proof terms
   regardless of their provenance (built vs restored).
3. **Every merged olean is fully kernel-replayed.** A push to `main` runs audit + replay with
   no BASE_SHA → the full library is re-audited and re-replayed. A cache that ever drifted from
   source would surface there (or fail to load), so it cannot silently admit an unsound proof.
4. **Key invalidation.** Toolchain / mathlib / lakefile changes change the key prefix → cold
   rebuild, so oleans are never reused across an incompatible compiler or dependency set.

## Consequences

- **Positive.** Gate A's long pole (the library build) goes from ~16-21 min × 3 to one
  incremental build; re-runs of a cancelled run are near-instant (exact-key hit on the sha).
- **Positive.** Lower runner-minute spend; faster autonomous merge loop (ADR-005).
- **Negative.** First run after a toolchain/mathlib bump (or the very first run introducing the
  cache) pays one cold build. A cache miss degrades gracefully to today's behaviour.
- **Follow-up.** A Namespace cache volume mounted at `.lake` in the runner profile would remove
  even the restore/save step; this PR's cache step becomes redundant and removable if adopted.

## Amendment (2026-06-15): the restored cache did not make `lake build` a no-op — skip it instead

The decision above assumed that restoring `.lake/build` would let `lake build UnsorryLibrary`
recompile *only* changed modules, so the library would build once per run. **Run logs show it did
not.** Even on an **exact-key cache hit** (e.g. run 27536559685: `gate-a-audit` restored
gate-a-prepare's 160 MB `.lake/build` in 8 s), `lake build UnsorryLibrary --wfail` still
**recompiled the heavy library modules from scratch — ~213 s** — in the audit job, and again in
replay. The cache restores fine; Lake just does not trust the restored oleans, because
`lean-action` re-provisions mathlib **after** the cache restore, so the library oleans look stale
relative to their freshly-laid mathlib dependencies and Lake re-elaborates them. Net: the
intended "build once" never happened — the full library build ran in all three jobs (~3.5 min ×
3), the single biggest constant cost of every active-PR gate run.

Forcing Lake to trust the restored oleans (e.g. mtime manipulation) would be **unsound** — a
genuinely-changed module could be skipped. So instead we **stop audit and replay from building at
all on an exact-key hit**: `gate-a-prepare` remains the authoritative builder (`lake build
UnsorryLibrary --wfail`, always), and `gate-a-audit` / `gate-a-replay` guard their library-build
step with `if: steps.lake_build_cache.outputs.cache-hit != 'true'`. On the exact-commit-sha key
those jobs restore prepare's exact oleans and **load** them — `axiom_audit` is a standalone
`lean_exe` (root `AxiomAudit.Main`, imports only `Lean`) run via `lake exe`, and `leanchecker`
runs via `lake env`; neither triggers a library `lake build` — so the ~213 s rebuild is pure
waste and is dropped. On a cache miss the build runs as before (self-healing).

Soundness is unchanged and arguably clearer: the kernel replay still kernel-checks every olean it
loads, the oleans are prepare's build of the *same commit* (exact-sha key), the `--wfail` bar is
enforced once in prepare, and the push-to-`main` full audit + replay remain the post-merge
backstop. Prepare's own build is still a full (non-incremental) compile — fixing *that* would
require resolving the Lake-trust-after-restore issue and is left as a follow-up; this amendment
removes two of the three redundant builds, which is the bulk of the waste.

## References

| Reference ID | Title | Type | Location |
|--------------|-------|------|----------|
| REF-1 | Build-cache spec | Specification | specs/SPEC-045-A-Gate-A-Library-Build-Cache.md |
| REF-2 | Gate A workflow | Specification | specs/SPEC-006-B-Gate-A-Workflow.md |
| REF-3 | Incremental kernel replay | Decision | ADR-033-Incremental-Kernel-Replay.md |
| REF-4 | Gate A soundness enforcement | Decision | ADR-006-Gate-A-Soundness-Enforcement.md |

## Status History

| Status | Approver | Date |
|--------|----------|------|
| Proposed | unsorry maintainers | 2026-06-15 |
| Accepted | unsorry maintainers | 2026-06-15 |
| Amended (skip redundant build in audit/replay on cache hit) | unsorry maintainers | 2026-06-15 |