ci: fix Idris2/Agda required-check deadlock (pass-through shim) (#256)

ci: fix required-check deadlock on Idris2/Agda workflows (pass-through
shim)

"Type-check Idris2 ABI definitions" (idris2-abi-ci.yml) and "Type-check
Agda
proofs" (agda-meta-checker.yml) are REQUIRED status checks but are
path-filtered.
A path-filtered REQUIRED check deadlocks every PR that does not touch
its paths:
branch protection waits for a run that never starts, so echidna's main
is
unmergeable via normal PR flow.

Fix (pass-through shim): drop the pull_request paths-filter so each job
ALWAYS
runs and the required check always reports. A "Detect relevant changes"
step
reads the PR's changed files via the GitHub API and gates the heavy
steps -- the
real type-check runs only when the relevant sources change, otherwise
the job
passes through in seconds. push triggers stay scoped to main
(paths-filtered),
so post-merge behaviour is unchanged and feature-branch pushes don't
double-fire
alongside the pull_request run. Job names are preserved so the existing
required-status contexts still match. agda gains pull-requests:read for
the
detector.

(The SHA-pin half of the original work merged separately as cb5e41a;
this lands
only the deadlock fix, which was stranded on the merged branch.)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/agda-meta-checker.yml

@@ -9,10 +9,11 @@ on:
     branches: [main]
     paths:
       - 'meta-checker/**'
+  # No paths-filter on pull_request: this is a REQUIRED status check, so it must
+  # report on every PR (a path-filtered required check deadlocks PRs that don't
+  # touch its paths). The "Detect relevant changes" step path-gates internally.
   pull_request:
     branches: [main]
-    paths:
-      - 'meta-checker/**'
   workflow_dispatch:
 
 # Cause-B mitigation (#77): cancel superseded runs so stacked pushes
@@ -23,6 +24,7 @@ concurrency:
 
 permissions:
   contents: read
+  pull-requests: read   # change-detector reads the PR's file list (gh api pulls/.../files)
 
 jobs:
   verify-proofs:
@@ -33,13 +35,39 @@ jobs:
       - name: Checkout
         uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10  # v6.0.3
 
+      # Required-check shim: only the meta-checker/ tree needs the real proof
+      # check. Non-PR events (push, workflow_dispatch) always run it.
+      - name: Detect relevant changes
+        id: detect
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          PATTERN='^meta-checker/'
+          if [ "${{ github.event_name }}" = "pull_request" ]; then
+            FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
+                      --paginate --jq '.[].filename')
+            if printf '%s\n' "$FILES" | grep -qE "$PATTERN"; then
+              echo "relevant=true" >> "$GITHUB_OUTPUT"
+              echo "meta-checker/ sources changed — running full Agda type-check."
+            else
+              echo "relevant=false" >> "$GITHUB_OUTPUT"
+              echo "No meta-checker changes — pass-through (required-check shim)."
+            fi
+          else
+            echo "relevant=true" >> "$GITHUB_OUTPUT"
+            echo "Non-PR event — running full Agda type-check."
+          fi
+
       - name: Setup Haskell
+        if: steps.detect.outputs.relevant == 'true'
         uses: haskell-actions/setup@cd0d9bdd65b20557f41bea4dbe43d0b5fbbfe553 # v2
         with:
           ghc-version: '9.6'
           cabal-version: '3.10'
 
       - name: Cache Agda
+        if: steps.detect.outputs.relevant == 'true'
         uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
         with:
           path: |
@@ -48,6 +76,7 @@ jobs:
           key: agda-${{ runner.os }}-${{ hashFiles('meta-checker/**/*.agda') }}
 
       - name: Install Agda
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           cabal update
           # --overwrite-policy=always: the cached ~/.cabal restore already
@@ -56,6 +85,7 @@ jobs:
           cabal install Agda-2.7.0.1 --overwrite-policy=always
 
       - name: Install Agda standard library
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           mkdir -p ~/.agda
           cd /tmp
@@ -65,6 +95,7 @@ jobs:
           echo "standard-library" > ~/.agda/defaults
 
       - name: Type-check meta-checker
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           cd meta-checker
           echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries

.github/workflows/idris2-abi-ci.yml

@@ -3,15 +3,17 @@ name: Idris2 ABI Type-Check
 
 on:
   push:
+    branches: [main]   # only post-merge; feature-branch PRs are gated by the pull_request run below
     paths:
       - 'src/abi/**'
       - 'src/idris/**'
       - '.github/workflows/idris2-abi-ci.yml'
+  # No paths-filter on pull_request: this job is a REQUIRED status check, so it
+  # must report on every PR (a path-filtered required check deadlocks PRs that
+  # don't touch its paths — they wait forever for a run that never happens). The
+  # "Detect relevant changes" step below does the path-gating internally instead,
+  # so the check always reports while heavy work runs only when sources change.
   pull_request:
-    paths:
-      - 'src/abi/**'
-      - 'src/idris/**'
-      - '.github/workflows/idris2-abi-ci.yml'
 
 # Cause-B mitigation (#77): cancel superseded runs so stacked pushes
 # to the same ref don't pile up identical jobs in the queue.
@@ -29,7 +31,33 @@ jobs:
     steps:
       - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
 
+      # Required-check shim: decide whether ABI/proof sources actually changed.
+      # The workflow file itself is intentionally NOT in the pattern, so CI-only
+      # edits pass through. Non-PR events (push) always run the full check.
+      - name: Detect relevant changes
+        id: detect
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          PATTERN='^(src/abi/|src/idris/)'
+          if [ "${{ github.event_name }}" = "pull_request" ]; then
+            FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
+                      --paginate --jq '.[].filename')
+            if printf '%s\n' "$FILES" | grep -qE "$PATTERN"; then
+              echo "relevant=true" >> "$GITHUB_OUTPUT"
+              echo "Idris2 ABI/proof sources changed — running full type-check."
+            else
+              echo "relevant=false" >> "$GITHUB_OUTPUT"
+              echo "No Idris2 source changes — pass-through (required-check shim)."
+            fi
+          else
+            echo "relevant=true" >> "$GITHUB_OUTPUT"
+            echo "Non-PR event — running full type-check."
+          fi
+
       - name: Install Idris2
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           # Idris2 v0.8.0 has no pre-built Linux release binary — the
           # release-assets array on https://api.github.com/repos/idris-lang/Idris2/releases/tags/v0.8.0
@@ -54,13 +82,15 @@ jobs:
           idris2 --version
 
       - name: Type-check all ABI modules via ipkg
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           cd src/abi
           echo "=== Type-checking ECHIDNA ABI package (16 modules) ==="
           idris2 --build echidnaabi.ipkg
           echo "✓ All ABI modules type-check successfully"
 
       - name: Type-check Idris2 proof validator (src/idris)
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           # Mirrors `just proofs-idris`. --typecheck (not --build) so no codegen
           # backend is required; the declared executable's `main` is exercised
@@ -71,6 +101,7 @@ jobs:
           echo "✓ Validator modules type-check successfully"
 
       - name: Verify no dangerous patterns
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           echo "=== Scanning for dangerous patterns in ABI code ==="
           FOUND=0
@@ -88,6 +119,7 @@ jobs:
           fi
 
       - name: Count modules and report
+        if: steps.detect.outputs.relevant == 'true'
         run: |
           echo "=== ABI Module Summary ==="
           IDR_COUNT=$(find src/abi -name "*.idr" | wc -l)