name: Lean CI

on:
  push:
  pull_request:
  workflow_dispatch:

permissions: {}

concurrency:
  group: lean-ci-${{ github.head_ref || github.ref }}
  cancel-in-progress: true

env:
  ELAN_HOME: /home/runner/.elan

jobs:
  # CONTRACT: org ruleset requires this exact check name 'build'
  build:
    runs-on: ubuntu-latest
    timeout-minutes: 120
    permissions:
      contents: read
    steps:
      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6

      - name: Install elan and toolchain
        run: |
          curl -sSf https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh | sh -s -- -y --default-toolchain none
          echo "${ELAN_HOME}/bin" >> "${GITHUB_PATH}"
          export PATH="${ELAN_HOME}/bin:${PATH}"
          elan --version
          elan show

      - name: Cache Lake build artifacts
        uses: actions/cache@cdf6c1fa76f9f475f3d7449005a359c84ca0f306 # v5.0.3
        with:
          path: .lake
          key: lake-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json') }}
          restore-keys: lake-

      - name: Get Mathlib cache
        run: lake exe cache get || true

      - name: Build (fail on warnings and sorry)
        run: make build

      - name: Verify theorem dashboard
        run: make verify

      - name: Check documented theorem names
        run: make check-doc-names

      - name: Audit for proof placeholders
        run: make audit

      - name: Lint (Mathlib environment linters)
        run: lake lint

      - name: Check axiom dashboard for sorry contamination
        run: |
          echo "Checking axiom dependencies..."
          touch OrdvecFormalization/Verify.lean
          lake env lean OrdvecFormalization/Verify.lean 2>&1 | tee verify_output.txt
          if grep -q "sorryAx" verify_output.txt; then
            echo "FATAL: sorryAx found in verified theorems!"
            exit 1
          fi
          echo "No sorry contamination detected."