From f679205c2971eab80a666cb41c8d24d753fdf54a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sun, 31 May 2026 07:03:15 +0000
Subject: [PATCH] ci(idris): add fast proof-check gate over all Proofs.idr
 (#145)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds a dedicated `proof-check` job to idris2-ci.yml that type-checks every
src/**/Proofs.idr (glob-discovered) with `idris2 -p contrib -p network
--check`, in parallel with the slow full `build`.

Closes the gap that let #127's swapped-arg `appendLengthInc` reach main:
the full build was too slow to gate (merges outraced it while queued), and
the explicit per-module --check list covered ZERO Proofs.idr files — exactly
the modules the discharge campaign edits each PR.

The job never installs proven and never caches build/, so a stale cache
cannot mask a source-level break. Documents the decision as ADR-004; the
remaining step (make proof-check a REQUIRED status check via branch
protection) is an admin action tracked in #145.

Refs #145, #144, #127.

https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy
---
 .github/workflows/idris2-ci.yml | 70 +++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/.github/workflows/idris2-ci.yml b/.github/workflows/idris2-ci.yml
index 28b58afc..20520786 100644
--- a/.github/workflows/idris2-ci.yml
+++ b/.github/workflows/idris2-ci.yml
@@ -94,6 +94,76 @@ jobs:
           idris2 --check src/Proven/SafeDateTime.idr
           idris2 --check src/Proven/SafeNetwork.idr
 
+  # Fast, targeted gate over every Proofs.idr companion module.
+  #
+  # Rationale (issue #145): the swapped-arg `appendLengthInc` break (#127)
+  # reached main because the only job that compiles the proof modules is the
+  # slow full `build` above (~12-20 min on a warm runner), which merges
+  # routinely outrace. The explicit "Type check all modules" list above
+  # covers zero Proofs.idr files — exactly the modules the discharge campaign
+  # keeps editing. This job type-checks ALL of them, independently and in
+  # parallel with `build`, so a non-compiling proof is caught fast. Make THIS
+  # job a required status check on main (branch protection) to close the gate.
+  proof-check:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    strategy:
+      matrix:
+        idris2-version: ['0.8.0']
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+
+      - name: Install Idris 2 dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme libgmp-dev
+
+      # Cache the Idris2 compiler + bundled packages (base/contrib/network)
+      # only. This job never runs `idris2 --install proven.ipkg` and never
+      # caches `build/`, so every run type-checks the CURRENT source of each
+      # Proofs.idr — a stale cache cannot mask a source-level break.
+      - name: Cache Idris 2
+        id: cache-idris2
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: |
+            ~/.idris2
+            ~/idris2-${{ matrix.idris2-version }}
+          key: idris2-${{ matrix.idris2-version }}-${{ runner.os }}
+
+      - name: Install Idris 2
+        if: steps.cache-idris2.outputs.cache-hit != 'true'
+        run: |
+          git clone --depth 1 --branch v${{ matrix.idris2-version }} https://github.com/idris-lang/Idris2.git ~/idris2-${{ matrix.idris2-version }}
+          cd ~/idris2-${{ matrix.idris2-version }}
+          make bootstrap SCHEME=chezscheme
+          make install
+
+      - name: Add Idris 2 to PATH
+        run: echo "$HOME/.idris2/bin" >> $GITHUB_PATH
+
+      - name: Type check every Proofs.idr
+        run: |
+          set -uo pipefail
+          rm -rf build
+          fail=0
+          checked=0
+          while IFS= read -r f; do
+            checked=$((checked + 1))
+            echo "::group::idris2 --check $f"
+            if idris2 -p contrib -p network --check "$f"; then
+              echo "PASS  $f"
+            else
+              echo "::error file=$f::idris2 --check failed"
+              fail=1
+            fi
+            echo "::endgroup::"
+          done < <(find src -name 'Proofs.idr' | sort)
+          echo "Checked $checked Proofs.idr module(s); fail=$fail"
+          exit "$fail"
+
   docs:
     runs-on: ubuntu-latest
     needs: build