Skip to content

Commit 818492f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
ci: split status-gate (fast core / slow-cancellable tests) + fix rust-ci toolchain
status-gate: - scripts/status-gate.sh gains --proofs / --tests / (both) modes. - status-gate.yml split into two jobs: * status-gate-core — proof-count only (grep, ~1s, no toolchain). The core drift gate; the one to keep required. * status-gate-tests — test-count only (full cargo build, minutes). Emits a ::notice:: that it is the slow, doc-hygiene-only job and is SAFE TO CANCEL when rushing, since the core gate is independent. Cancelling it never lets admit/soundness drift through. rust-ci: the no-default-features and wasm-validate jobs SHA-pin dtolnay/rust-toolchain without `with: toolchain:` — and there is no rust-toolchain.toml, so the step failed with "'toolchain' is a required input" (latest rust-ci run = failure). Same footgun fixed in #302's status-gate; add the explicit input to both jobs. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 2275698 commit 818492f

3 files changed

Lines changed: 85 additions & 39 deletions

File tree

‎.github/workflows/rust-ci.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,8 @@ jobs:
3737

3838
- name: Install Rust toolchain
3939
uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # stable
40+
with:
41+
toolchain: stable # required when SHA-pinned (no rust-toolchain.toml in repo)
4042

4143
- name: Cache cargo registry and build
4244
uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
@@ -76,6 +78,8 @@ jobs:
7678

7779
- name: Install Rust toolchain
7880
uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # stable
81+
with:
82+
toolchain: stable # required when SHA-pinned (no rust-toolchain.toml in repo)
7983

8084
- name: Cache cargo registry and build
8185
uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2

‎.github/workflows/status-gate.yml‎

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,15 @@
11
# SPDX-License-Identifier: MPL-2.0
22
# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3-
# Status Gate — fail a PR when the PROOF-NEEDS.md / TEST-NEEDS.md count
4-
# markers drift from coqc/cargo ground truth. This wires the previously
5-
# broken (`//` syntax error on line 3) + unwired scripts/status-gate.sh
6-
# into CI so admit-count / test-count drift is caught automatically.
7-
# NOTE: not yet a required status check — see .github/settings.yml.
3+
# Status Gate — fail when the PROOF-NEEDS.md / TEST-NEEDS.md count markers
4+
# drift from coqc/cargo ground truth.
5+
#
6+
# Split into two independent jobs so the slow one is cancellable without
7+
# losing the core gate:
8+
# * status-gate-core — proof-count only (grep, ~1s, no toolchain). This is
9+
# the CORE drift gate; this is the one to keep required.
10+
# * status-gate-tests — test-count only (full `cargo` build, minutes). Slow,
11+
# doc-hygiene-only; SAFE TO CANCEL if you're in a rush
12+
# (it emits a ::notice:: saying so when it starts).
813
name: Status Gate
914

1015
on:
@@ -28,10 +33,26 @@ concurrency:
2833
cancel-in-progress: true
2934

3035
jobs:
31-
status-gate:
32-
name: status-gate
36+
# CORE — fast, no toolchain. Keep this one required: a new Admitted that
37+
# isn't reflected in PROOF-NEEDS.md fails here in ~1 second.
38+
status-gate-core:
39+
name: status-gate-core
3340
runs-on: ubuntu-latest
3441
steps:
42+
- name: Checkout repository
43+
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
44+
- name: Proof-count drift (grep only — no build)
45+
run: ./scripts/status-gate.sh --proofs
46+
47+
# SLOW — full cargo build to count tests. Cancellable: the core gate above
48+
# is independent, so cancelling this never lets soundness/admit drift through.
49+
status-gate-tests:
50+
name: status-gate-tests (slow · cancellable)
51+
runs-on: ubuntu-latest
52+
steps:
53+
- name: Notice — this is the slow, skippable job
54+
run: |
55+
echo "::notice title=Slow check — safe to cancel::status-gate-tests runs a full cargo build just to verify the TEST-NEEDS.md test count. The core proof-count gate (status-gate-core) is a separate, independent job and is already enforced. If you're in a rush you can cancel THIS job without letting any core gating go."
3556
- name: Checkout repository
3657
uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
3758
- name: Install Rust toolchain
@@ -40,7 +61,7 @@ jobs:
4061
toolchain: stable # required input when the action is SHA-pinned (the `stable` ref's default is not inherited by SHA)
4162
- name: Cache cargo
4263
uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
43-
- name: Run status-gate (proof + test count drift)
64+
- name: Test-count drift (full build — slow)
4465
env:
4566
CARGO_INCREMENTAL: "0"
46-
run: ./scripts/status-gate.sh
67+
run: ./scripts/status-gate.sh --tests

‎scripts/status-gate.sh‎

