proofs.yml

# 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) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# Proofs Gate — type-check every Idris2 proof + enforce the trusted base.
#
# Closes the gap that let cartridge ABIs rot into non-compiling states:
# abi-drift.yml only runs iseriser's *structural* manifest check, and nothing
# ever ran `idris2 --typecheck` on cartridges/**/abi in CI (the Justfile's old
# `typecheck` recipe covered only 5 of ~50 cartridge ABIs and was never wired
# into a workflow). This gate type-checks the core ABI package AND every
# cartridge ABI under the pinned toolchain (.mise.toml → idris2), and
# runs the trusted-base audit so no new believe_me / axiom slips in.
name: Proofs Gate

# Runs on every PR and push to main, with no path filter and no `changes`
# gate. A path-skipped proof job reports success without checking anything,
# which is how a duplicate `allTake` in SafetyLemmas.idr sat in main behind a
# green gate (#343, DEBT P-1). This workflow is not a required check, so always
# running it blocks nothing.
on:
  push:
    branches: [main]
  pull_request:
    branches: [main]
  workflow_dispatch:
  # Weekly re-verification of main, so toolchain or runner drift is caught
  # even when nothing is merged.
  schedule:
    - cron: '17 6 * * 1'   # Mondays 06:17 UTC

permissions:
  actions: read
  contents: read

concurrency:
  group: proofs-${{ github.ref }}
  cancel-in-progress: ${{ github.event_name == 'pull_request' }}

jobs:
  # Cheap, dependency-free gate: scan for unsound constructs + axiom-count drift.
  trusted-base:
    name: Trusted-base audit (no new axioms)
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - uses: actions/checkout@v6.0.2
      - name: Enforce trusted base
        run: bash scripts/check-trusted-base.sh

  # Full type-check of the core ABI + every cartridge ABI under the pinned Idris2.
  typecheck:
    name: Idris2 type-check (core + all cartridge ABIs)
    runs-on: ubuntu-latest
    timeout-minutes: 45
    steps:
      - uses: actions/checkout@v6.0.2

      # The pin lives in .mise.toml (.tool-versions was converted, 4d1fe0c9).
      # Fail here on an empty or malformed value rather than asking asdf to
      # install version "".
      - name: Read pinned Idris2 version
        id: ver
        run: |
          set -euo pipefail
          v=$(awk -F'"' '/^idris2[[:space:]]*=/{print $2}' .mise.toml)
          if ! printf '%s' "$v" | grep -qE '^[0-9]+\.[0-9]+\.[0-9]+$'; then
            echo "::error file=.mise.toml::no idris2 = \"X.Y.Z\" pin found (got '$v')"
            exit 1
          fi
          echo "idris2=$v" >> "$GITHUB_OUTPUT"

      - name: Install build deps (Chez Scheme + GMP)
        run: sudo apt-get update && sudo apt-get install -y chezscheme libgmp-dev build-essential

      - name: Cache asdf + Idris2 toolchain
        uses: actions/cache@v4.2.2
        with:
          path: ~/.asdf
          key: idris2-asdf-${{ runner.os }}-${{ steps.ver.outputs.idris2 }}

      - name: Install asdf + Idris2 ${{ steps.ver.outputs.idris2 }}
        env:
          # Ubuntu's chezscheme package installs the interpreter as `scheme`;
          # Idris2's bootstrap Makefile reads $SCHEME (defaults to `chez`).
          SCHEME: scheme
        run: |
          set -euo pipefail
          if [ ! -f "$HOME/.asdf/asdf.sh" ]; then
            git clone --depth 1 --branch v0.14.0 https://github.com/asdf-vm/asdf.git "$HOME/.asdf"
          fi
          . "$HOME/.asdf/asdf.sh"
          asdf plugin add idris2 || true
          asdf install idris2 "${{ steps.ver.outputs.idris2 }}"
          asdf global  idris2 "${{ steps.ver.outputs.idris2 }}"

      - name: Put Idris2 on PATH
        run: echo "$HOME/.asdf/shims" >> "$GITHUB_PATH"

      - name: Idris2 version
        run: idris2 --version

      - name: Type-check all proofs (core + cartridges)
        run: bash scripts/typecheck-proofs.sh