name: Lean Action CI

# The build runs in one of three modes, decided per run by a cheap `plan` job
# (scripts/ci/plan-build-shards.py) from the diff and the cache state:
#
# - `skip`: an exact README-only change. It still reports the
#   protected `Build project` check without spending hours rebuilding Lean.
# - `single`: the classic one-job pipeline. This is the fast path for the
#   common case — a PR that adds or edits a project or three.
# - `rebase`: reuse an earlier green PR build after the automatic merge of
#   independent pool content, then build the combined root and check metadata.
# - `sharded`: for the runs that take hours serially (cold cache,
#   toolchain/manifest bump, refactors touching many projects), the dirty
#   projects are bin-packed into parallel `shard` build jobs. Pool projects
#   never import each other, so project-granular shards duplicate no work.
#   Each shard uploads only the files its build produced; `finalize` merges
#   them, builds the root library (also a safety net: anything a shard
#   missed is built here), and runs the whole-pool linters and quality
#   checks once.
#
# Shard assignment is computed from the tree at run time — there is no
# static shard list to maintain as the pool grows. The `Build project`
# gate job reports the overall verdict under the same check name the
# single-job workflow used.

on:
  merge_group:
    types: [checks_requested]
  push:
    branches:
      - main
    paths:
      - '**/*.lean'
      - 'lakefile.toml'
      - 'lean-toolchain'
      - 'lake-manifest.json'
      - 'LeanPool/projects/**'
      - 'LeanPool/projects.yml'
      - 'python/lean_pool/quality.py'
      - 'python/lean_pool/registry.py'
      - 'python/lean_pool/indexes.py'
      - 'python/lean_pool/queue_build.py'
      - 'python/lean_pool/validation_cache.py'
      - 'python/lean_pool/ci_artifacts.py'
      - 'python/lean_pool/ci_cache.py'
      - 'python/lean_pool/ci_pr_build.py'
      - 'python/lean_pool/ci_validation_artifacts.py'
      - 'python/lean_pool/rebase_fastpath.py'
      - 'python/pyproject.toml'
      - 'python/uv.lock'
      - 'scripts/nolints-style.txt'
      - 'scripts/ci/**'
      - '.github/CODE_QUALITY.md'
      - '.github/workflows/lean_action_ci.yml'
  pull_request:
    branches:
      - main
      # Work stacks on the bump branch during a Lean/Mathlib migration, and
      # a contribution that never builds is a contribution nobody can judge:
      # PR #301 added a 210-file project onto `bump/v4.33.0-rc1` and got no
      # build, no linters, and no quality checks at all.
      - 'bump/**'
  workflow_dispatch:
    inputs:
      force_full:
        description: "Shard-build the whole pool even when a warm cache exists"
        required: false
        type: boolean
        default: false

# Let main finish and seed caches; cancel superseded PR runs.
concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}

permissions:
  contents: read
  pages: write
  id-token: write
  actions: read

