Skip to content

feat(ci): Lean proof + Bazel + proptest CI gates (#135)#151

Merged
avrabe merged 3 commits intomainfrom
feat/135-lean-bazel-ci
Apr 26, 2026
Merged

feat(ci): Lean proof + Bazel + proptest CI gates (#135)#151
avrabe merged 3 commits intomainfrom
feat/135-lean-bazel-ci

Conversation

@avrabe
Copy link
Copy Markdown
Contributor

@avrabe avrabe commented Apr 25, 2026

Summary

Adds the three CI gates required by issue #135 so that spar's existing verification artifacts (Lean proofs, rivet schemas, Bazel rules) become CI-gated evidence instead of documentation:

  • .github/workflows/proofs.yml — runs lake build against proofs/ on every PR + main push. Uses leanprover/lean-action@v1, which reads proofs/lean-toolchain (currently pinned to leanprover/lean4:v4.29.0-rc6). Mathlib + transitive .olean outputs are cached via actions/cache@v4 keyed on lean-toolchain + lake-manifest.json. On failure, per-target lake build logs are uploaded as the lake-build-log artifact for forensic review.
  • bazel-test job in ci.yml — wires up bazel test //... via bazelbuild/setup-bazelisk@v3, with ~/.cache/bazel cached. Currently continue-on-error: true and informational because there is no root MODULE.bazel/WORKSPACE yet (the tools/bazel/rules_* rules are consumed by generated BUILD files); the gate will flip the moment a root workspace marker lands — no follow-up workflow edit needed.
  • rivet-validate job in ci.yml — installs the rivet CLI pinned to the same v0.1.0 tag the existing compliance action uses, then runs rivet validate --format text. Mirrors the local pre-commit invariant from AGENTS.md.
  • Proptest — verified that Proptest (extended) already runs on every PR (the workflow's top-level on: covers it). Added a comment documenting the gate.
  • README badges — added Lean Proofs and Rivet validate badges next to the existing CI/codecov badges.
  • proofs/README.md — new doc covering the three verified theorems, the toolchain pin, and how CI consumes them.

Test plan

  • CI workflow Lean Proofs runs lake build to green on this PR (cold run will be slow — Mathlib is ~2 GB; subsequent runs reuse the cache).
  • CI workflow CI / Rivet validate (artifacts) runs rivet validate to green.
  • CI workflow CI / Bazel test (//...) runs and emits the informational warning (no MODULE.bazel yet); job is continue-on-error: true so it does not block.
  • CI workflow CI / Proptest (extended) continues to pass on this PR.
  • All existing CI jobs (Format, Clippy, Test, Security Audit, Cargo Deny, Code Coverage, Miri, Mutation Testing, Fuzz smoke, Supply Chain, Bench compile smoke, Kani) remain green.
  • README badges render on GitHub.

Local smoke tests

  • lake build — not run locally (sandbox lacks lake/elan). Validation will happen on the first CI run.
  • bazel test //... — not run locally; the repo also has no root MODULE.bazel, so the new job is intentionally informational until that lands. Documented in the workflow comment.

Deferred / follow-ups

  • Once a root MODULE.bazel (and any required BUILD.bazel files generated from spar codegen) is committed, flip bazel-test from continue-on-error: true to a hard gate.
  • Once the Lean proof job has had ~2 weeks of stable green runs, consider adding proofs.yml::lean to the required-checks list.

🤖 Generated with Claude Code

@codecov
Copy link
Copy Markdown

codecov Bot commented Apr 25, 2026

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

@avrabe avrabe force-pushed the feat/135-lean-bazel-ci branch from 0fd4fb9 to 54eae48 Compare April 25, 2026 09:09
@avrabe avrabe mentioned this pull request Apr 25, 2026
Merged
4 tasks
@avrabe avrabe force-pushed the feat/135-lean-bazel-ci branch from 54eae48 to 22d1b1a Compare April 25, 2026 13:42
avrabe added a commit that referenced this pull request Apr 25, 2026
@avrabe @claude
docs+test: Track A close-out (commit 4/4) — COMPLIANCE narrative + CL…
b2092fa 
…I integration (#154)

Closes the v0.7.0 Track A milestone:

- COMPLIANCE.md "In progress / v0.7.0" expanded into a full narrative
  covering all four Track A commits (foundation #145, hierarchical RTA
  #147, Lean convergence #148, this close-out), the Track B variant-
  contract foundation (#144), v0.7.x infrastructure landings (#141-143,
  #151), and v0.8.0 planning anchors (Track D #149/#152, Track E
  #150/#153).

- Updated header date to 2026-04-25 and crate count from "16 crates,
  1200+ tests" to "17 crates, 1900+ tests" reflecting the test growth
  through Track A and the v0.7.x infrastructure additions.

- New CLI integration test crates/spar-cli/tests/track_a_close_out.rs
  exercises the full parse → instance → analyze pipeline on a model
  using the Spar_Timing::ISR_* property surface plus a sporadic handler
  thread. The unit + fixture tests in spar-analysis cover the algorithm
  at the analysis-crate level; this test guards the property surface
  flowing through the CLI binary end-to-end.

Out-of-scope items explicitly recorded: PIP/PCP blocking deferred to
v0.7.1, multi-processor ISR migration deferred, cache-aware
interference inflation deferred to v1.0+.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Apr 25, 2026
@avrabe @claude
ci(proofs): enable mathlib precompiled cache + 90min timeout
c3e8895 
The first cold-cache run on #151 cancelled at ~98% Mathlib build
(module 2796 of 2845) when it hit the 60-minute GH Actions timeout.
Compiling Mathlib from source on a single runner takes ~70-90 min;
GitHub's hosted runners can't fit that in 60.

Two fixes, both standard Lean-community practice:

1. use-mathlib-cache: true — leanprover/lean-action runs
   `lake exe cache get` before `lake build`, pulling ~2 GB of
   precompiled `.olean` files from Mathlib's cloud cache instead of
   rebuilding from source. Cuts cold-cache time from 70+ min to
   roughly 5 min for the fetch + 1-2 min for our in-tree proofs.

2. timeout-minutes: 90 — covers a worst-case fetch path (slow S3,
   region thrash, etc.) without forcing future cancellations.

Warm runs (after actions/cache hits on `proofs/.lake`) land in well
under 10 minutes — those rebuild only modules that changed.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@avrabe avrabe force-pushed the feat/135-lean-bazel-ci branch from 22d1b1a to c3e8895 Compare April 25, 2026 15:41
@avrabe avrabe mentioned this pull request Apr 25, 2026
Merged
2 tasks
avrabe added a commit that referenced this pull request Apr 25, 2026
@avrabe @claude
fix(proofs): move RTAJittered.lean imports above all comments (#159)
c5b35df 
The Lean compiler requires `import` statements to appear before any
other top-level content (including doc-comment blocks `/- ... -/`).
The original file from #148 had two stacked comment blocks (a `/-!`
docstring then a `/- ... -/` overview) above the `import` lines, and
Lean 4.29.0-rc6 rejects that with:

    error: Proofs/Scheduling/RTAJittered.lean:35:0:
           invalid 'import' command, it must be used in the beginning
           of the file

Fix: merge the two blocks into a single `/-! ... -/` module docstring
that sits *before* the imports — Lean treats the leading docstring as
metadata, not as a top-level command, so imports following it are still
"at the beginning". Same content, different framing.

Discovered by the new Lean CI gate from #151 once Mathlib's precompiled
cache lands fast enough to actually reach our in-tree files.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Apr 25, 2026
@avrabe @claude
ci(proofs): enable mathlib precompiled cache + 90min timeout
1a564f8 
The first cold-cache run on #151 cancelled at ~98% Mathlib build
(module 2796 of 2845) when it hit the 60-minute GH Actions timeout.
Compiling Mathlib from source on a single runner takes ~70-90 min;
GitHub's hosted runners can't fit that in 60.

Two fixes, both standard Lean-community practice:

1. use-mathlib-cache: true — leanprover/lean-action runs
   `lake exe cache get` before `lake build`, pulling ~2 GB of
   precompiled `.olean` files from Mathlib's cloud cache instead of
   rebuilding from source. Cuts cold-cache time from 70+ min to
   roughly 5 min for the fetch + 1-2 min for our in-tree proofs.

2. timeout-minutes: 90 — covers a worst-case fetch path (slow S3,
   region thrash, etc.) without forcing future cancellations.

Warm runs (after actions/cache hits on `proofs/.lake`) land in well
under 10 minutes — those rebuild only modules that changed.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@avrabe avrabe force-pushed the feat/135-lean-bazel-ci branch from c3e8895 to 1a564f8 Compare April 25, 2026 22:21
@avrabe avrabe mentioned this pull request Apr 25, 2026
Merged
1 task
avrabe added a commit that referenced this pull request Apr 26, 2026
@avrabe @claude
fix(proofs): use /- ... -/ block comment to match RTA.lean style (#165)
3bed345 
Lean 4.29.0-rc6 rejects `import` after a `/-! ... -/` module-docstring
in this file's pattern, even though Mathlib uses module docstrings
throughout — likely an interaction with the closing `-/` being on the
same line as content text. The other working files in this directory
(RTA.lean, RMBound.lean, EDF.lean) all use a regular `/- ... -/`
block comment with the closing `-/` on its own line, so we match that
style.

#159 (the previous import-order fix) addressed the structural ordering
but introduced the `/-!` form. CI surfaced that in #151's first run
that actually reached our in-tree files via mathlib-cache.

Body unchanged. Format-only edit.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe and others added 3 commits April 26, 2026 08:50
@avrabe @claude
feat(ci): Lean proof + Bazel + proptest CI gates (#135)
1b4d7a9 
Adds three CI gates that promote spar's verification artifacts from
"documentation that should be checked" to "CI-gated evidence":

- .github/workflows/proofs.yml — `lake build` for proofs/, with
  Mathlib cache and audit artifact upload
- bazel-test job in ci.yml — `bazel test //...` for the full
  Rust + Lean + Bazel target sweep
- Proptest CI confirmation — extended-cases run on every PR

Lean toolchain pinned via lean-toolchain file (matches rules_lean
4.27.0 per issue notes). Mathlib is cached on `lake-manifest.json`
hash to avoid recompiles.

Status badges added to README for Rust CI, Lean proofs, rivet validate.

Closes #135.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@avrabe @claude
ci: bump rivet pin v0.1.0 -> v0.4.3 for unknown-field tolerance
d8f236f 
The rivet-validate job pinned to v0.1.0 was treating legitimate
schema-extension fields (used by Track A/B/D/E artifacts and EU AI
Act / IEC 62304 / DO-178C bridges) as hard errors. v0.4.x reclassifies
unknown-field warnings to INFO level — matching what `rivet validate`
returns locally on the same artifact set today (PASS, 91 INFO).

release.yml still pins v0.1.0 for its legacy compliance-action; that's
a separate cleanup, not blocking this PR.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@avrabe @claude
ci(proofs): enable mathlib precompiled cache + 90min timeout
e443aab 
The first cold-cache run on #151 cancelled at ~98% Mathlib build
(module 2796 of 2845) when it hit the 60-minute GH Actions timeout.
Compiling Mathlib from source on a single runner takes ~70-90 min;
GitHub's hosted runners can't fit that in 60.

Two fixes, both standard Lean-community practice:

1. use-mathlib-cache: true — leanprover/lean-action runs
   `lake exe cache get` before `lake build`, pulling ~2 GB of
   precompiled `.olean` files from Mathlib's cloud cache instead of
   rebuilding from source. Cuts cold-cache time from 70+ min to
   roughly 5 min for the fetch + 1-2 min for our in-tree proofs.

2. timeout-minutes: 90 — covers a worst-case fetch path (slow S3,
   region thrash, etc.) without forcing future cancellations.

Warm runs (after actions/cache hits on `proofs/.lake`) land in well
under 10 minutes — those rebuild only modules that changed.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@avrabe avrabe force-pushed the feat/135-lean-bazel-ci branch from 1a564f8 to e443aab Compare April 26, 2026 06:51
@avrabe avrabe merged commit 4a4a747 into main Apr 26, 2026
17 checks passed
@avrabe avrabe deleted the feat/135-lean-bazel-ci branch April 26, 2026 13:15
@avrabe avrabe mentioned this pull request Apr 26, 2026
Merged
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@avrabe