Make setup and generated skill current #306

Workflow file for this run

	name: ci

	on:
	push:
	branches: [main]
	pull_request:

	# Cancel a PR's superseded in-flight run when a new commit is pushed (the
	# kickoff-agent loop waits on this CI, so stale runs are pure latency). Main
	# pushes are NOT cancelled: those runs are the verification record of record.
	concurrency:
	group: ci-${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: ${{ github.event_name == 'pull_request' }}

	# Two jobs, run in parallel (REQ-5 — the full gauntlet still runs; a non-zero
	# exit in any step fails CI, R-DEFER-6):
	#
	# checks — the compile-light gates: fmt, clippy, the python doc-drift gate,
	# the skill-budget gate, and doctests. Run once.
	# test — the Verus/Z3-backed conformance suite plus mandatory live Lean replay,
	# which dominates wall-clock
	# (~100 of the workspace's integration-test binaries invoke the real
	# solver). Profiling showed this is test EXECUTION time, not compile
	# time, so it is sharded across N runners with cargo-nextest's
	# partitioning; wall-clock drops ~linearly with the shard count.
	#
	# Both jobs install the pinned Rust toolchain (rust-toolchain.toml channel,
	# 1.95.0) and restore the shared Rust build cache + pinned Verus distribution.
	# The test shards also build the Lean modules and install the pinned
	# CaDiCaL/drat-trim pair used by live reconstruction tests; a missing proof
	# dependency is a hard failure, not a skipped test. Verus is the L3 verification
	# gate (it bundles the matching rust toolchain + z3); tests resolve it via
	# VERUS_BIN.
	# The skill-budget gate fails CI if the generated THERMITE.skill.md exceeds its
	# 6,000-token budget (design §2.2 / §10).
	jobs:
	checks:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# Full history: the doc-drift tripwire's commit-set predicate
	# (`git log --full-history <pin>..HEAD`) and pin validation
	# (`merge-base --is-ancestor`) need the pinned commits present; a
	# shallow clone would mis-class every pin as INVALID-PIN.
	fetch-depth: 0

	- name: Install toolchain (pinned to rust-toolchain.toml channel)
	uses: dtolnay/rust-toolchain@1.95.0
	with:
	components: rustfmt, clippy

	# Fail-fast: the cheap, no-compile gates first.
	- name: cargo fmt
	run: cargo fmt --all --check

	- name: tooling gate tests (tooling/tests)
	run: python3 -m unittest discover -s tooling/tests
	- name: doc-drift tripwire (design-doc freshness)
	run: python3 tooling/doc-drift.py
	# The gate that guards the gates (crosslink #93): asserts the two
	# agent-facing hooks are still WIRED in the tracked settings.json, which
	# `crosslink init` regenerates and 5581b65f silently clobbered.
	- name: control-plane gate (hook wiring)
	run: python3 tooling/control-plane-check.py
	- name: req-status lint (source-comment status consistency)
	run: python3 tooling/req-status.py
	- name: req-registry gate (canonical status inventory)
	run: tooling/reqs check

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	# Distinct cache slot from the test job: this job builds with
	# `--all-targets` for clippy, a different artifact set.
	key: checks

	# Verus is restored here too so doctests that exercise the solver path
	# still run (the old single-job `cargo test --workspace` ran doctests).
	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	- name: cargo clippy
	run: cargo clippy --workspace --all-targets -- -D warnings

	# Stage-3 REQ-1 / AC-1: the @bv tag's build-flag gate (the structural lock
	# R-BV-1). The default `cargo nextest run --workspace` (in the `test` job)
	# already exercises the NEGATIVE half — the tag is a parse error without the
	# `bv` plumbing. Here we additionally (a) clippy and (b) test the
	# POSITIVE half: with `--features bv`, all four widths + `nowrap`
	# parse with the AST tag recovered. Both halves of AC-1 thus run in one CI
	# run. (`.design/stage3-bv-reconstruction.md` REQ-1.)
	- name: bv build-flag gate (stage-3 REQ-1 / AC-1)
	run: \|
	cargo clippy -p thermite-syntax --all-targets --features bv -- -D warnings
	cargo test -p thermite-syntax --features bv --test bv_tag_parse

	# nextest does not run doctests; run them here so coverage matches the
	# previous `cargo test --workspace`.
	- name: cargo test --doc
	run: cargo test --doc --workspace

	- name: skill budget gate (issue #7, design §2.2 / §10)
	run: cargo run -p thermite-skill -- --check-budget

	test:
	runs-on: ubuntu-latest
	strategy:
	# Surface every shard's failures, not just the first.
	fail-fast: false
	matrix:
	shard: [1, 2, 3, 4]
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# Some conformance tests (audit/doc-drift) read git history.
	fetch-depth: 0

	- name: Install elan (Lean toolchain manager)
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build (.lake)
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch prebuilt Mathlib cache (oleans)
	working-directory: lean
	run: lake exe cache get

	- name: Build modules used by live Lean tests
	working-directory: lean
	run: >-
	lake build
	Thermite.Stabilize
	Thermite.Exec.Stmt
	Thermite.Exec.WhileBody
	Thermite.Strat.Cls.Wire
	Thermite.Reconstruct

	- name: Install toolchain (pinned to rust-toolchain.toml channel)
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: test

	- name: Install cargo-nextest
	uses: taiki-e/install-action@v2
	with:
	tool: nextest

	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	- name: Cache Stage 4 proof tools
	uses: actions/cache@v4
	with:
	path: target/g4-tools
	key: g4-tools-${{ hashFiles('scripts/g4-toolchain.env', 'scripts/g4-tools/drat-trim') }}

	- name: Install pinned CaDiCaL and drat-trim
	run: \|
	bash scripts/install-g4-tools.sh
	echo "THERMITE_EPR_CADICAL=$PWD/target/g4-tools/bin/cadical" >> "$GITHUB_ENV"
	echo "THERMITE_EPR_DRAT_TRIM=$PWD/target/g4-tools/bin/drat-trim" >> "$GITHUB_ENV"

	# Shard the suite across the matrix: nextest assigns each test to one
	# partition deterministically, so the union of shards is the full suite.
	- name: cargo nextest run (shard ${{ matrix.shard }}/4)
	run: cargo nextest run --workspace --partition count:${{ matrix.shard }}/4

	# The Lean spine + axiom probe (trust-audit finding F4: until now `lake build` and the
	# `#print axioms` gate ran only in a local `make audit`, so a commit breaking the Lean
	# build or a relax-spine lemma acquiring a disallowed axiom would go unseen in CI).
	# SPLIT into two parallel jobs (#340, CI speedup options 2+3 — zero coverage loss):
	# lean-probe — `lake build` the spine subset + the `#print axioms` gate
	# (scripts/lean-axiom-probe.sh, the same check [1] `make audit`
	# runs, so local and CI cannot drift).
	# lean-spine-forge — an independent run of the spine-gated forge tests.
	# The ordinary test matrix also provisions Lean so a missing
	# dependency cannot turn a live replay into an accidental skip.
	# This dedicated matrix keeps the Lean-backed gate visible and
	# shards the slow Verus discharges four ways.
	# Each job restores the shared lean-${{ hashFiles(...) }} `.lake` cache independently
	# (no `needs:` between them → they run concurrently; on a warm cache the per-job
	# `lake build` is incremental). lean-smt is SHA-pinned; Mathlib oleans come from the
	# cloud cache (`lake exe cache get`).
	#
	# OPTION 1 (future, deliberately NOT done here): trim lean-spine-forge to ONLY the
	# spine-gated tests (dropping the redundancy with the `test` shards on non-spine forge
	# tests). Deferred because a name-PATTERN filter risks SILENT coverage drift — a
	# spine-gated test the pattern misses would run in NEITHER place (skipped in `test`,
	# excluded here). Doing it safely needs the spine-gated tests TAGGED as a stable nextest
	# test-group (a test-code change) so the selector can't drift. Until then we run the
	# full `-p forge` (sharded) — redundant on non-spine tests, but provably complete.
	lean-probe:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# forge's audit/doc-drift conformance tests read git history
	fetch-depth: 0

	- name: Install elan (Lean toolchain manager)
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build (.lake)
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	# Keyed on the dep lockfile + toolchain pin: a lean-smt/Mathlib bump or a
	# toolchain change busts the cache; spine edits reuse it (lake rebuilds only the
	# changed modules).
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch prebuilt Mathlib cache (oleans)
	working-directory: lean
	# Without this the relax island's `import Mathlib.Data.Real.Basic` would compile a
	# large slice of Mathlib from source (hours). The cache makes it olean loads.
	run: lake exe cache get

	- name: Lean spine build + axiom probe (lake build + #print axioms gate)
	run: bash scripts/lean-axiom-probe.sh

	# The independent spine-GATED forge tests (Audit F4 / #309). Lean + Verus are
	# mandatory here and in the ordinary test matrix; missing dependencies fail rather
	# than silently reducing coverage. Sharded 4 ways so the slow Verus discharges run in
	# parallel; the union is the whole `-p forge` suite. Restores the same `.lake` cache
	# as lean-probe; no `needs:` so it runs concurrently.
	lean-spine-forge:
	runs-on: ubuntu-latest
	strategy:
	# Surface every shard's failures, not just the first.
	fail-fast: false
	matrix:
	shard: [1, 2, 3, 4]
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	# forge's audit/doc-drift conformance tests read git history
	fetch-depth: 0

	- name: Install elan (Lean toolchain manager)
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build (.lake)
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	# Same key as lean-probe — both restore the shared spine build.
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch prebuilt Mathlib cache (oleans)
	working-directory: lean
	run: lake exe cache get

	- name: Build the spine modules forge's live Lean drivers need
	working-directory: lean
	# forge's `--engine lean` export imports `Thermite.Stabilize` / `Exec.Stmt` /
	# `Exec.WhileBody` (NOT the root `Thermite`, which pulls the cvc5-FFI `SmtDemo`);
	# the REQ-4 differential battery runs `lake env lean --run Thermite/Strat/Cls/Wire.lean`,
	# which needs `Thermite.Strat.Cls.Wire` built (it pulls Fragment/Graph/Nnf
	# transitively). The old monolithic job got the Strat oleans for free from the
	# axiom-probe's `lake build`; this split moved the probe to `lean-probe`, so the
	# forge job must build Wire itself. Without these the live tests fail with
	# "unknown module prefix 'Thermite'" / "spine may not be built". Incremental on a
	# warm `.lake` cache.
	run: >-
	lake build
	Thermite.Stabilize
	Thermite.Exec.Stmt
	Thermite.Exec.WhileBody
	Thermite.Strat.Cls.Wire
	Thermite.Reconstruct

	- name: Install Rust toolchain (pinned)
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: lean-spine-tests

	- name: Install cargo-nextest
	uses: taiki-e/install-action@v2
	with:
	tool: nextest

	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus (L3 verification gate — pinned to dev version)
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version

	- name: Cache Stage 4 proof tools
	uses: actions/cache@v4
	with:
	path: target/g4-tools
	key: g4-tools-${{ hashFiles('scripts/g4-toolchain.env', 'scripts/g4-tools/drat-trim') }}

	- name: Install pinned CaDiCaL and drat-trim
	run: \|
	bash scripts/install-g4-tools.sh
	echo "THERMITE_EPR_CADICAL=$PWD/target/g4-tools/bin/cadical" >> "$GITHUB_ENV"
	echo "THERMITE_EPR_DRAT_TRIM=$PWD/target/g4-tools/bin/drat-trim" >> "$GITHUB_ENV"

	# Shard the forge suite WITH the spine present: nextest assigns each test to one
	# partition deterministically, so shards 1..4 union to the full `-p forge` suite —
	# the spine-gated live tests are distributed across shards and every one runs.
	- name: forge tests WITH the spine, shard ${{ matrix.shard }}/4 (lake-gated live tests run here)
	run: cargo nextest run -p forge --partition count:${{ matrix.shard }}/4

	- name: Stage-2 G2 gate — fixed-seed differential + two-phase sweep ([8] / [9])
	# The reproducible per-PR half of REQ-9 checks [8]/[9] (`.design/stage2-stratified-cage.md`
	# REQ-9 / AC-9): the classifier differential battery (Rust classifier ≡ Lean
	# `Thermite.Strat.Cls.admitted` over generated formulae, the Lean side via
	# `lake env lean --run`) and the stratified two-phase TV sweep, both at the pinned
	# default seed. The rotating-seed half is the scheduled `generated-tv` job. A
	# classifier disagreement / tripwire ([8]) or a divergence / withheld clause ([9])
	# is a verification-failure exit and fails the job. lake is on PATH here, so
	# `strat-tv` takes its RUN branch (not the honest lake-absent SKIP).
	#
	# This is a single whole-corpus gate, NOT a partitioned test, so run it ONCE
	# (shard 1) — its env (lake + the spine incl Strat.Cls.Wire + Rust + Verus) is
	# present in every lean-spine-forge shard; gating on shard 1 avoids running it 4×.
	if: ${{ matrix.shard == 1 }}
	run: \|
	set -euo pipefail
	cargo run -q -p forge -- strat-tv
	cargo run -q -p forge -- strat-faithful-tv

	# Keep the parser lock, fixed-width checks, and Lean replay in one gate.
	g3:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Install elan
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch Mathlib cache
	working-directory: lean
	run: lake exe cache get

	- name: Cache Verus
	uses: actions/cache@v4
	with:
	path: ~/verus-dist
	key: verus-0.2026.05.24.ecee80a-x86-linux

	- name: Install Verus and Z3
	run: \|
	set -euo pipefail
	VERUS_VER="0.2026.05.24.ecee80a"
	if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null \| grep -q .; then
	curl -fsSL -o /tmp/verus.zip \
	"https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip"
	mkdir -p "$HOME/verus-dist"
	unzip -q /tmp/verus.zip -d "$HOME/verus-dist"
	fi
	VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus \| head -1)"
	test -n "$VERUS_BIN_PATH"
	echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV"
	echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH"
	"$VERUS_BIN_PATH" --version
	"$(dirname "$VERUS_BIN_PATH")/z3" --version

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: g3

	- name: Gate G3
	run: bash scripts/g3-gate.sh

	# Stage 4 closes the admitted S₂.0 relation/array residual. Keep its pinned
	# SAT/LRAT tools and complete replay matrix visible as one fail-fast check.
	g4:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

	- name: Install Rust toolchain
	uses: dtolnay/rust-toolchain@1.95.0

	- name: Install elan
	run: \|
	set -euo pipefail
	curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh
	bash /tmp/elan-init.sh -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

	- name: Cache Lean build
	uses: actions/cache@v4
	with:
	path: \|
	lean/.lake/packages
	lean/.lake/build
	key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }}
	restore-keys: \|
	lean-

	- name: Fetch Mathlib cache
	working-directory: lean
	run: lake exe cache get

	- name: Install Z3 witness solver
	run: \|
	set -euo pipefail
	sudo apt-get update
	sudo apt-get install --yes z3
	z3 --version

	- name: Cache Stage 4 proof tools
	uses: actions/cache@v4
	with:
	path: target/g4-tools
	key: g4-tools-${{ hashFiles('scripts/g4-toolchain.env', 'scripts/g4-tools/drat-trim') }}

	- name: Install pinned CaDiCaL and drat-trim
	run: bash scripts/install-g4-tools.sh

	- name: Rust build cache
	uses: Swatinem/rust-cache@v2
	with:
	key: g4

	- name: Gate G4
	run: bash scripts/g4-gate.sh

Navigation Menu

Uh oh!

Make setup and generated skill current #306

Workflow file

Make setup and generated skill current #306

Uh oh!

Workflow file for this run