From f98710f41b2c9124519f5cdc3c4d023a36e75f28 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 6 Oct 2026 10:55:49 +0100 Subject: [PATCH] ci: remove the agda-cicd catalogue gate that could never start .github/workflows/agda-cicd.yml (added in #7) called hyperpolymath/standards/.github/workflows/echidna-verify.yml@main as a reusable workflow, but that file declares no workflow_call trigger: it is standards' own lol/proofs + avow corpus gate. GitHub therefore refused the call at plan time and every run recorded failure with zero jobs (run 37231048694 on main; the same on arena 01c5afd). It never passed on any head. The proofs job in ci.yml (proofs/check.sh under Debian 13's Agda 2.6.4.3 and agda-stdlib 2.1) is the repo's proof gate and is green at aa8f6e6. Nothing in the proof corpus changes here. The ISSUE.md checklist line that recorded the gate is struck through with the reason rather than deleted. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01AjVQUkziVYywrLNsbPordh --- .github/workflows/agda-cicd.yml | 43 --------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 .github/workflows/agda-cicd.yml diff --git a/.github/workflows/agda-cicd.yml b/.github/workflows/agda-cicd.yml deleted file mode 100644 index 6455b55..0000000 --- a/.github/workflows/agda-cicd.yml +++ /dev/null @@ -1,43 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# Agda CICD gate pulled from the estate CICD-WORKFLOW-CATALOG.md -# (catalog entry: echidna-verify.yml — ECHIDNA trust-pipeline proof verification, -# Agda/Idris2; reusable = Yes; source = hyperpolymath/standards). -# See .github/workflows/ci.yml `proofs` job for the repo-specific proof gate -# (`proofs/check.sh`, `proofs/agda/`); this gate ensures the catalogue entry -# is present and checked as the repo extends. - -name: Agda CICD Gate (catalogue) - -on: - push: - branches: [main, arena/*] - paths: - - 'proofs/**' - - '.github/workflows/agda-cicd.yml' - pull_request: - paths: - - 'proofs/**' - - '.github/workflows/agda-cicd.yml' - workflow_dispatch: - -permissions: - contents: read - -concurrency: - group: agda-cicd-${{ github.ref }} - cancel-in-progress: true - -jobs: - catalogue-gate: - name: Agda — catalogue gate (echidna-verify) - runs-on: ubuntu-24.04 - timeout-minutes: 20 - # Reusable workflow from the estate standards repo (catalog entry: - # echidna-verify.yml — ECHIDNA trust-pipeline proof verification, Agda/Idris2; - # reusable = Yes). It checks `lol/proofs/` and `2-protocols/avow/`; the repo's - # own proof corpus (`proofs/agda/`) is covered by `.github/workflows/ci.yml` - # (`proofs/check.sh`). This gate ensures the catalogue entry is present - # and checked as the repo extends. - uses: hyperpolymath/standards/.github/workflows/echidna-verify.yml@main