fix(ci): resync actions.lock and add a lock-sync recurrence gate (#403) #59
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # This workflow is managed by gh actions-lock. | ||
| # SPDX-License-Identifier: MPL-2.0 | ||
| # This workflow is managed by gh actions-lock. | ||
| # Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | ||
| # Status Gate — fail when the PROOF-NEEDS.md / TEST-NEEDS.md count markers | ||
| # drift from coqc/cargo ground truth. | ||
| # | ||
| # Split into two independent jobs so the slow one is cancellable without | ||
| # losing the core gate: | ||
| # * status-gate-core — proof-count only (grep, ~1s, no toolchain). This is | ||
| # the CORE drift gate; this is the one to keep required. | ||
| # * status-gate-tests — test-count only (full `cargo` build, minutes). Slow, | ||
| # doc-hygiene-only; SAFE TO CANCEL if you're in a rush | ||
| # (it emits a ::notice:: saying so when it starts). | ||
| name: Status Gate | ||
| on: | ||
| pull_request: | ||
| paths: | ||
| - 'formal/**' | ||
| - 'PROOF-NEEDS.md' | ||
| - 'TEST-NEEDS.md' | ||
| - 'scripts/status-gate.sh' | ||
| - 'Cargo.toml' | ||
| - 'Cargo.lock' | ||
| - '**/Cargo.toml' | ||
| - '.github/workflows/status-gate.yml' | ||
| workflow_dispatch: | ||
| permissions: | ||
| contents: read | ||
| concurrency: | ||
| group: status-gate-${{ github.ref }} | ||
| cancel-in-progress: true | ||
| jobs: | ||
| # CORE — fast, no toolchain. Keep this one required: a new Admitted that | ||
| # isn't reflected in PROOF-NEEDS.md fails here in ~1 second. | ||
| status-gate-core: | ||
| name: status-gate-core | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 10 | ||
| steps: | ||
| - name: Checkout repository | ||
| uses: actions/checkout@v7.0.1 | ||
| - name: Proof-count drift (grep only — no build) | ||
| run: ./scripts/status-gate.sh --proofs | ||
| # SLOW — full cargo build to count tests. Cancellable: the core gate above | ||
| # is independent, so cancelling this never lets soundness/admit drift through. | ||
| status-gate-tests: | ||
| name: status-gate-tests (slow · cancellable) | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 30 | ||
| steps: | ||
| - name: Notice — this is the slow, skippable job | ||
| run: | | ||
| 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." | ||
| - name: Checkout repository | ||
| uses: actions/checkout@v7.0.1 | ||
| - name: Install Rust toolchain | ||
| uses: dtolnay/rust-toolchain@v1 | ||
| with: | ||
| toolchain: v1 | ||
| with: | ||
| toolchain: stable # required input when the action is SHA-pinned (the `stable` ref's default is not inherited by SHA) | ||
| - name: Cache cargo | ||
| uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 | ||
| - name: Test-count drift (full build — slow) | ||
| env: | ||
| CARGO_INCREMENTAL: "0" | ||
| run: ./scripts/status-gate.sh --tests | ||
