fix(ci): close the governance gate — SPDX, permissions, SHA pins, reusable bump #92
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: MPL-2.0 | |
| # CI workflow for ECHIDNA Agda meta-checker | |
| # Type-checks all formal proofs verifying trust pipeline correctness | |
| name: Agda Meta-Checker | |
| on: | |
| push: | |
| 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] | |
| workflow_dispatch: | |
| # Cause-B mitigation (#77): cancel superseded runs so stacked pushes | |
| # to the same ref don't pile up identical jobs in the queue. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| pull-requests: read # change-detector reads the PR's file list (gh api pulls/.../files) | |
| jobs: | |
| verify-proofs: | |
| name: Type-check Agda proofs | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 | |
| # 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@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 | |
| with: | |
| path: | | |
| ~/.cabal | |
| ~/.agda | |
| 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 | |
| # carries the agda symlink, so a plain install aborts with | |
| # "Path '.../bin/agda' already exists" on a warm cache. | |
| 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 | |
| wget -q https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz | |
| tar xzf v2.1.tar.gz | |
| echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" > ~/.agda/libraries | |
| 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 | |
| agda src/Echidna/MetaChecker.agda | |
| echo "✓ All 30+ properties machine-verified" |