coq-proof-gate.yml

# SPDX-License-Identifier: MPL-2.0
# This workflow is managed by gh actions-lock.
# This workflow is managed by gh actions-lock.
# Coq/Rocq proof gate for the `formal/` mechanised-metatheory track (issue #513).
#
# This gate is deliberately FAIL-CLOSED. It does NOT probe for the prover and
# skip when absent — the container guarantees `coqc` exists, so a missing
# prover is an infrastructure failure, not a silent pass.
#
# `formal/justfile` remains the single source of truth for the proof list and
# its dependency order; this workflow parses that list rather than duplicating
# it, and fails if any `formal/*.v` on disk is not named there.
name: Coq Proof Gate
on:
  pull_request:
    paths:
      - 'formal/**'
      - '.github/workflows/coq-proof-gate.yml'
  push:
    branches: [main]
    paths:
      - 'formal/**'
      - '.github/workflows/coq-proof-gate.yml'
  workflow_dispatch:
permissions: read-all
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true
jobs:
  coq-proofs:
    runs-on: ubuntu-latest
    timeout-minutes: 30
    # The image ships bash 5.2, but GitHub fell back to `sh -e {0}` (dash) on
    # the first run, which rejects `set -o pipefail` and the bash-only string
    # operations below. Declare the shell explicitly rather than depending on
    # the runner's detection.
    defaults:
      run:
        shell: bash
    container:
      # coqorg/coq:8.20 — pinned by digest. `formal/README.adoc` documents 8.18;
      # the corpus was verified to check clean on 8.20.1 (deprecation warnings
      # for `app_length` only, no errors).
      image: coqorg/coq@sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674
      options: --user root
    steps:
      - uses: actions/checkout@v7.0.1

      # The coqorg images install Coq into an opam switch owned by the `coq`
      # user and put it on PATH via an ENTRYPOINT wrapper. GitHub Actions
      # overrides the entrypoint for job containers, so that wrapper never
      # runs and `coqc` is not on PATH — the switch has to be added by hand.
      # Globbed rather than hard-coded so an image bump does not silently
      # break the gate; fails loudly if the switch cannot be located.
      - name: Put the image's opam switch on PATH
        run: |
          set -euo pipefail
          sw="$(ls -d /home/coq/.opam/*/bin 2>/dev/null | head -1 || true)"
          if [ -z "$sw" ] || [ ! -x "$sw/coqc" ]; then
            echo "::error::could not locate coqc in the image's opam switch"
            exit 1
          fi
          echo "$sw" >> "$GITHUB_PATH"
          echo "added $sw to PATH"

      # The coqorg images install Coq into an opam switch owned by the `coq`
      # user and put it on PATH via an ENTRYPOINT wrapper. GitHub Actions
      # overrides the entrypoint for job containers, so that wrapper never
      # runs and `coqc` is not on PATH — the switch has to be added by hand.
      # Globbed rather than hard-coded so an image bump does not silently
      # break the gate; fails loudly if the switch cannot be located.
      - name: Put the image's opam switch on PATH
        run: |
          set -euo pipefail
          sw="$(ls -d /home/coq/.opam/*/bin 2>/dev/null | head -1 || true)"
          if [ -z "$sw" ] || [ ! -x "$sw/coqc" ]; then
            echo "::error::could not locate coqc in the image's opam switch"
            exit 1
          fi
          echo "$sw" >> "$GITHUB_PATH"
          echo "added $sw to PATH"

      - name: Record prover version
        run: coqc --version

      - name: Extract the ordered proof list from formal/justfile
        id: list
        run: |
          set -euo pipefail
          cd formal
          list="$(sed -n '/for f in /,/; do/p' justfile \
                  | tr '\n' ' ' \
                  | sed 's/.*for f in //; s/; do.*//; s/\\//g' \
                  | tr -s ' ')"
          if [ -z "${list// /}" ]; then
            echo "::error::could not parse the proof list out of formal/justfile"
            exit 1
          fi
          echo "count=$(printf '%s' "$list" | wc -w)"
          echo "list=$list" >> "$GITHUB_OUTPUT"

      - name: Guard — every formal/*.v must be wired into the gate
        env:
          LIST: ${{ steps.list.outputs.list }}
        run: |
          set -euo pipefail
          cd formal
          missing=0
          for f in *.v; do
            b="${f%.v}"
            case " $LIST " in
              *" $b "*) ;;
              *) echo "::error file=formal/$f::proof file is not listed in formal/justfile — it would never be checked"; missing=1 ;;
            esac
          done
          [ "$missing" -eq 0 ] || exit 1
          echo "all on-disk proofs are wired into the gate"

      - name: Type-check every proof and reject any axiom / Admitted
        env:
          LIST: ${{ steps.list.outputs.list }}
        run: |
          set -euo pipefail
          cd formal
          all=""
          for f in $LIST; do
            echo "== coqc $f.v =="
            o="$(coqc -Q . ASFormal "$f.v")"
            printf '%s\n' "$o"
            all+="$o"$'\n'
          done
          # `Print Assumptions` emits "Axioms:" when a theorem depends on an
          # axiom or an `Admitted` proof; "Closed under the global context"
          # is the clean result.
          if printf '%s' "$all" | grep -q "Axioms:"; then
            echo "::error::a proof depends on an axiom / Admitted"
            exit 1
          fi
          echo "OK: all proofs mechanised; no axioms."