Vilin97 · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026 · Oct 10, 2026
diff --git a/.github/workflows/cache-maintenance.yml b/.github/workflows/cache-maintenance.yml
@@ -0,0 +1,28 @@
+name: Cache maintenance
+
+on:
+  schedule:
+    - cron: '43 * * * *'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  actions: write
+
+concurrency:
+  group: cache-maintenance
+  cancel-in-progress: false
+
+jobs:
+  prune:
+    runs-on: ubuntu-latest
+    name: Prune superseded main caches
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          persist-credentials: false
+      - name: Retain the newest cache in each known family
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+        run: PYTHONPATH=python python3 -m lean_pool.ci_cache prune --repository "$REPOSITORY"
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -15,6 +15,8 @@ on:
       - 'lean-toolchain'
       - 'docbuild/**'
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/documentation.py'
+      - 'python/lean_pool/indexes.py'
       - 'python/lean_pool/quality.py'
       - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
@@ -46,17 +48,57 @@ permissions:
   actions: read
 
 jobs:
+  scope:
+    runs-on: ubuntu-latest
+    outputs:
+      applicable: ${{ steps.scope.outputs.applicable }}
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - id: scope
+        env:
+          EVENT: ${{ github.event_name }}
+          BASE: ${{ github.event.merge_group.base_sha || github.event.pull_request.base.sha }}
+        run: |
+          set -euo pipefail
+          applicable=true
+          if [ "$EVENT" = merge_group ] || [ "$EVENT" = pull_request ]; then
+            applicable=false
+            if [ "$EVENT" = pull_request ]; then
+              files=$(git diff --name-only --no-renames "$BASE"...HEAD)
+            else
+              files=$(git diff --name-only --no-renames "$BASE"..HEAD)
+            fi
+            # Git may quote names containing Unicode or control characters.
+            if grep -Eq '^"?(docbuild/|lean-toolchain$|lakefile\.toml$|lake-manifest\.json$|python/lean_pool/(exposition/|documentation\.py$|indexes\.py$|quality\.py$|validation_cache\.py$|ci_artifacts\.py$|ci_cache\.py$|rebase_fastpath\.py$)|python/(pyproject\.toml|uv\.lock)$|scripts/exposition/|\.github/workflows/docs\.yml$)' <<< "$files"; then
+              applicable=true
+            fi
+          fi
+          echo "applicable=$applicable" >> "$GITHUB_OUTPUT"
   # Fail cheap consistency checks before either multi-hour documentation job
   # starts. In particular, a stale generated root should not spend runner time
   # building documentation that cannot be merged.
   preflight:
+    needs: scope
+    if: always() && (needs.scope.result != 'success' || needs.scope.outputs.applicable != 'false')
     runs-on: ubuntu-latest
     name: Documentation preflight
     outputs:
       build_revision: ${{ steps.build-identity.outputs.revision }}
       readme_only: ${{ steps.scope.outputs.readme_only }}
       rebase_only: ${{ steps.rebase.outputs.rebase_only }}
     steps:
+      - name: Require successful change classification
+        env:
+          SCOPE_RESULT: ${{ needs.scope.result }}
+          APPLICABLE: ${{ needs.scope.outputs.applicable }}
+        run: |
+          if [ "$SCOPE_RESULT" != success ] || [ "$APPLICABLE" != true ]; then
+            echo "::error::Change classification failed; required validation cannot be skipped."
+            exit 1
+          fi
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
         with:
@@ -84,7 +126,7 @@ jobs:
           set -euo pipefail
           readme_only=false
           if [ "$EVENT_NAME" = "pull_request" ]; then
-            files="$(git diff --name-only "$BASE_SHA"..."$HEAD_SHA")"
+            files="$(git diff --name-only --no-renames "$BASE_SHA"..."$HEAD_SHA")"
             if [ "$files" = "README.md" ]; then
               readme_only=true
             fi
@@ -275,17 +317,6 @@ jobs:
           path: .lake/exposition-cache/v1
           key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
 
-      - name: Prune old copies of project extraction cache
-        if: always() && steps.extraction-cache-save.outcome == 'success' && github.ref == 'refs/heads/main'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: ${{ steps.extraction-cache.outputs.cache-primary-key }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - name: Upload extraction timings and logs
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -419,17 +450,6 @@ jobs:
             .lake/packages/MD4Lean
           key: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
 
-      - name: Prune old copies of mathlib documentation checkpoint
-        if: steps.mathlib-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: DocsInfoMathlib-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
   build:
     needs:
       - preflight
@@ -562,17 +582,6 @@ jobs:
             .lake/packages/MD4Lean
           key: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }}
 
