ci.yml

name: CI

on:
  push:
    branches: [master]
  pull_request:
    branches: [master]
  workflow_dispatch:

permissions:
  contents: read

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  build:
    name: Build and audit
    runs-on: ubuntu-latest
    timeout-minutes: 60

    steps:
      - name: Check out repository
        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2

      - name: Build Lean project
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
        with:
          auto-config: false
          build: true
          build-args: GQ2 Challenge Solution
          use-mathlib-cache: true

      - name: Check axiom and placeholder hygiene
        run: bash scripts/check_axioms.sh

      - name: Check transitive axiom ledger
        run: lake env lean GQ2/AxiomLedger.lean