ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

# A superseded five-hour run has no value. This also prevents a burst of PR
# updates from consuming the entire hosted-runner pool with stale work.
concurrency:
  group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

permissions:
  contents: read

jobs:
  classify:
    name: Classify changes
    runs-on: ubuntu-latest
    timeout-minutes: 5
    outputs:
      source_changed: ${{ steps.changes.outputs.source_changed }}
      generated_changed: ${{ steps.changes.outputs.generated_changed }}
      run_checks: ${{ steps.changes.outputs.run_checks }}
      run_catalog: ${{ steps.changes.outputs.run_catalog }}
      selection_mode: ${{ steps.changes.outputs.selection_mode }}
      selected_problem_count: ${{ steps.changes.outputs.selected_problem_count }}
      selected_modules: ${{ steps.changes.outputs.selected_modules }}
      matrix: ${{ steps.changes.outputs.matrix }}
    steps:
      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
        with:
          fetch-depth: 0
          persist-credentials: false

      - name: Audit workflow action pins
        run: python scripts/action_pin_audit.py

      - name: Python syntax checks
        run: python -m py_compile scripts/*.py scripts/security_probes/*.py

      # Install the pinned Lean toolchain without building the project. The
      # dependency selector consumes a graph produced by Lean's header parser;
      # Python never attempts to parse Lean import syntax.
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          build: false
          test: false
          lint: false
          use-mathlib-cache: false
          use-github-cache: false

      - name: Export Lean import graph
        run: |
          set -euo pipefail
          mkdir -p .ci
          lake build EvalTools.CIImportGraph
          lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json

      - name: Select affected catalog problems
        id: changes
        env:
          BASE_SHA: ${{ github.event.pull_request.base.sha || github.event.before }}
          HEAD_SHA: ${{ github.event.pull_request.head.sha || github.sha }}
        run: |
          set -euo pipefail
          python scripts/select_ci_problems.py \
            --event "$GITHUB_EVENT_NAME" \
            --base "$BASE_SHA" \
            --head "$HEAD_SHA" \
            --shards 8 \
            --import-graph .ci/import-graph.json \
            --github-output "$GITHUB_OUTPUT"

  checks:
    name: Repository checks
    needs: classify
    if: needs.classify.outputs.run_checks == 'true'
    runs-on: ubuntu-latest
    timeout-minutes: 90
    steps:
      - name: Free up disk space
        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
        with:
          tool-cache: false
          android: true
          dotnet: true
          haskell: true
          large-packages: true
          docker-images: true
          swap-storage: true

      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
        with:
          fetch-depth: 0
          persist-credentials: false

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true
          # Nothing here needs the whole library built, and building it would
          # compile TauCeti; the catalog shards build problem modules from its
          # cache.
          build: false
          test: false
          lint: false

      # Module compilation and tagged-declaration inventory now run in the
      # catalog shards. Keep the cheap whole-repository invariants here.
      - name: Validate manifest structure and module coverage
        run: lake exe lean-eval validate-manifest --structure-only

      - name: Validate catalog lifecycle metadata and frozen sets
        env:
          BASE_SHA: ${{ github.event.pull_request.base.sha || github.event.before }}
        run: |
          set -euo pipefail
          base_args=()
          if [ -n "$BASE_SHA" ] &&
              [ "$BASE_SHA" != "0000000000000000000000000000000000000000" ] &&
              git cat-file -e "$BASE_SHA^{commit}"; then
            base_args+=(--base-ref "$BASE_SHA")
          fi
          python scripts/validate_catalog.py "${base_args[@]}"

      # Source-only changes intentionally leave generated/index.json for the
      # trusted main regenerator. If a PR touches generated/ itself, however,
      # its committed global index must be current and it may not add an
      # unexpected workspace directory.
      - name: Validate generated index and unexpected directories
        if: needs.classify.outputs.source_changed != 'true' || needs.classify.outputs.generated_changed == 'true'
        run: lake exe lean-eval validate-generated-catalog

      - name: Submission policy smoke check
        run: lake exe lean-eval validate-submission --file generated/two_plus_two/Solution.lean

      - name: Submission policy diff check
        if: github.event_name == 'pull_request'
        env:
          BASE_SHA: ${{ github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
        run: |
          set -euo pipefail
          MERGE_BASE=$(git merge-base "$BASE_SHA" "$HEAD_SHA")
          mapfile -t changed_files < <(git diff --name-only "$MERGE_BASE".."$HEAD_SHA")
          if [ "${#changed_files[@]}" -eq 0 ]; then
            echo "No changed files; skipping submission diff validation."
            exit 0
          fi
          for path in "${changed_files[@]}"; do
            if [[ ! "$path" =~ ^generated/ ]]; then
              echo "Diff includes repository source; skipping submission-only validation."
              exit 0
            fi
          done
          lake exe lean-eval validate-submission --base "$MERGE_BASE" --head "$HEAD_SHA"

      - name: Run Lean unit tests
        run: |
          lake exe test_validate_submission
          lake exe test_generate
          lake exe test_module_coverage
          lake exe test_check_comparator_installation

      - name: Run Python unit tests
        run: python -m unittest discover -s tests/python -p 'test_*.py'

  security:
    name: Security and scoring smoke tests
    needs: classify
    if: needs.classify.outputs.run_checks == 'true'
    runs-on: ubuntu-latest
    timeout-minutes: 60
    steps:
      - name: Free up disk space
        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
        with:
          tool-cache: false
          android: true
          dotnet: true
          haskell: true
          large-packages: true
          docker-images: true
          swap-storage: true

      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
        with:
          fetch-depth: 0
          persist-credentials: false

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true
          # Nothing here needs the whole library built, and building it would
          # compile TauCeti; the catalog shards build problem modules from its
          # cache.
          build: false
          test: false
          lint: false

      # actions/setup-go pinned to b7ad1dad (= refs/tags/v7.0.0 as of 2026-07-30).
      - uses: actions/setup-go@b7ad1dad31e06c5925ef5d2fc7ad053ef454303e
        with:
          go-version: '1.25.12'
          cache: false

      - name: Install landrun
        run: |
          # landrun pinned to 5ed4a3db (zouuup/landrun main HEAD as of 2026-05-04).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          go install github.com/zouuup/landrun/cmd/landrun@5ed4a3db3a4ad930d577215c6b9abaa19df7f99f
          echo "$(go env GOPATH)/bin" >> "$GITHUB_PATH"

      - name: Build lean4export
        run: |
          set -euo pipefail
          git clone https://github.com/leanprover/lean4export.git .ci/lean4export
          cd .ci/lean4export
          # lean4export pinned to 076e8e57 (= refs/tags/v4.34.0 as of 2026-09-16).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout 076e8e57707e813375e8f9da8bf989799ace9680  # pin-audit: exempt -- SHA, see comment
          cp "$GITHUB_WORKSPACE/lean-toolchain" lean-toolchain
          lake build lean4export
          echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

      - name: Build comparator
        run: |
          git clone https://github.com/leanprover/comparator.git .ci/comparator
          cd .ci/comparator
          # comparator pinned to d03acab1 (= refs/tags/v4.34.0 as of 2026-09-16).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout d03acab154d269c06e60e4de7e4cc85deebff94b  # pin-audit: exempt -- SHA, see comment
          lake build comparator
          echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

      - name: Build nanoda
        run: |
          set -euo pipefail
          git clone https://github.com/robsimmons/nanoda_lib.git .ci/nanoda
          cd .ci/nanoda
          # nanoda pinned to 68d5ca9 (robsimmons/nanoda_lib HEAD as of 2026-07-29).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout 68d5ca9db226849b41a6fff59d796ff19d0a8840  # pin-audit: exempt -- SHA, see comment
          cargo build --release
          echo "$PWD/target/release" >> "$GITHUB_PATH"

      # These probes stay in the mandatory path. Parallelization must not
      # weaken the submission trust boundary.
      - name: Probe sandbox is engaged
        run: python scripts/sandbox_engaged_probe.py --require-tools

      - name: Probe env-var allowlist
        run: python scripts/security_probes/env_dump_probe.py --require-tools

      - name: Refresh smoke-test workspace
        run: lake exe lean-eval generate --problem two_plus_two

      - name: Check comparator installation
        run: lake exe lean-eval check-comparator-installation

      - name: Run eval workflow smoke test
        run: lake exe lean-eval check-eval-workflow

  catalog:
    name: Catalog validation (shard ${{ matrix.shard }}/${{ matrix.shard_count }})
    needs: classify
    if: needs.classify.outputs.run_catalog == 'true'
    runs-on: ubuntu-latest
    timeout-minutes: 60
    strategy:
      fail-fast: false
      matrix: ${{ fromJSON(needs.classify.outputs.matrix) }}
    steps:
      - name: Free up disk space
        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
        with:
          tool-cache: false
          android: true
          dotnet: true
          haskell: true
          large-packages: true
          docker-images: true
          swap-storage: true

      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
        with:
          fetch-depth: 0
          persist-credentials: false

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true
          build: false
          test: false
          lint: false

      - name: Fetch TauCeti's build cache
        # Problem modules that import TauCeti download its published oleans
        # instead of compiling it; see scripts/fetch_dependency_caches.sh.
        run: bash scripts/fetch_dependency_caches.sh --restore .

      - name: Clear cached problem-module artifacts
        run: |
          set -euo pipefail
          artifact_dir=.lake/build/lib/lean/LeanEval
          if [ -d "$artifact_dir" ]; then
            find "$artifact_dir" \( -type f -o -type l \) -delete
          fi

      - name: Build problem modules without warnings
        env:
          MODULES: ${{ matrix.modules }}
          SHARD_INDEX: ${{ matrix.shard }}
        run: |
          set -euo pipefail
          IFS=',' read -r -a modules <<< "$MODULES"
          module_args=()
          for module in "${modules[@]}"; do
            module_args+=(--module "$module")
          done
          lake exe lean-eval check-problem-build "${module_args[@]}"
          mkdir -p .ci/problem-inventory
          lake exe lean-eval problem-inventory \
            ".ci/problem-inventory/$SHARD_INDEX.json" "${module_args[@]}"

      - name: Generate or verify this shard
        env:
          PROBLEMS: ${{ matrix.problems }}
          SOURCE_CHANGED: ${{ needs.classify.outputs.source_changed }}
          GENERATED_CHANGED: ${{ needs.classify.outputs.generated_changed }}
          EVENT_NAME: ${{ github.event_name }}
        run: |
          set -euo pipefail
          IFS=',' read -r -a selected <<< "$PROBLEMS"
          if [ "${#selected[@]}" -eq 0 ]; then
            echo "Shard is empty."
            exit 0
          fi
          printf 'Selected problems: %s\n' "${selected[*]}"

          generate_mode="none"
          if [ "$SOURCE_CHANGED" = true ]; then
            generate_mode="write"
          elif [ "$EVENT_NAME" = push ] && [ "$GENERATED_CHANGED" = true ]; then
            generate_mode="check"
          fi
          if [ "$generate_mode" != none ]; then
            for problem in "${selected[@]}"; do
              if [ "$generate_mode" = check ]; then
                lake exe lean-eval generate --problem "$problem" --check
              else
                lake exe lean-eval generate --problem "$problem"
              fi
            done
          fi

          # Every workspace requires a subset of the root's pinned dependencies
          # (always Mathlib, plus e.g. TauCeti for problems that import it).
          # Reuse the root cache with symlinks instead of cloning/decompressing
          # it once and hard-link-walking ~13 GB hundreds of times, and give
          # each workspace the root manifest, which pins all of them. Running
          # `lake update` here instead could re-resolve transitive dependencies
          # and check them out inside the shared package directory.
          for problem in "${selected[@]}"; do
            mkdir -p "generated/$problem/.lake"
            ln -s "$GITHUB_WORKSPACE/.lake/packages" \
              "generated/$problem/.lake/packages"
            cp lake-manifest.json "generated/$problem/lake-manifest.json"
          done

          build_args=()
          for problem in "${selected[@]}"; do
            build_args+=(--problem "$problem")
          done
          lake exe lean-eval check-generated-builds "${build_args[@]}"

      - name: Upload problem inventory
        # actions/upload-artifact pinned to 043fb46d (= refs/tags/v7.0.1 as of 2026-08-17).
        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a
        with:
          name: problem-inventory-${{ matrix.shard }}
          path: .ci/problem-inventory/${{ matrix.shard }}.json
          if-no-files-found: error
          retention-days: 1

  catalog_inventory:
    name: Manifest inventory aggregate
    needs: [classify, catalog]
    if: needs.classify.outputs.run_catalog == 'true'
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
        with:
          persist-credentials: false

      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          use-mathlib-cache: true
          build: false
          test: false
          lint: false

      - name: Download problem inventories
        # actions/download-artifact pinned to 3e5f45b2 (= refs/tags/v8.0.1 as of 2026-08-17).
        uses: actions/download-artifact@3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c
        with:
          pattern: problem-inventory-*
          path: .ci/problem-inventory
          merge-multiple: true

      - name: Validate aggregated manifest inventory
        env:
          MODULES: ${{ needs.classify.outputs.selected_modules }}
        run: |
          set -euo pipefail
          IFS=',' read -r -a modules <<< "$MODULES"
          module_args=()
          for module in "${modules[@]}"; do
            module_args+=(--module "$module")
          done
          lake exe lean-eval validate-manifest \
            --inventory-dir .ci/problem-inventory "${module_args[@]}"

  # Preserve the existing required-check name while making it an aggregate of
  # every parallel branch. A green `verify` now means the entire fan-out passed.
  verify:
    name: verify
    if: always()
    needs: [classify, checks, security, catalog, catalog_inventory]
    runs-on: ubuntu-latest
    timeout-minutes: 2
    steps:
      - name: Require every CI branch to pass
        env:
          CLASSIFY_RESULT: ${{ needs.classify.result }}
          CHECKS_RESULT: ${{ needs.checks.result }}
          SECURITY_RESULT: ${{ needs.security.result }}
          CATALOG_RESULT: ${{ needs.catalog.result }}
          CATALOG_INVENTORY_RESULT: ${{ needs.catalog_inventory.result }}
        run: |
          set -euo pipefail
          for result in "$CLASSIFY_RESULT" "$CHECKS_RESULT" \
              "$SECURITY_RESULT" "$CATALOG_RESULT" \
              "$CATALOG_INVENTORY_RESULT"; do
            if [ "$result" != success ] && [ "$result" != skipped ]; then
              echo "A required CI branch ended with: $result" >&2
              exit 1
            fi
          done