-      - name: Prune old copies of pool documentation checkpoint
-        if: steps.pool-doc-cache.outputs.cache-hit != 'true' && github.ref == 'refs/heads/main'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-${{ needs.preflight.outputs.build_revision }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - name: Build documentation
         run: cd docbuild && ~/.elan/bin/lake build LeanPool:docs
 

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
@@ -87,6 +87,7 @@ jobs:
       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 }}
@@ -145,16 +146,16 @@ jobs:
           : > "$changed_files"
           case "$EVENT_NAME" in
             merge_group)
-              git diff --name-only "$BASE_SHA"..HEAD > "$changed_files"
+              git diff --name-only --no-renames "$BASE_SHA"..HEAD > "$changed_files"
               ;;
             pull_request)
-              git diff --name-only "$BASE_SHA"...HEAD > "$changed_files"
+              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 "$BEFORE_SHA"..HEAD > "$changed_files"
+                git diff --name-only --no-renames "$BEFORE_SHA"..HEAD > "$changed_files"
               else
                 diff_available=false
               fi
@@ -168,6 +169,15 @@ jobs:
             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" \
@@ -242,6 +252,7 @@ jobs:
           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: >-
@@ -428,17 +439,6 @@ jobs:
           path: .lake/validation-cache/v1
           key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
-      - name: Prune old copies of project validation
-        if: success() && github.ref == 'refs/heads/main'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - 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
@@ -448,35 +448,13 @@ jobs:
             .lake/packages
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
-      - name: Prune old copies of lean dependencies
-        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - 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 }}
 
-      - name: Prune old copies of pool build
-        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
   shard:
     needs: plan
     if: needs.plan.outputs.mode == 'sharded'
@@ -624,6 +602,7 @@ jobs:
           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: >-
@@ -814,17 +793,6 @@ jobs:
           path: .lake/validation-cache/v1
           key: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
 
-      - name: Prune old copies of project validation
-        if: success() && github.ref == 'refs/heads/main'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanValidation-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - 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
@@ -834,17 +802,6 @@ jobs:
             .lake/packages
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
-      - name: Prune old copies of lean dependencies
-        if: always() && github.ref == 'refs/heads/main' && steps.mathlib-cache.outcome == 'success' && steps.dependency-cache.outputs.cache-hit != 'true'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
       - 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
@@ -854,17 +811,6 @@ jobs:
 
   # 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.
-      - name: Prune old copies of pool build
-        if: always() && github.ref == 'refs/heads/main' && steps.compilation.outcome == 'success' && steps.cache.outputs.cache-hit != 'true'
-        continue-on-error: true
-        env:
-          GH_TOKEN: ${{ github.token }}
-          REPOSITORY: ${{ github.repository }}
-          CACHE_KEY: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.plan.outputs.build_revision }}
-        run: >-
-          PYTHONPATH=python python3 -m lean_pool.ci_cache prune
-          --repository "$REPOSITORY" --key "$CACHE_KEY"
-
   rebase:
     needs: plan
     if: needs.plan.outputs.mode == 'rebase'
@@ -930,6 +876,7 @@ jobs:
           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: >-

diff --git a/.github/workflows/proof-profile-comment.yml b/.github/workflows/proof-profile-comment.yml
@@ -1,13 +1,8 @@
 name: Proof Profile Comment
 
-# Companion to the `Proof Profile` workflow. That workflow runs the PR's Lean
-# code to profile it, so it must run on the `pull_request` event — where a PR
-# from a fork only gets a read-only GITHUB_TOKEN and cannot post a comment.
-# This workflow fires when it finishes, runs in the base-repo context with a
-# writable token, and posts the already-rendered profile for every PR, fork or
-# not. It never checks out or runs PR code; it only downloads the pre-rendered
-# `proof-profile-comment` artifact and posts it, so the writable token is never
-# exposed to untrusted PR code.
+# Retries comment publication when an on-demand `Proof Profile` run could not
+# post directly. It only downloads the rendered artifact and never executes
+# PR code with its writable token.
 on:
   workflow_run:
     workflows: ["Proof Profile"]