From 2d7231ebaf7b58c3af3c26c62e3067cc2fb0619b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 25 Jun 2026 09:54:35 +0100 Subject: [PATCH] ci(proofs): add weekly schedule so the proof gate re-checks main MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Proofs Gate is path-filtered: the `changes` job skips the heavy type-check unless a PR/push touches src/abi/**, cartridges/**/abi, etc. A break already in main (merged before this gate existed, or via a path the filter ignores) is therefore never re-detected — every off-path PR's typecheck job is skipped and reports success to the required check. Add a weekly `schedule` trigger. On a schedule event the detect step leaves run=true (its default), so the full core + every-cartridge Idris2 type-check runs unconditionally against main and catches proof drift. Motivated by a duplicate `allTake` definition that sat in src/abi/Boj/SafetyLemmas.idr on main with a green gate (fixed separately). Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/proofs.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 3f590145..c517ec01 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -22,6 +22,17 @@ on: pull_request: branches: [main] workflow_dispatch: + # Weekly baseline re-verification of main. The `changes` path-filter below + # skips the heavy type-check on PRs/pushes that don't touch src/abi/** (so an + # off-path PR isn't blocked and doesn't pay for a 45-min Idris2 build). The + # side effect is that a proof break ALREADY living in main — merged before + # this gate existed, or via a path the filter ignores — is otherwise never + # re-detected. On a `schedule` event the detect step leaves run=true (its + # default), so the full core + every-cartridge type-check runs unconditionally + # and catches such drift. (This is exactly how a duplicate `allTake` in + # SafetyLemmas.idr sat in main with a green gate — see PR fixing it.) + schedule: + - cron: '17 6 * * 1' # Mondays 06:17 UTC permissions: contents: read