fix(ci): Agda job — use -i stdlib sources (Ubuntu ships no .agda-lib)… #8
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: Type-check CNO + OND (--safe --without-K) | |
| working-directory: proofs/agda | |
| run: | | |
| agda --version | |
| # The Ubuntu agda-stdlib package installs the SOURCES (no .agda-lib | |
| # manifest), so add its root directly to Agda's include path via -i. | |
| # Locate the root as the parent of Data/Nat.agda (version-dir robust). | |
| NAT="$(dpkg -L agda-stdlib | grep -m1 '/Data/Nat\.agda$')" | |
| STDLIB="${NAT%/Data/Nat.agda}" | |
| echo "stdlib include path: $STDLIB" | |
| [ -d "$STDLIB" ] || { echo "::error::agda-stdlib source dir not found"; dpkg -L agda-stdlib | tail -60; exit 1; } | |
| agda --safe --without-K -i "$STDLIB" CNO.agda | |
| agda --safe --without-K -i "$STDLIB" 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" |