name: Lean

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

permissions:
  contents: read

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

jobs:
  build-depth1:
    if: github.event.repository.private == false
    uses: ./.github/workflows/build-depth.yml
    with:
      depth: 1

  build-depth2:
    if: github.event.repository.private == false
    needs: build-depth1
    uses: ./.github/workflows/build-depth.yml
    with:
      depth: 2

  verify:
    if: github.event.repository.private == false
    needs: build-depth2
    runs-on: ubuntu-24.04
    timeout-minutes: 360
    env:
      LEAN_NUM_THREADS: "1"
      PYTHONDONTWRITEBYTECODE: "1"
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
        with:
          persist-credentials: false
      - name: Audit the full physical source manifest
        shell: bash
        run: |
          set -euo pipefail
          mkdir -p "$RUNNER_TEMP/verification"
          python3 -B .github/verification/generate_manifest.py \
            --root . --config .github/verification/manifest-config.json \
            --manifest "$RUNNER_TEMP/verification/modules.json" \
            --report "$RUNNER_TEMP/verification/source-audit.json" 2>&1 | tee "$RUNNER_TEMP/verification/source-audit.log"
      - name: Install pinned Lean and obtain the pinned mathlib cache
        uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1
        with:
          auto-config: "false"
          build: "false"
          test: "false"
          lint: "false"
          use-mathlib-cache: "true"
          use-github-cache: "false"
      - name: Restore completed project outputs from the depth jobs
        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
        with:
          path: |
            .lake/build/lib/lean
            .lake/build/ir/**/*.c
            .lake/build/ir/**/*.c.hash
            .lake/build/ir/**/*.bc
            .lake/build/ir/**/*.bc.hash
            ${{ runner.temp }}/project-build-cache.json
          key: lean-project-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}-verify-${{ github.run_id }}-${{ github.run_attempt }}
          restore-keys: |
            lean-project-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}-
            lean-project-v1-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
      - name: Validate cached output integrity
        shell: bash
        run: |
          set -euo pipefail
          python3 -B .github/verification/project_cache.py restore \
            --metadata "$RUNNER_TEMP/project-build-cache.json" \
            --report "$RUNNER_TEMP/verification/cache-restore.json"
      - name: Build exact checker revisions
        shell: bash
        run: |
          set -euo pipefail
          python3 -B .github/verification/setup_tools.py \
            --checkouts "$RUNNER_TEMP/verification-tools" \
            --output "$RUNNER_TEMP/verification/setup"
      - name: Build, audit all declarations, check NanoDa, and replay the Lean kernel
        shell: bash
        run: |
          set -euo pipefail
          python3 -B .github/verification/verify.py \
            --package-root "$GITHUB_WORKSPACE" \
            --manifest "$RUNNER_TEMP/verification/modules.json" \
            --output "$RUNNER_TEMP/verification/checks" \
            --exporter-checkout "$RUNNER_TEMP/verification-tools/lean4export" \
            --nanoda-checkout "$RUNNER_TEMP/verification-tools/nanoda_lib" \
            --nanoda-binary "$RUNNER_TEMP/verification-tools/nanoda_lib/target/release/nanoda_bin"
      - name: Check designated main declarations in the audited inventory
        shell: bash
        run: |
          set -euo pipefail
          python3 -B .github/verification/check_main_declarations.py \
            --contract .github/verification/main-declarations.json \
            --verification "$RUNNER_TEMP/verification/checks" \
            --output "$RUNNER_TEMP/verification/main-declarations.json"
      - name: Check whitespace
        run: git diff-tree --check --root -r HEAD
      - name: Preserve logs and receipts even when a check fails
        if: always()
        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
        with:
          name: verification-${{ github.run_id }}-${{ github.run_attempt }}
          path: |
            ${{ runner.temp }}/verification/
            !${{ runner.temp }}/verification/checks/selected.ndjson
          if-no-files-found: error
          retention-days: 14