jobs:
  plan:
    runs-on: ubuntu-latest
    name: Plan build
    outputs:
      build_revision: ${{ steps.build-identity.outputs.revision }}
      base_build_revision: ${{ steps.build-identity.outputs.base_revision }}
      minimal_build: ${{ steps.plan.outputs.minimal_build }}
      dependency_tests: ${{ steps.plan.outputs.dependency_tests }}
      mode: ${{ steps.plan.outputs.mode }}
      matrix: ${{ steps.plan.outputs.matrix }}
      reuse_run_id: ${{ steps.plan.outputs.reuse_run_id }}
      previous_head: ${{ steps.plan.outputs.previous_head }}
    steps:
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      - name: Install Python tooling runtime
        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
        with:
          enable-cache: true

      - name: Identify compiled Lean sources
        id: build-identity
        env:
          BASE_REF: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha || github.sha }}
        run: |
          set -euo pipefail
          revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
          echo "revision=$revision" >> "$GITHUB_OUTPUT"
          base_revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision --ref "$BASE_REF")
          echo "base_revision=$base_revision" >> "$GITHUB_OUTPUT"

      # A cold build cache is when whole-pool sharding pays off most.
      - name: Check for a warm build cache
        id: lake-cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          lookup-only: true
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ steps.build-identity.outputs.revision }}
          restore-keys: |
            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Plan the build
        id: plan
        env:
          EVENT_NAME: ${{ github.event_name }}
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          BEFORE_SHA: ${{ github.event.before }}
          FORCE_FULL: ${{ inputs.force_full }}
          CACHE_MATCHED: ${{ steps.lake-cache.outputs.cache-matched-key }}
          GH_TOKEN: ${{ github.token }}
          REPOSITORY: ${{ github.repository }}
          PR_NUMBER: ${{ github.event.pull_request.number }}
          PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
        run: |
          set -euo pipefail
          diff_available=true
          # A file, not an environment variable: a large import's path list
          # exceeds the kernel's 128 KiB limit on a single environment string.
          changed_files="$RUNNER_TEMP/changed-files.txt"
          : > "$changed_files"
          case "$EVENT_NAME" in
            merge_group)
              git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files"
              ;;
            pull_request)
              git diff --name-only --no-renames "$BASE_SHA"...HEAD > "$changed_files"
              ;;
            push)
              if [ -n "$BEFORE_SHA" ] \
                 && ! printf '%s' "$BEFORE_SHA" | grep -q '^0*$' \
                 && git cat-file -e "$BEFORE_SHA" 2>/dev/null; then
                git diff --name-only --no-renames "$BEFORE_SHA"..HEAD > "$changed_files"
              else
                diff_available=false
              fi
              ;;
            workflow_dispatch)
              diff_available=false
              ;;
          esac
          minimal_build=false
          if [ "$EVENT_NAME" = pull_request ] && grep -Eq '^(python/lean_pool/(exposition/|ci_artifacts.py$)|scripts/exposition/|.github/workflows/exposition-verify.yml$)' "$changed_files"; then
            minimal_build=true
          fi
          echo "minimal_build=$minimal_build" >> "$GITHUB_OUTPUT"
          dependency_tests=true
          if [ "$diff_available" = true ] && [ "$FORCE_FULL" != true ]; then
            dependency_tests=false
            # Git may quote names containing Unicode or control characters.
            if grep -Eq '^"?(lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/|scripts/ci/|scripts/exposition/|scripts/ProjectIndexes\.lean$|\.github/workflows/lean_action_ci\.yml$)' "$changed_files"; then
              dependency_tests=true
            fi
          fi
          echo "dependency_tests=$dependency_tests" >> "$GITHUB_OUTPUT"
          cold=false
          if [ -z "$CACHE_MATCHED" ]; then cold=true; fi
          plan=$(CHANGED_FILES_PATH="$changed_files" DIFF_AVAILABLE="$diff_available" \
                 COLD="$cold" FORCE_FULL="$FORCE_FULL" \
                 python3 scripts/ci/plan-build-shards.py)
          reuse_run_id=""
          previous_head=""
          if [ "$EVENT_NAME" = "pull_request" ] && [ "$FORCE_FULL" != "true" ] && [ "$minimal_build" != true ]; then
            reuse=$(PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath decide \
              --repository "$REPOSITORY" --number "$PR_NUMBER" \
              --head "$PR_HEAD" --base "$BASE_SHA")
            if [ "$(echo "$reuse" | python3 -c 'import json,sys; print(str(json.load(sys.stdin)["eligible"]).lower())')" = true ]; then
              reuse_run_id=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["run_id"])')
              previous_head=$(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["previous_head"])')
              plan='{"mode":"rebase","matrix":{"include":[{"shard":"00","projects":""}]}}'
            else
              echo "Rebase reuse unavailable: $(echo "$reuse" | python3 -c 'import json,sys; print(json.load(sys.stdin)["reason"])')"
            fi
          fi
          echo "Plan: $plan"
          {
            echo "mode=$(echo "$plan" | python3 -c 'import json,sys; print(json.load(sys.stdin)["mode"])')"
            echo "matrix=$(echo "$plan" | python3 -c 'import json,sys; print(json.dumps(json.load(sys.stdin)["matrix"]))')"
            echo "reuse_run_id=$reuse_run_id"
            echo "previous_head=$previous_head"
          } >> "$GITHUB_OUTPUT"

  # The single-job pipeline is the fast path for ordinary PRs.
  build:
    needs: plan
    if: needs.plan.outputs.mode == 'single'
    runs-on: ubuntu-latest
    name: Build pool
    permissions:
      contents: read
      actions: write
    steps:
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      # Keep the large toolchain/Mathlib cache independent of per-commit builds.
      - name: Restore Lean dependencies
        id: dependency-cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Restore pool build
        id: cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
          restore-keys: |
            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Install Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: false

      - name: Install uv
        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
        with:
          enable-cache: true

      - name: Check compiled artifact dependency tracking with pinned Lean
        if: needs.plan.outputs.dependency_tests == 'true'
        env:
          LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
        run: >-
          uv run --project python --group test pytest -q
          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
          -k 'test_lake_'

      - name: Install Mathlib cache
        id: mathlib-cache
        run: |
          if [ ! -d ".lake/packages/mathlib" ]; then
            ~/.elan/bin/lake exe cache get
          else
            echo "Mathlib already present from cache"
          fi

      - name: Check library indexes use the module system and are up to date
        run: |
          if ! ~/.elan/bin/lake exe mk_all --module --check; then
            echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result."
            exit 1
          fi

      - name: Reuse compiled projects from merged PRs
        if: github.event_name == 'push' && steps.cache.outputs.cache-hit != 'true'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          REPOSITORY: ${{ github.repository }}
          BEFORE_SHA: ${{ github.event.before }}
        run: |
          if PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build \
            --repository "$REPOSITORY" --base "$BEFORE_SHA" --head "$GITHUB_SHA" --merged; then
            echo 'Restored the successfully merged queue build.'
          elif git cat-file -e "$BEFORE_SHA" 2>/dev/null; then
            PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main \
              --repository "$REPOSITORY" --head "$BEFORE_SHA" --base "$GITHUB_SHA"
          fi

      - name: Reuse compiled files from this PR's successful runs
        if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          PR_NUMBER: ${{ github.event.pull_request.number }}
          PR_BRANCH: ${{ github.head_ref }}
          PR_HEAD: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
          PR_BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          CURRENT_RUN: ${{ github.run_id }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build
          --number "$PR_NUMBER" --branch "$PR_BRANCH"
          --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN"

      - name: Reuse successful queued PR builds
        if: github.event_name == 'merge_group'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BASE_SHA: ${{ github.event.merge_group.base_sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
          --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Build project
        id: compilation
        run: |
          set -euo pipefail
          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
          if grep -nE '(^|: )warning:' lean-build.log; then
            echo "::error::Lean build emitted warnings; fix them before merging."
            exit 1
          fi

      # Main publishes the shared full build. A minimal-verifier PR publishes
      # only its own projects; the verifier overlays them on the main cache.
      - name: Package build for documentation
        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
        env:
          BUILD_EVENT: ${{ github.event_name }}
          BASE_SHA: ${{ github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
        run: |
          if [ "$BUILD_EVENT" = pull_request ]; then
            PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack --base "$BASE_SHA" --head "$HEAD_SHA"
          else
            PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
          fi

      - name: Share build with documentation
        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lean-pool-build
          path: lean-pool-build.tar.zst
          if-no-files-found: error
          compression-level: 0
          retention-days: 1

      # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same
      # PR can reuse receipts, while main and other PRs cannot read them.
      - name: Restore project validation
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/validation-cache/v1
          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
          restore-keys: |
            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Recover saved validation when caches were evicted
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BUILD_EVENT: ${{ github.event_name }}
          BUILD_HEAD: ${{ github.sha }}
        run: >-
          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
          --event "$BUILD_EVENT" --head "$BUILD_HEAD"

      - name: Install validation dependencies
        run: cd python && uv sync --locked

      - name: Reuse successful queued PR validation
        if: github.event_name == 'merge_group'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BASE_SHA: ${{ github.event.merge_group.base_sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
          --base "$BASE_SHA" --head "$HEAD_SHA" --receipts

      - name: Lint
        run: |
          cd python
          uv run python -m lean_pool.validation_cache lint --repo ..
          cd ..

      - name: Text style lint
        run: |
          ~/.elan/bin/lake exe lint-style LeanPool

      - name: Repository quality checks
        run: |
          cd python
          uv run python -m lean_pool.validation_cache quality --repo ..

      - name: Retain successful validation independently of build caches
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lean-validation-receipts
          path: .lake/validation-cache/v1/passes.json
          include-hidden-files: true
          if-no-files-found: error
          compression-level: 1
          retention-days: 14

      - name: Package PR project build for later rebases
        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
        continue-on-error: true
        env:
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Retain PR project build
        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: rebase-project-build
          path: rebase-project-build.tar.gz
          if-no-files-found: error
          compression-level: 0
          retention-days: 14

      - name: Save project validation
        # Successful receipts are tiny; retain PR results across registry rebases.
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/validation-cache/v1
          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}

      - name: Save Lean dependencies
        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Save pool build
        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}

  shard:
    needs: plan
    if: needs.plan.outputs.mode == 'sharded'
    runs-on: ubuntu-latest
    name: Build shard ${{ matrix.shard }}
    strategy:
      # One shard failing must not cancel the rest: `finalize` rebuilds any
      # gap itself, so the run still yields a complete log — but the gate
      # job fails whenever a shard failed (a shard's warning gate must not
      # be bypassable by cache replay in `finalize`).
      fail-fast: false
      matrix: ${{ fromJSON(needs.plan.outputs.matrix) }}
    steps:
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      - name: Restore Lean dependencies
        id: dependency-cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Restore pool build
        id: cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
          restore-keys: |
            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Install Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: false

      - name: Install Mathlib cache
        id: mathlib-cache
        run: |
          if [ ! -d ".lake/packages/mathlib" ]; then
            ~/.elan/bin/lake exe cache get
          else
            echo "Mathlib already present from cache"
          fi

      - name: Build this shard's projects
        env:
          PROJECTS: ${{ matrix.projects }}
        run: |
          set -euo pipefail
          touch "$RUNNER_TEMP/build-stamp"
          modules=""
          # shellcheck disable=SC2086 # word-split the project list on purpose
          for project in $PROJECTS; do
            project_modules=$(git ls-files -- "LeanPool/$project.lean" "LeanPool/$project/" \
              | grep '\.lean$' \
              | sed -e 's/\.lean$//' -e 's#/#.#g' \
              | tr '\n' ' ')
            modules="$modules $project_modules"
          done
          # shellcheck disable=SC2086 # modules is a space-separated list on purpose
          ~/.elan/bin/lake build $modules 2>&1 | tee shard-build.log
          if grep -nE '(^|: )warning:' shard-build.log; then
            echo "::error::Lean build emitted warnings; fix them before merging."
            exit 1
          fi

      # Ship only what this build produced; unchanged (cache-replayed)
      # files stay out, so `finalize` can layer the shard outputs onto the
      # same restored cache without clobbering anything fresher.
      - name: Package new build outputs
        env:
          SHARD: ${{ matrix.shard }}
        run: |
          set -euo pipefail
          find .lake/build -type f -newer "$RUNNER_TEMP/build-stamp" \
            > "$RUNNER_TEMP/new-files.txt"
          echo "$(wc -l < "$RUNNER_TEMP/new-files.txt") new build files"
          if [ -s "$RUNNER_TEMP/new-files.txt" ]; then
            tar -czf "shard-oleans-$SHARD.tar.gz" -T "$RUNNER_TEMP/new-files.txt"
          fi

      - name: Upload build outputs
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: ci-oleans-${{ matrix.shard }}
          path: shard-oleans-*.tar.gz
          if-no-files-found: ignore
          retention-days: 1

  finalize:
    needs: [plan, shard]
    # Run even when a shard failed: merging what succeeded and building the
    # rest here still produces a complete build log and lint report for
    # debugging. The gate job is what enforces that every shard was green.
    if: >-
      !cancelled() && needs.plan.result == 'success' &&
      needs.plan.outputs.mode == 'sharded'
    runs-on: ubuntu-latest
    name: Assemble and lint
    permissions:
      contents: read
      actions: write
    steps:
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      - name: Restore Lean dependencies
        id: dependency-cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Restore pool build
        id: cache
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
          restore-keys: |
            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Install Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: false

      - name: Install uv
        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
        with:
          enable-cache: true

      - name: Check compiled artifact dependency tracking with pinned Lean
        if: needs.plan.outputs.dependency_tests == 'true'
        env:
          LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
        run: >-
          uv run --project python --group test pytest -q
          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
          -k 'test_lake_'

      - name: Install Mathlib cache
        id: mathlib-cache
        run: |
          if [ ! -d ".lake/packages/mathlib" ]; then
            ~/.elan/bin/lake exe cache get
          else
            echo "Mathlib already present from cache"
          fi

      # Recover PR outputs once; fresh shard files are layered on afterwards.
      - name: Reuse compiled files from this PR's successful runs
        if: github.event_name == 'pull_request' && steps.cache.outputs.cache-hit != 'true'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          PR_NUMBER: ${{ github.event.pull_request.number }}
          PR_BRANCH: ${{ github.head_ref }}
          PR_HEAD: ${{ github.event.pull_request.head.sha }}
          PR_BASE: ${{ github.event.pull_request.base.sha }}
          CURRENT_RUN: ${{ github.run_id }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.ci_pr_build
          --number "$PR_NUMBER" --branch "$PR_BRANCH"
          --head "$PR_HEAD" --base "$PR_BASE" --current-run "$CURRENT_RUN"

      - name: Download shard build outputs
        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
        with:
          pattern: ci-oleans-*
          merge-multiple: true

      - name: Merge shard build outputs
        run: |
          set -euo pipefail
          for archive in shard-oleans-*.tar.gz; do
            if [ -e "$archive" ]; then
              tar -xzf "$archive"
              rm "$archive"
            fi
          done

      - name: Check library indexes use the module system and are up to date
        run: |
          if ! ~/.elan/bin/lake exe mk_all --module --check; then
            echo "::error::Library indexes are out of date or missing module headers. Run 'lake exe mk_all --module' locally and commit the result."
            exit 1
          fi

      # With the shard outputs in place this is mostly cache replay; it
      # builds the root module and anything a shard missed or failed to
      # deliver, so the assembled pool is complete regardless.
      - name: Reuse successful queued PR builds
        if: github.event_name == 'merge_group'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BASE_SHA: ${{ github.event.merge_group.base_sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
          --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Build project
        id: compilation
        run: |
          set -euo pipefail
          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
          if grep -nE '(^|: )warning:' lean-build.log; then
            echo "::error::Lean build emitted warnings; fix them before merging."
            exit 1
          fi

      # Main publishes the shared full build. A minimal-verifier PR publishes
      # only its own projects; the verifier overlays them on the main cache.
      - name: Package build for documentation
        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
        env:
          BUILD_EVENT: ${{ github.event_name }}
          BASE_SHA: ${{ github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.pull_request.head.sha }}
        run: |
          if [ "$BUILD_EVENT" = pull_request ]; then
            PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack --base "$BASE_SHA" --head "$HEAD_SHA"
          else
            PYTHONPATH=python python3 -m lean_pool.ci_artifacts pack
          fi

      - name: Share build with documentation
        if: github.ref == 'refs/heads/main' || (github.event_name == 'pull_request' && needs.plan.outputs.minimal_build == 'true')
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lean-pool-build
          path: lean-pool-build.tar.zst
          if-no-files-found: error
          compression-level: 0
          retention-days: 1

      # Actions scopes PR caches to refs/pull/<n>/merge: updates to the same
      # PR can reuse receipts, while main and other PRs cannot read them.
      - name: Restore project validation
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/validation-cache/v1
          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
          restore-keys: |
            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Recover saved validation when caches were evicted
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BUILD_EVENT: ${{ github.event_name }}
          BUILD_HEAD: ${{ github.sha }}
        run: >-
          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
          --event "$BUILD_EVENT" --head "$BUILD_HEAD"

      - name: Install validation dependencies
        run: cd python && uv sync --locked

      - name: Reuse successful queued PR validation
        if: github.event_name == 'merge_group'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          BASE_SHA: ${{ github.event.merge_group.base_sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.queue_build
          --base "$BASE_SHA" --head "$HEAD_SHA" --receipts

      - name: Lint
        run: |
          cd python
          uv run python -m lean_pool.validation_cache lint --repo ..
          cd ..

      - name: Text style lint
        run: |
          ~/.elan/bin/lake exe lint-style LeanPool

      - name: Repository quality checks
        run: |
          cd python
          uv run python -m lean_pool.validation_cache quality --repo ..

      - name: Retain successful validation independently of build caches
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lean-validation-receipts
          path: .lake/validation-cache/v1/passes.json
          include-hidden-files: true
          if-no-files-found: error
          compression-level: 1
          retention-days: 14

      - name: Package PR project build for later rebases
        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
        continue-on-error: true
        env:
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Retain PR project build
        if: github.event_name == 'pull_request' || github.event_name == 'merge_group'
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: rebase-project-build
          path: rebase-project-build.tar.gz
          if-no-files-found: error
          compression-level: 0
          retention-days: 14

      - name: Save project validation
        # Successful receipts are tiny; retain PR results across registry rebases.
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/validation-cache/v1
          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}

      - name: Save Lean dependencies
        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Save pool build
        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}

  # Reuse the prior green project's compiled modules and current main's cache.
  # A missing artifact falls back to the full validation sequence in this job.
  rebase:
    needs: plan
    if: needs.plan.outputs.mode == 'rebase'
    runs-on: ubuntu-latest
    name: Check rebased root
    steps:
      - name: Checkout project
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
        with:
          fetch-depth: 0

      - name: Restore Lean dependencies
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: |
            ~/.elan
            .lake/packages
          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}

      - name: Restore current main build
        id: main-build
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/build
          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.base_build_revision }}
          restore-keys: |
            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Install uv
        uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
        with:
          enable-cache: true

      - name: Reuse newly merged projects while the main cache warms
        if: steps.main-build.outputs.cache-hit != 'true'
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          REPOSITORY: ${{ github.repository }}
          PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }}
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore-main
          --repository "$REPOSITORY" --head "$PREVIOUS_HEAD" --base "$BASE_SHA"

      - name: Restore previously validated PR modules
        id: project-build
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          RUN_ID: ${{ needs.plan.outputs.reuse_run_id }}
          PREVIOUS_HEAD: ${{ needs.plan.outputs.previous_head }}
          REPOSITORY: ${{ github.repository }}
        run: >-
          PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath restore
          --repository "$REPOSITORY" --run-id "$RUN_ID" --head "$PREVIOUS_HEAD"

      - name: Install Lean
        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
        with:
          auto-config: false
          use-github-cache: false
          use-mathlib-cache: false

      - name: Check compiled artifact dependency tracking with pinned Lean
        if: needs.plan.outputs.dependency_tests == 'true'
        env:
          LEAN_POOL_REQUIRE_TEST_TOOLCHAIN: '1'
        run: >-
          uv run --project python --group test pytest -q
          python/tests/test_ci_pr_build.py python/tests/test_indexes.py
          -k 'test_lake_'

      - name: Install Mathlib cache
        run: |
          if [ ! -d ".lake/packages/mathlib" ]; then
            ~/.elan/bin/lake exe cache get
          fi

      - name: Check generated index
        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath check-index

      - name: Build combined Lean root
        run: |
          set -euo pipefail
          ~/.elan/bin/lake build LeanPool 2>&1 | tee lean-build.log
          if grep -nE '(^|: )warning:' lean-build.log; then
            echo "::error::Lean build emitted warnings; fix them before merging."
            exit 1
          fi

      - name: Install validation dependencies
        run: cd python && uv sync --locked

      - name: Validate combined repository metadata
        if: steps.project-build.outcome == 'success'
        run: cd python && uv run python -m lean_pool.quality --repo .. --static-only

      - name: Restore validation cache for the combined checkout
        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
        with:
          path: .lake/validation-cache/v1
          key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
          restore-keys: |
            LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-

      - name: Carry saved checks through the verified rebase
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          PREVIOUS_RUN: ${{ needs.plan.outputs.reuse_run_id }}
          BUILD_HEAD: ${{ github.sha }}
        run: >-
          PYTHONPATH=python python3 -m lean_pool.ci_validation_artifacts
          --event pull_request --head "$BUILD_HEAD" --previous-run "$PREVIOUS_RUN"

      - name: Full validation when the prior artifact is unavailable
        if: steps.project-build.outcome != 'success'
        run: |
          set -euo pipefail
          (cd python && uv run python -m lean_pool.validation_cache lint --repo ..)
          ~/.elan/bin/lake exe lint-style LeanPool
          (cd python && uv run python -m lean_pool.validation_cache quality --repo ..)

      - name: Retain successful validation independently of build caches
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: lean-validation-receipts
          path: .lake/validation-cache/v1/passes.json
          include-hidden-files: true
          if-no-files-found: warn
          compression-level: 1
          retention-days: 14

      - name: Package PR project build for later rebases
        continue-on-error: true
        env:
          BASE_SHA: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
          HEAD_SHA: ${{ github.event.merge_group.head_sha || github.event.pull_request.head.sha }}
        run: PYTHONPATH=python uv run --project python --locked python -m lean_pool.rebase_fastpath pack --base "$BASE_SHA" --head "$HEAD_SHA"

      - name: Retain PR project build
        continue-on-error: true
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: rebase-project-build
          path: rebase-project-build.tar.gz
          if-no-files-found: error
          compression-level: 0
          retention-days: 14

  # Single overall verdict under the check name the one-job workflow used,
  # so nothing watching "Build project" needs to change.
  gate:
    needs: [plan, build, shard, finalize, rebase]
    if: always()
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Check outcome
        env:
          MODE: ${{ needs.plan.outputs.mode }}
          PLAN_RESULT: ${{ needs.plan.result }}
          BUILD_RESULT: ${{ needs.build.result }}
          SHARD_RESULT: ${{ needs.shard.result }}
          FINALIZE_RESULT: ${{ needs.finalize.result }}
          REBASE_RESULT: ${{ needs.rebase.result }}
        run: |
          set -euo pipefail
          echo "plan=$PLAN_RESULT mode=$MODE build=$BUILD_RESULT shard=$SHARD_RESULT finalize=$FINALIZE_RESULT"
          if [ "$PLAN_RESULT" != "success" ]; then
            echo "::error::Build planning failed."
            exit 1
          fi
          case "$MODE" in
            skip)
              echo "No Lean build inputs changed."
              ;;
            rebase)
              [ "$REBASE_RESULT" = "success" ] || { echo "::error::Rebase validation failed."; exit 1; }
              ;;
            single)
              [ "$BUILD_RESULT" = "success" ] || { echo "::error::Build failed."; exit 1; }
              ;;
            sharded)
              [ "$SHARD_RESULT" = "success" ] || { echo "::error::A build shard failed."; exit 1; }
              [ "$FINALIZE_RESULT" = "success" ] || { echo "::error::Assembly or linting failed."; exit 1; }
              ;;
            *)
              echo "::error::Unknown build mode: $MODE"
              exit 1
              ;;
          esac
          echo "CI passed in $MODE mode."