ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - name: Free up disk space
        uses: jlumbroso/free-disk-space@v1.3.1
        with:
          tool-cache: false
          android: true
          dotnet: true
          haskell: true
          large-packages: true
          docker-images: true
          swap-storage: true

      - uses: actions/checkout@v4
        with:
          fetch-depth: 0

      - uses: leanprover/lean-action@v1
        with:
          use-mathlib-cache: true

      - uses: actions/setup-go@v5
        with:
          go-version: stable

      - name: Install landrun
        run: |
          go install github.com/zouuup/landrun/cmd/landrun@main
          echo "$(go env GOPATH)/bin" >> "$GITHUB_PATH"

      - name: Build lean4export
        run: |
          git clone https://github.com/leanprover/lean4export.git .ci/lean4export
          cd .ci/lean4export
          git checkout v4.30.0-rc2
          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
          git checkout 71b52ec29e06d4b7d882726553b1ceb99a2499e0
          lake build comparator
          echo "$PWD/.lake/build/bin" >> "$GITHUB_PATH"

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

      - name: Validate Manifest
        run: python scripts/validate_manifest.py

      - name: Build Problem Modules
        run: python scripts/check_problem_build.py

      # 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. check_eval_workflow.py) 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/|manifests/problems\.toml$|scripts/generate_projects\.py$|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: python scripts/generate_projects.py

      - name: Submission Policy Check
        run: python scripts/validate_submission.py --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

          python scripts/validate_submission.py --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Run Submission Policy Tests
        run: python -m unittest tests.test_validate_submission

      - name: Run Generator Tests
        run: python -m unittest tests.test_generate_projects

      - name: Run Scoring Tests
        run: python -m unittest tests.test_run_eval

      - name: Run Leaderboard Update Tests
        run: python -m unittest tests.test_update_leaderboard

      - name: Run Fetch Submission Tests
        run: python -m unittest tests.test_fetch_submission

      - name: Run Evaluate Submission Tests
        run: python -m unittest tests.test_evaluate_submission

      - name: Run Comparator Installation Checks
        run: |
          python -m unittest tests.test_check_comparator_installation
          python scripts/check_comparator_installation.py

      - name: Run Eval Workflow Check
        run: python scripts/check_eval_workflow.py

      # 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: python scripts/check_generated_builds.py