docs(citation): align CITATIONS.adoc author form with CITATION.cff (#… #57
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
| # This workflow is managed by gh actions-lock. | |
| # SPDX-License-Identifier: MPL-2.0 | |
| # This workflow is managed by gh actions-lock. | |
| # This workflow is managed by gh actions-lock. | |
| # 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 Mathlib-free Lean core (CNO, OND, CNOCategory, CNOBridge, FilesystemCNO, | |
| # LambdaCNO) is built here too, with the toolchain pinned in | |
| # proofs/lean4/lean-toolchain, and proofs/lean4/AxiomAudit.lean pins the | |
| # signature of every axiom and the axiom list of every theorem (issue #125). | |
| # | |
| # The heavy provers (Lean + multi-GB Mathlib for QuantumCNO/StatMech, 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] | |
| pull_request: | |
| paths: | |
| - 'proofs/**' | |
| - 'absolute-zero-abi.ipkg' | |
| - '.github/workflows/proofs.yml' | |
| - 'Justfile' | |
| - '*.agda-lib' | |
| - 'lakefile*' | |
| 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@v7.0.1 | |
| - 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)" | |
| - name: Print Assumptions gate (17 named theorems closed) + control | |
| working-directory: proofs/coq | |
| run: | | |
| bash check-assumptions.sh | |
| bash check-assumptions.sh --control | |
| - name: Axiom tag grammar gate + control (issue #171) | |
| working-directory: proofs/coq | |
| run: | | |
| bash check-axiom-tags.sh | |
| bash check-axiom-tags.sh --control | |
| - name: Axiom dependency census (issue #171) | |
| working-directory: proofs/coq | |
| run: | | |
| bash census-assumptions.sh | |
| agda: | |
| name: Agda — CNO + OND | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 25 | |
| steps: | |
| - uses: actions/checkout@v7.0.1 | |
| - name: Install Agda (binary only) | |
| # Install just the `agda` binary (2.6.3 on 24.04). NOT `agda-stdlib` — | |
| # the Ubuntu stdlib package ships no usable library manifest; we fetch a | |
| # version-matched stdlib from git instead (validated locally). | |
| run: sudo apt-get update && sudo apt-get install -y agda | |
| - name: Fetch + register agda-stdlib v1.7.3 (matches Agda 2.6.3) | |
| run: | | |
| git clone -q --depth 1 --branch v1.7.3 \ | |
| https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib" | |
| # The upstream manifest is named `standard-library-1.7.3`; the repo's | |
| # absolute-zero.agda-lib depends on `standard-library`, so align it. | |
| sed -i 's/^name: .*/name: standard-library/' \ | |
| "$HOME/agda-stdlib/standard-library.agda-lib" | |
| mkdir -p "$HOME/.agda" | |
| echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries" | |
| echo "standard-library" > "$HOME/.agda/defaults" | |
| - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K) | |
| working-directory: proofs/agda | |
| run: | | |
| agda --version | |
| agda --safe --without-K CNO.agda | |
| agda --safe --without-K OND.agda | |
| agda --safe --without-K EchoBridgeScaffold.agda | |
| agda --safe --without-K EchoBridgeCNO.agda | |
| echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check" | |
| z3: | |
| name: Z3 — CNO + OND bounded checks | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@v7.0.1 | |
| - name: Install Z3 | |
| run: sudo apt-get update && sudo apt-get install -y z3 | |
| - name: Run Z3 checks | |
| run: | | |
| z3 --version | |
| bash proofs/z3/verify.sh | |
| echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation" | |
| - name: Gate self-test (stub provers + z3 mutants must turn the gate red) | |
| run: bash proofs/tests/gate-selftest.sh | |
| lean: | |
| name: Lean — core CNO (6 modules + axiom audit) | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 20 | |
| steps: | |
| - uses: actions/checkout@v7.0.1 | |
| - name: Install elan v4.2.4 (sha256-verified) and the pinned toolchain | |
| # elan is fetched as a release tarball and checksum-verified rather than | |
| # via a third-party action, so the repo's Actions allow-list is not in | |
| # play. The toolchain itself comes from proofs/lean4/lean-toolchain. | |
| run: | | |
| curl -fsSL --retry 3 -o elan.tgz \ | |
| https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz | |
| echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63 elan.tgz" | sha256sum -c - | |
| tar -xzf elan.tgz | |
| ./elan-init -y --no-modify-path --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Build the six Mathlib-free modules and run the axiom audit | |
| run: bash proofs/lean4/check-core.sh |