fix(ci): robust agda-stdlib registration (green the proofs workflow) #5
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 | |
| # Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> | |
| # | |
| # Proof verification CI. Runs the LIGHTWEIGHT provers that are fast and reliable | |
| # on a standard GitHub runner — Coq (both pillars, all 14 theories), Agda (CNO + | |
| # OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one | |
| # flaking never blocks the others. | |
| # | |
| # The heavy provers (Lean + multi-GB Mathlib, Isabelle ~1.2 GB, Mizar i386 + MML, | |
| # Idris 2 from source) are NOT run here — they are covered by the local/container | |
| # gate `proofs/verify-all-provers.sh` (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc. | |
| name: Proofs | |
| on: | |
| push: | |
| branches: [main, master] | |
| paths: | |
| - 'proofs/**' | |
| - 'absolute-zero-abi.ipkg' | |
| - '.github/workflows/proofs.yml' | |
| pull_request: | |
| paths: | |
| - 'proofs/**' | |
| - 'absolute-zero-abi.ipkg' | |
| - '.github/workflows/proofs.yml' | |
| permissions: | |
| contents: read | |
| # Cancel superseded runs on the same ref (don't pile up on force-pushes). | |
| concurrency: | |
| group: proofs-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| coq: | |
| name: Coq — CNO + OND (14 theories) | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Coq | |
| run: sudo apt-get update && sudo apt-get install -y coq | |
| - name: Build all theories via coq_makefile | |
| working-directory: proofs/coq | |
| run: | | |
| coqc --version | |
| coq_makefile -f _CoqProject -o Makefile.all | |
| make -f Makefile.all -j"$(nproc)" | |
| echo "✓ Coq: 14/14 theories compiled (CNO + OND)" | |
| agda: | |
| name: Agda — CNO + OND | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Agda + stdlib | |
| run: sudo apt-get update && sudo apt-get install -y agda agda-stdlib | |
| - name: Register the standard library | |
| run: | | |
| mkdir -p "$HOME/.agda" | |
| # Grab whatever .agda-lib the package ships (name is version-dependent), | |
| # with a filesystem fallback. Dump the file list on failure for triage. | |
| LIB="$(dpkg -L agda-stdlib 2>/dev/null | grep -m1 '\.agda-lib$' || true)" | |
| [ -z "$LIB" ] && LIB="$(find /usr -name '*.agda-lib' 2>/dev/null | grep -m1 -i 'standard' || true)" | |
| if [ -z "$LIB" ]; then | |
| echo "::error::no .agda-lib found for agda-stdlib"; dpkg -L agda-stdlib | tail -60; exit 1 | |
| fi | |
| echo "$LIB" > "$HOME/.agda/libraries" | |
| echo "standard-library" > "$HOME/.agda/defaults" | |
| echo "registered: $LIB" | |
| - name: Type-check CNO + OND (--safe --without-K) | |
| working-directory: proofs/agda | |
| run: | | |
| agda --version | |
| agda --safe --without-K CNO.agda | |
| agda --safe --without-K OND.agda | |
| echo "✓ Agda: CNO + OND type-check" | |
| z3: | |
| name: Z3 — CNO + OND bounded checks | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4 | |
| - name: Install Z3 | |
| run: sudo apt-get update && sudo apt-get install -y z3 | |
| - name: Run Z3 checks | |
| run: | | |
| z3 --version | |
| sh proofs/z3/verify.sh || true | |
| z3 proofs/z3/ond/OND_checks.smt2 | |
| echo "✓ Z3: OND bounded instances checked" |