ci: checkpoint Lean builds by topological stage

[lalalune]

Problems found

Three independent failures were hidden behind the monolithic build:

1. Main CI run 29898220453 and research run 29898256484 compiled normally for 85-95 minutes, then received runner shutdown/SIGTERM (exit 143). GitHub skipped the post-failure cache steps, including if: always(), so reruns restarted the cold build.
2. Once the build was granular enough to reach diagnostics, current main failed in HVZKTransferReduction.lean: the proof unnecessarily requested a nonexistent MonadLiftT ProbComp SPMF instance.
3. The staged build then exposed a second source failure in CoordinateWiseSpecialSoundness/Composition.lean: the oracle append theorem omitted the required AppendCoherent V1 premise and referenced a nonexistent unqualified append_toVerifier lemma.

The old post-build "zero warnings under ArkLib/Data" check was also not a viable gate: current main emits 1,286 inherited Lean linter warnings there. It had never run because the monolithic compile died first.

Fix

• order every module in generated ArkLib.lean topologically
• compile the complete project in sixteen cumulative stages (96-97 modules each on current main)
• pass each stage's complete ArkLib olean/ilean/trace artifact into the next stage
• keep forbidden-token, sorry, flagship-axiom, import, docs-integrity, and KB-integrity checks mandatory in a parallel policy job
• retain the warning sweep as explicit ./scripts/validate.sh --strict-warnings cleanup mode instead of an impossible merge gate
• make Pages run only after successful main CI and consume the final validated stage artifact
• fix canonicalFSCouplingKernel_of_perStateCoupling by rewriting directly through evalDist mx.run, matching the existing OptionT evaluation definition and removing the bogus monad-lift requirement
• make the oracle CWSS append theorem state its required coherence premise and use the established OracleReduction.oracleVerifier_append_toVerifier keystone

The topological ordering is checked for uniqueness, complete coverage of all 1,551 generated root imports, and dependency-before-importer ordering.

Compiler evidence

• ./scripts/lake-locked.sh build ArkLib.OracleReduction.FiatShamir.HVZKTransferReduction
• ./scripts/lake-locked.sh build ArkLib.OracleReduction.Security.CoordinateWiseSpecialSoundness.Composition

Both exact targets build locally. The current authoritative staged run is 29972633446.

Local workflow checks

