name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  verify:
    runs-on: ubuntu-latest
    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 11bd7190 (= refs/tags/v4.2.2 as of 2026-05-04).
      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
        with:
          fetch-depth: 0

      # 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

      # actions/setup-go pinned to d35c59ab (= refs/tags/v5.5.0 as of 2026-05-04).
      - uses: actions/setup-go@d35c59abb061a4a6fb18e82ac0862c26744d6ab5
        with:
          # Concrete Go version, not `stable`, so a runner-image bump cannot
          # silently change the toolchain we install landrun with.
          go-version: '1.24.0'

      - 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: |
          git clone https://github.com/leanprover/lean4export.git .ci/lean4export
          cd .ci/lean4export
          # lean4export pinned to 3de59f10 (= refs/tags/v4.32.0-rc1 as of 2026-06-27).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout 3de59f10bc4b4a0f2de698597aeb1246caa0df0a  # pin-audit: exempt -- SHA, see comment
          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 71b52ec2 (leanprover/comparator, originally adopted before 2026-05-04).
          # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
          git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0  # pin-audit: exempt -- SHA, see comment
          lake build comparator
          echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

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

      # SECURITY: assert comparator's landrun sandbox actually denies
      # writes outside .lake/. Catches landrun fail-open on novel
      # kernels and policy regressions in comparator. See SECURITY.md
      # > "Validations done at submission time" > sandbox-engaged.
      - name: Probe sandbox is engaged
        run: python scripts/sandbox_engaged_probe.py --require-tools

      # SECURITY: assert env-var allowlist seen by Submission's
      # elaboration is exactly {PATH, HOME, LEAN_ABORT_ON_PANIC}.
      # Catches secret-env-var leakage to user code if comparator's
      # envPass ever drifts. See SECURITY.md > "env allowlist".
      - name: Probe env-var allowlist
        run: python scripts/security_probes/env_dump_probe.py --require-tools

      - name: Python Syntax Checks
        run: python -m py_compile scripts/*.py scripts/security_probes/*.py

      - name: Validate Manifest
        run: lake exe lean-eval validate-manifest

      - name: Build Problem Modules
        run: lake exe lean-eval check-problem-build

      # Decide whether to run workspace generation/build. Source-only PRs
      # regenerate generated/ in the runner's working tree (the regenerate-main
      # workflow is the only thing that commits generated/ to main); solver PRs
      # build the committed tree as-is. Done early so that downstream steps
      # which read generated/ (e.g. `lean-eval check-eval-workflow`) see a tree
      # that matches the source.
      - name: Detect changes
        id: changes
        run: |
          BASE="${{ github.event.pull_request.base.sha || github.event.before }}"
          if [ "$BASE" = "0000000000000000000000000000000000000000" ]; then
            echo "source_changed=true" >> "$GITHUB_OUTPUT"
            echo "generated_changed=true" >> "$GITHUB_OUTPUT"
          else
            CHANGED=$(git diff --name-only "$BASE"..HEAD)
            if echo "$CHANGED" | grep -Eq '^(LeanEval/|EvalTools/|templates/|manifests/problems/.*\.toml$|lakefile\.toml$|lean-toolchain$)'; then
              echo "source_changed=true" >> "$GITHUB_OUTPUT"
            else
              echo "source_changed=false" >> "$GITHUB_OUTPUT"
            fi
            if echo "$CHANGED" | grep -q '^generated/'; then
              echo "generated_changed=true" >> "$GITHUB_OUTPUT"
            else
              echo "generated_changed=false" >> "$GITHUB_OUTPUT"
            fi
          fi

      - name: Regenerate workspaces from source
        if: steps.changes.outputs.source_changed == 'true'
        run: lake exe lean-eval generate

      - name: Submission Policy Check
        run: lake exe lean-eval validate-submission --file generated/two_plus_two/Solution.lean

      # Submission diff validation is a PR-time contributor policy: it
      # decides whether a PR that only touches `generated/` looks like a
      # well-formed submission. On `push` to `main` the diffs we see are
      # either merged PR results or the regenerator bot's
      # `chore: regenerate generated/ workspaces` commit, neither of
      # which the submission policy applies to. `main` itself is
      # PR-protected for humans (see docs/ci-secrets.md), so we lose no
      # meaningful coverage by gating this step on `pull_request`.
      - 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

          mapfile -t CHANGED_FILES < <(git diff --name-only "$BASE_SHA..$HEAD_SHA")

          if [ "${#CHANGED_FILES[@]}" -eq 0 ]; then
            echo "No changed files in $BASE_SHA..$HEAD_SHA; skipping submission diff validation."
            exit 0
          fi

          IS_SUBMISSION_DIFF=true
          for path in "${CHANGED_FILES[@]}"; do
            if [[ ! "$path" =~ ^generated/ ]]; then
              IS_SUBMISSION_DIFF=false
              break
            fi
          done

          if [ "$IS_SUBMISSION_DIFF" = false ]; then
            echo "Diff includes non-generated paths; treating this as repo development and skipping submission diff validation."
            exit 0
          fi

          lake exe lean-eval validate-submission --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Run Submission Policy Tests
        run: lake exe test_validate_submission

      - name: Run Generate Tests
        run: lake exe test_generate

      - name: Run Comparator Installation Checks
        run: |
          lake exe test_check_comparator_installation
          lake exe lean-eval check-comparator-installation

      - name: Run Eval Workflow Check
        run: lake exe lean-eval check-eval-workflow

      # Download Mathlib cache once in the first workspace, then hard-link
      # its .lake/packages tree into every other workspace so that each
      # subsequent `lake build` skips the ~2 GB download + decompression.
      - name: Prepare shared Mathlib cache for workspaces
        if: steps.changes.outputs.source_changed == 'true' || steps.changes.outputs.generated_changed == 'true'
        run: |
          set -euo pipefail
          FIRST=$(find generated -maxdepth 1 -mindepth 1 -type d -exec test -f '{}/lakefile.toml' \; -print | sort | head -1)
          if [ -z "$FIRST" ]; then
            echo "No generated workspaces found; skipping."
            exit 0
          fi
          echo "==> Fetching Mathlib cache in $FIRST"
          (cd "$FIRST" && lake update && lake exe cache get)
          for ws in generated/*/; do
            [ -f "${ws}lakefile.toml" ] || continue
            [ "$(realpath "$ws")" = "$(realpath "$FIRST/")" ] && continue
            echo "==> Linking Mathlib packages into $ws"
            mkdir -p "${ws}.lake"
            rm -rf "${ws}.lake/packages"
            cp -al "${FIRST}/.lake/packages" "${ws}.lake/packages"
            cp "${FIRST}/lake-manifest.json" "${ws}lake-manifest.json"
          done

      - name: Build Generated Workspaces
        if: steps.changes.outputs.source_changed == 'true' || steps.changes.outputs.generated_changed == 'true'
        run: lake exe lean-eval check-generated-builds