agda.yml

# SPDX-License-Identifier: PMPL-1.0-or-later
# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)

name: Agda

on:
  push:
    branches:
      - "**"
  pull_request:

permissions: read-all

jobs:
  check:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2

      - name: Install Agda and standard library
        run: |
          sudo apt-get update
          sudo apt-get install -y agda git

      - name: Fetch Agda standard library (v2.3)
        id: stdlib
        run: |
          STDLIB_DIR="$HOME/agda-stdlib"
          git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git "$STDLIB_DIR"
          echo "stdlib_dir=$STDLIB_DIR" >> "$GITHUB_OUTPUT"

      - name: Fetch absolute-zero library
        id: absz
        run: |
          ABSZ_DIR="$HOME/absolute-zero"
          git clone --depth 1 https://github.com/hyperpolymath/absolute-zero.git "$ABSZ_DIR"
          echo "absz_commit=$(git -C "$ABSZ_DIR" rev-parse HEAD)" >> "$GITHUB_OUTPUT"
          echo "absz_dir=$ABSZ_DIR" >> "$GITHUB_OUTPUT"

      - name: Register libraries for Agda
        run: |
          mkdir -p "$HOME/.agda"

          STDLIB_LIB="$RUNNER_TEMP/standard-library.agda-lib"
          cat > "$STDLIB_LIB" <<EOF
          name: standard-library
          include: ${{ steps.stdlib.outputs.stdlib_dir }}/src
          EOF

          ABSZ_LIB="$RUNNER_TEMP/absolute-zero.agda-lib"
          cat > "$ABSZ_LIB" <<EOF
          name: absolute-zero
          include: ${{ steps.absz.outputs.absz_dir }}/proofs/agda
          EOF

          printf '%s\n%s\n' "$STDLIB_LIB" "$ABSZ_LIB" > "$HOME/.agda/libraries"
          printf '%s\n' "standard-library" > "$HOME/.agda/defaults"

      # Cache Agda interface (.agdai) files. A fresh runner otherwise
      # recompiles the entire stdlib subset + the whole proof development
      # from scratch every run (the multi-minute cold pass). Agda validates
      # each .agdai against its source, so a stale cache is always safe —
      # it just means more modules recompile. The key rotates on any proof
      # source change or absolute-zero bump; restore-keys give a warm
      # partial cache even when it does.
      - name: Cache Agda interface files
        uses: actions/cache@v4
        with:
          path: |
            ~/agda-stdlib/**/*.agdai
            ~/absolute-zero/**/*.agdai
            proofs/agda/**/*.agdai
          key: agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-absz${{ steps.absz.outputs.absz_commit }}-${{ hashFiles('proofs/agda/**/*.agda') }}
          restore-keys: |
            agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-absz${{ steps.absz.outputs.absz_commit }}-
            agdai-${{ runner.os }}-agda2.6.3-stdlib2.3-

      - name: Typecheck full suite
        run: agda -i proofs/agda proofs/agda/All.agda

      - name: Smoke-check headline theorems
        run: agda -i proofs/agda proofs/agda/Smoke.agda

      - name: Typecheck characteristic lane (Gate #2 audit modules)
        run: agda -i proofs/agda proofs/agda/characteristic/All.agda

      - name: Typecheck examples lane (Gate #3 canonical examples)
        run: agda -i proofs/agda proofs/agda/examples/All.agda