Agda Meta-Checker #114
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/**' | |
| pull_request: | |
| branches: [main] | |
| paths: | |
| - 'meta-checker/**' | |
| 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 | |
| jobs: | |
| verify-proofs: | |
| name: Type-check Agda proofs | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: Setup Haskell | |
| uses: haskell-actions/setup@cd0d9bdd65b20557f41bea4dbe43d0b5fbbfe553 # v2 | |
| with: | |
| ghc-version: '9.6' | |
| cabal-version: '3.10' | |
| - name: Cache Agda | |
| uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5 | |
| with: | |
| path: | | |
| ~/.cabal | |
| ~/.agda | |
| key: agda-${{ runner.os }}-${{ hashFiles('meta-checker/**/*.agda') }} | |
| - name: Install Agda | |
| run: | | |
| cabal update | |
| cabal install Agda-2.7.0.1 | |
| - name: Install Agda standard library | |
| 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 | |
| run: | | |
| cd meta-checker | |
| echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries | |
| agda src/Echidna/MetaChecker.agda | |
| echo "✓ All 30+ properties machine-verified" |