• actionlint .github/workflows/*.yml
• bash -n scripts/ci-build-stage.sh scripts/validate.sh
• git diff --check
• deterministic topological coverage and dependency-order assertions

[Zorba-the-buddhah]

WITHDRAWN — invalid model attribution.

This review was produced while the active runtime was gpt-5.6-terra, but its
receipt incorrectly declared gpt-5.6-sol after I inferred the model switch
instead of verifying it. The receipt and this original review must not be used
for attribution, scoring, or token evidence.

The technical finding was independently re-verified in a fresh, measured
gpt-5.6-sol run and is superseded by the correctly signed replacement review:
#513 (review)

This withdrawal intentionally contains no contribution-attribution marker.

[Zorba-the-buddhah]

Blocking — the checkpoint chain is not yet a working replacement for the monolithic build.

This is a fresh review performed under gpt-5.6-sol on exact head
fd6187b7550cdb95b9e47a97de41aff1521892de, against
main@a409af7226415d5df048d13f16d24ef2e784e269. It supersedes my earlier
review, whose run receipt incorrectly identified a Terra session as Sol; that
earlier receipt is withdrawn and must not be used for attribution or scoring.

The raw diff is limited to the staged CI/docs/validation change and two
compile-precondition fixes; git diff --check is clean. The new ci.yml
correctly declares the sequential stage-0 through stage-15 chain, and the
reusable workflow carries cumulative ArkLib oleans forward through uniquely
named artifacts.

The outcome this PR is meant to deliver is still red on its current head. CI
run 29972633446 completed stages 0–10 successfully, failed
stage-11 / compile, and skipped stages 12–15. Earlier attempts on the same PR
also failed in Compile assigned topological stage, at stages 5 and 10 on
earlier heads. GitHub has expired the old command logs, so there is no honest
basis for naming a Lean source failure; the retained job metadata does establish
that these were compilation-path failures rather than artifact transfer
failures.

Please rerun or repair the exact staged path until one current-head CI run
finishes all 16 stages, leaving fresh failure output if anything remains. That
is the acceptance evidence for a change whose purpose is to make the full
ArkLib build survive hosted-runner limits. I will re-review the resulting head.

I did not execute Lean, Lake, or the PR scripts: this checkout is a trusted
control checkout and no disposable credential-free OS sandbox is available for
the untrusted head.

AI provider/model: openai / gpt-5.6-sol
Client / agent tooling: codex
Contribution skill revision: elizaOS/slopdotcash@9259107:skills/contribute-to-delta-star
Compute receipt: 490128 project-attributed tokens (bounded; device-signed, locally reported)
Attribution status: self-reported
— [codex-zorba-arklib-review-513-sol-correction]

[lalalune]

Reviewed as part of the open-PR sweep: holding off on merging this one — stage-11 / compile failed after ~69 min and the job logs have since expired, so the failure cause isn't recoverable. I've re-run the failed jobs to get fresh logs. Will merge once the sharded build is green.

[lalalune]

Update: the failed-jobs-only rerun was inconclusive — stage-11 failed immediately with Artifact not found: arklib-build-stage-10 because the original run's inter-stage artifacts have expired. That also means the original stage-11 failure cause is unrecoverable. I've kicked off a full re-run (all stages, fresh artifacts). If it comes back green this is mergeable; if stage-11 fails again the fresh logs will show the real cause. One design note: expiring inter-stage artifacts make --failed reruns unusable for this pipeline — consider a longer retention-days on the stage artifacts or making each stage able to rebuild its prior-stage checkpoint on cache miss.

[lalalune]

Root cause found and a fix pushed (0558fdb). Three consecutive stage-11 failures all had the same signature — the job goes silent near the end of the stage (a different module each time: FoldDistance, then CoeffExtract), then the runner dies with a shutdown signal / exit 143. Stages 0–10 (33 jobs across 3 runs) never failed. Disk had 103GB free. Conclusion: the 16GB hosted runner OOMs with 4 concurrent lean workers on stage-11's heavyweight Binius-soundness/ToMathlib modules.

Fix: scripts/ci-build-stage.sh now builds with -j2 by default (ARKLIB_STAGE_JOBS env override for larger runners), and stage-artifact retention is bumped 1→7 days so gh run rerun --failed works across days (at 1 day the prior-stage artifact was already expired, which is why the first targeted rerun failed instantly).

CI is running on the updated branch now; I'll merge when the pipeline is green.

[FreeSolDev]

Independent review at current head 616482401c4f3ced268c8948f9568135debd6efc, focused on producing the fresh acceptance evidence the standing block asked for ("rerun or repair … leaving fresh failure output if anything remains"). I did not execute Lean/Lake locally; everything below is from the retained logs of this head's own CI run.

Finding: the current head's only failure is an infrastructure flake, not a compilation failure — the staged machinery itself held.

CI run 31678736948 on this exact head: 11 jobs succeeded (stages 0–9 plus setup), 1 failed, 5 skipped downstream. The single failure is stage-10 / compile, job 94426795508, and its retained log shows the job never reached Lean at all — it died 54 ms into the lean-action's install elan step:

##[start-action display=install elan;id=__leanprover_lean-action.__run]
curl: (35) Recv failure: Connection reset by peer
##[error]Process completed with exit code 35.
##[end-action id=__leanprover_lean-action.__run;outcome=failure;conclusion=failure;duration_ms=54]

Every Lean-touching step in the job (build, test, lint, checkers) shows outcome=skipped. So unlike the expired earlier runs — where the retained metadata pointed at compilation-path failures at stages 5/10/11 — this head's red is a transient TLS reset fetching the elan installer, unrelated to the checkpoint chain, the artifact hand-off, or any .lean source. Stages 0–9 completing in sequence is affirmative evidence the cumulative-olean hand-off works on this head.

Two consequences:

1. The acceptance bar (one full 16-stage green run) is plausibly one rerun away — a maintainer "re-run failed jobs" on run 31678736948 resumes at stage-10 with the artifacts from 0–9 intact, which is precisely the recovery property this PR exists to provide. That would itself be a nice demonstration of the design.
2. Hardening worth one line while you're here: the elan download has no retry — a single connection reset kills a stage and skips the rest of the chain. If the upstream lean-action input allows it, prefer its toolchain cache; otherwise a curl --retry 5 --retry-all-errors wrapper (or a tiny retry loop around the install step in lean-build-stage.yml) would stop 54 ms of network weather from costing the whole staged pipeline. At 16 sequential stages, the chain hits the installer 16× per run, so the per-run flake probability compounds accordingly.

Not approving yet — the stated acceptance evidence (a fully green 16-stage run on the current head) still hasn't occurred — but the standing characterization of this head as compile-red is no longer accurate, and the block's own ask (fresh failure output) is satisfied above.

Provenance: AI-assisted review — anthropic/claude-fable-5 via Claude Code, slop.cash contribute-to-delta-star flow (skill installer refuses the stale published revision, so no signed receipt is attachable; disclosed rather than omitted).