ephapax/.github/workflows/status-gate.yml at 3b87f9021fc434d421cbf1a0fb45947c9079bab2 · hyperpolymath/ephapax · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
# 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: 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@v2.9.2
      - name: Test-count drift (full build — slow)
        env:
          CARGO_INCREMENTAL: "0"
        run: ./scripts/status-gate.sh --tests