|
94 | 94 | idris2 --check src/Proven/SafeDateTime.idr |
95 | 95 | idris2 --check src/Proven/SafeNetwork.idr |
96 | 96 |
|
| 97 | + # Fast, targeted gate over every Proofs.idr companion module. |
| 98 | + # |
| 99 | + # Rationale (issue #145): the swapped-arg `appendLengthInc` break (#127) |
| 100 | + # reached main because the only job that compiles the proof modules is the |
| 101 | + # slow full `build` above (~12-20 min on a warm runner), which merges |
| 102 | + # routinely outrace. The explicit "Type check all modules" list above |
| 103 | + # covers zero Proofs.idr files — exactly the modules the discharge campaign |
| 104 | + # keeps editing. This job type-checks ALL of them, independently and in |
| 105 | + # parallel with `build`, so a non-compiling proof is caught fast. Make THIS |
| 106 | + # job a required status check on main (branch protection) to close the gate. |
| 107 | + proof-check: |
| 108 | + runs-on: ubuntu-latest |
| 109 | + timeout-minutes: 30 |
| 110 | + strategy: |
| 111 | + matrix: |
| 112 | + idris2-version: ['0.8.0'] |
| 113 | + |
| 114 | + steps: |
| 115 | + - name: Checkout |
| 116 | + uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 |
| 117 | + |
| 118 | + - name: Install Idris 2 dependencies |
| 119 | + run: | |
| 120 | + sudo apt-get update |
| 121 | + sudo apt-get install -y chezscheme libgmp-dev |
| 122 | +
|
| 123 | + # Cache the Idris2 compiler + bundled packages (base/contrib/network) |
| 124 | + # only. This job never runs `idris2 --install proven.ipkg` and never |
| 125 | + # caches `build/`, so every run type-checks the CURRENT source of each |
| 126 | + # Proofs.idr — a stale cache cannot mask a source-level break. |
| 127 | + - name: Cache Idris 2 |
| 128 | + id: cache-idris2 |
| 129 | + uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0 |
| 130 | + with: |
| 131 | + path: | |
| 132 | + ~/.idris2 |
| 133 | + ~/idris2-${{ matrix.idris2-version }} |
| 134 | + key: idris2-${{ matrix.idris2-version }}-${{ runner.os }} |
| 135 | + |
| 136 | + - name: Install Idris 2 |
| 137 | + if: steps.cache-idris2.outputs.cache-hit != 'true' |
| 138 | + run: | |
| 139 | + git clone --depth 1 --branch v${{ matrix.idris2-version }} https://github.com/idris-lang/Idris2.git ~/idris2-${{ matrix.idris2-version }} |
| 140 | + cd ~/idris2-${{ matrix.idris2-version }} |
| 141 | + make bootstrap SCHEME=chezscheme |
| 142 | + make install |
| 143 | +
|
| 144 | + - name: Add Idris 2 to PATH |
| 145 | + run: echo "$HOME/.idris2/bin" >> $GITHUB_PATH |
| 146 | + |
| 147 | + - name: Type check the proof modules in proven.ipkg |
| 148 | + # Scope: every `*.Proofs` module LISTED IN proven.ipkg — i.e. the proof |
| 149 | + # modules the package actually builds. (64 of the 93 Proofs.idr files on |
| 150 | + # disk are intentionally absent from the package: env-blocked on retired |
| 151 | + # stdlib like Data.Nat.Division, or work-in-progress. Gating on those |
| 152 | + # would be stricter than `build` itself.) |
| 153 | + # |
| 154 | + # Run from the package source root (proven.ipkg `sourcedir = src`) with |
| 155 | + # module-relative paths. Idris2 matches a module's dotted namespace |
| 156 | + # against trailing path segments, so `Proven/Foo/Proofs.idr` resolves |
| 157 | + # `module Proven.Foo.Proofs` whereas `src/Proven/Foo/Proofs.idr` raises a |
| 158 | + # spurious "module name does not match file name". The clean `build/` |
| 159 | + # removal guarantees a stale TTC cannot mask a real break. |
| 160 | + run: | |
| 161 | + set -uo pipefail |
| 162 | + grep -oE 'Proven\.[A-Za-z0-9]+(\.[A-Za-z0-9]+)*\.Proofs' proven.ipkg \ |
| 163 | + | sort -u | sed 's#\.#/#g; s#$#.idr#' > /tmp/proof_modules.txt |
| 164 | + echo "Proof modules from proven.ipkg:"; cat /tmp/proof_modules.txt |
| 165 | + cd src |
| 166 | + rm -rf build |
| 167 | + fail=0 |
| 168 | + checked=0 |
| 169 | + while IFS= read -r f; do |
| 170 | + [ -f "$f" ] || { echo "::error file=proven.ipkg::listed proof module missing on disk: src/$f"; fail=1; continue; } |
| 171 | + checked=$((checked + 1)) |
| 172 | + echo "::group::idris2 --check $f" |
| 173 | + if idris2 -p contrib -p network --check "$f"; then |
| 174 | + echo "PASS $f" |
| 175 | + else |
| 176 | + echo "::error file=src/$f::idris2 --check failed" |
| 177 | + fail=1 |
| 178 | + fi |
| 179 | + echo "::endgroup::" |
| 180 | + done < /tmp/proof_modules.txt |
| 181 | + echo "Checked $checked proof module(s); fail=$fail" |
| 182 | + exit "$fail" |
| 183 | +
|
97 | 184 | docs: |
98 | 185 | runs-on: ubuntu-latest |
99 | 186 | needs: build |
|
0 commit comments