Lines changed: 51 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,24 @@
11
#!/usr/bin/env bash
22
# SPDX-License-Identifier: MPL-2.0
33
# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
#
5+
# status-gate.sh — fail when the doc count markers drift from ground truth.
6+
#
7+
# Two independent checks, selectable so CI can run the cheap one as a
8+
# required gate and the expensive one as a separate, cancellable job:
9+
#
10+
# --proofs Proof-count only: greps formal/*.v for `Admitted.` and
11+
# compares to PROOF-NEEDS.md. No toolchain, runs in ~1s.
12+
# This is the CORE gate — keep it required.
13+
# --tests Test-count only: `cargo test --all-targets -- --list` and
14+
# compares to TEST-NEEDS.md. Needs a full Rust build (minutes).
15+
# SAFE TO SKIP / CANCEL if you are in a rush — it never gates
16+
# soundness, only doc-count hygiene for the test inventory.
17+
# (no arg) Both (the local `just status-gate` default).
418
set -euo pipefail
519

20+
MODE="${1:-all}"
21+
622
ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
723
cd "$ROOT_DIR"
824

@@ -21,33 +37,38 @@ extract_claim() {
2137
echo "$line" | grep -Eo '[0-9]+' | head -n 1
2238
}
2339

24-
# Single-source claim: PROOF-NEEDS.md §4 carries the canonical
25-
# `Coq admitted proofs remaining: <n>` marker. ROADMAP.adoc no longer
26-
# duplicates this; see the per-file table + seam audit in PROOF-NEEDS.md.
27-
PROOF_NEEDS_CLAIM="$(extract_claim "PROOF-NEEDS.md" "Coq admitted proofs remaining")"
28-
TEST_NEEDS_CLAIM="$(extract_claim "TEST-NEEDS.md" "Documented all-target tests")"
29-
30-
ACTUAL_ADMITTED="$(
31-
(grep -R --include='*.v' -n '^[[:space:]]*Admitted\.' formal || true) \
32-
| wc -l \
33-
| tr -d ' '
34-
)"
35-
36-
if [ "$PROOF_NEEDS_CLAIM" != "$ACTUAL_ADMITTED" ]; then
37-
fail "PROOF-NEEDS.md claims ${PROOF_NEEDS_CLAIM} admitted proofs, actual is ${ACTUAL_ADMITTED}"
38-
fi
39-
40-
ACTUAL_TESTS="$(
41-
cargo test --all-targets -- --list \
42-
| grep ': test$' \
43-
| wc -l \
44-
| tr -d ' '
45-
)"
46-
47-
if [ "$TEST_NEEDS_CLAIM" != "$ACTUAL_TESTS" ]; then
48-
fail "TEST-NEEDS.md claims ${TEST_NEEDS_CLAIM} tests, actual is ${ACTUAL_TESTS}"
49-
fi
50-
51-
echo "status-gate: OK"
52-
echo " admitted proofs: ${ACTUAL_ADMITTED}"
53-
echo " all-target tests: ${ACTUAL_TESTS}"
40+
check_proofs() {
41+
# Single-source claim: PROOF-NEEDS.md §4 carries the canonical
42+
# `Coq admitted proofs remaining: <n>` marker. ROADMAP.adoc no longer
43+
# duplicates this; see the per-file table + seam audit in PROOF-NEEDS.md.
44+
local claim actual
45+
claim="$(extract_claim "PROOF-NEEDS.md" "Coq admitted proofs remaining")"
46+
actual="$(
47+
(grep -R --include='*.v' -n '^[[:space:]]*Admitted\.' formal || true) \
48+
| wc -l | tr -d ' '
49+
)"
50+
if [ "$claim" != "$actual" ]; then
51+
fail "PROOF-NEEDS.md claims ${claim} admitted proofs, actual is ${actual}"
52+
fi
53+
echo "status-gate[proofs]: OK — admitted proofs: ${actual}"
54+
}
55+
56+
check_tests() {
57+
local claim actual
58+
claim="$(extract_claim "TEST-NEEDS.md" "Documented all-target tests")"
59+
actual="$(
60+
cargo test --all-targets -- --list \
61+
| grep ': test$' | wc -l | tr -d ' '
62+
)"
63+
if [ "$claim" != "$actual" ]; then
64+
fail "TEST-NEEDS.md claims ${claim} tests, actual is ${actual}"
65+
fi
66+
echo "status-gate[tests]: OK — all-target tests: ${actual}"
67+
}
68+
69+
case "$MODE" in
70+
--proofs) check_proofs ;;
71+
--tests) check_tests ;;
72+
all|"") check_proofs; check_tests ;;
73+
*) fail "unknown mode '${MODE}' (use --proofs, --tests, or no argument)" ;;
74+
esac

0 commit comments

Comments
 (0)