Speed up CI and preserve completed checks through PR updates and merges

.github/workflows/auto-rebase.yml

@@ -27,6 +27,13 @@ on:
       - 'LeanPool/**'
       - 'LeanPool.lean'
   workflow_dispatch:
+  pull_request_target:
+    types: [ready_for_review]
+  workflow_run:
+    workflows: [Lean Action CI, Documentation, Exposition Verify]
+    types: [completed]
+  schedule:
+    - cron: '*/15 * * * *'
 
 concurrency:
   # Serialised: two runs rebasing the same PR would race on its branch.
@@ -45,21 +52,22 @@ jobs:
       pulls: ${{ steps.list.outputs.pulls }}
       any: ${{ steps.list.outputs.any }}
     steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
+        with:
+          ref: main
+          persist-credentials: false
+
       - name: Collect open pull requests
         id: list
         env:
           GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           REPO: ${{ github.repository }}
+          TARGET_PR: ${{ github.event.pull_request.number || github.event.workflow_run.pull_requests[0].number || 0 }}
         run: |
           set -euo pipefail
           pulls="$(gh pr list --repo "$REPO" --state open --limit 100 \
-            --json number,headRefName,headRepository,headRepositoryOwner,isCrossRepository,labels \
-            --jq '[.[]
-                  | select([.labels[].name] | index("needs-manual-rebase") | not)
-                  | select(.headRefName | startswith("bump/") | not)
-                  | {number, branch: .headRefName,
-                     repo: "\(.headRepositoryOwner.login)/\(.headRepository.name)",
-                     fork: .isCrossRepository}]')"
+            --json number,headRefName,headRefOid,headRepository,headRepositoryOwner,isCrossRepository,labels,isDraft,baseRefName,statusCheckRollup \
+            | PYTHONPATH=python python3 -m lean_pool.rebase_queue select --number "$TARGET_PR")"
           echo "pulls=$pulls" >> "$GITHUB_OUTPUT"
           if [ "$(echo "$pulls" | python3 -c 'import json,sys; print(len(json.load(sys.stdin)))')" = "0" ]; then
             echo "any=false" >> "$GITHUB_OUTPUT"
@@ -82,17 +90,49 @@ jobs:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
         with:
           fetch-depth: 0
+          ref: main
           token: ${{ secrets.REBASE_TOKEN || secrets.GITHUB_TOKEN }}
 
+      - name: Check this content branch needs updating
+        id: scope
+        env:
+          NUMBER: ${{ matrix.pull.number }}
+          BRANCH: ${{ matrix.pull.branch }}
+          EXPECTED_HEAD: ${{ matrix.pull.head }}
+          HEAD_REPO: ${{ matrix.pull.repo }}
+          TOKEN: ${{ secrets.REBASE_TOKEN || secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          cp python/lean_pool/rebase_queue.py "$RUNNER_TEMP/rebase-queue.py"
+          git remote add head "https://x-access-token:$TOKEN@github.com/$HEAD_REPO"
+          git fetch head "$BRANCH"
+          git fetch origin main
+          git checkout -B "pr-$NUMBER" "head/$BRANCH"
+          if [ "$(git rev-parse HEAD)" != "$EXPECTED_HEAD" ]; then
+            echo "Author updated the branch; defer until its checks finish."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          elif git merge-base --is-ancestor origin/main HEAD; then
+            echo "Already includes current main."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          elif python3 "$RUNNER_TEMP/rebase-queue.py" content; then
+            echo "needed=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "Infrastructure PR; preserve its current validation run."
+            echo "needed=false" >> "$GITHUB_OUTPUT"
+          fi
+
       - uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
+        if: steps.scope.outputs.needed == 'true'
         with:
           enable-cache: true
 
       - name: Install Python tooling
+        if: steps.scope.outputs.needed == 'true'
         run: cd python && uv sync --locked
 
       - name: Check we can push to this branch
         id: capable
+        if: steps.scope.outputs.needed == 'true'
         env:
           FORK: ${{ matrix.pull.fork }}
           HAS_TOKEN: ${{ secrets.REBASE_TOKEN != '' }}
@@ -118,11 +158,6 @@ jobs:
           git config user.name "github-actions[bot]"
           git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
 
-          remote="https://x-access-token:$TOKEN@github.com/$HEAD_REPO"
-          git remote add head "$remote"
-          git fetch head "$BRANCH"
-          git checkout -B "pr-$NUMBER" "head/$BRANCH"
-
           if git merge --no-edit origin/main; then
             echo "Merged cleanly."
             if git diff --quiet "head/$BRANCH" HEAD; then
@@ -179,7 +214,17 @@ jobs:
         env:
           NUMBER: ${{ matrix.pull.number }}
           BRANCH: ${{ matrix.pull.branch }}
-        run: git push head "pr-$NUMBER:$BRANCH"
+          EXPECTED_HEAD: ${{ matrix.pull.head }}
+          REPO: ${{ github.repository }}
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          if gh pr view "$NUMBER" --repo "$REPO" --json headRefOid,isDraft,statusCheckRollup \
+            | python3 "$RUNNER_TEMP/rebase-queue.py" can-push --head "$EXPECTED_HEAD"; then
+            git push head "pr-$NUMBER:$BRANCH"
+          else
+            echo "Branch or checks changed; defer this update."
+          fi
 
       - name: Flag PRs that need a human
         if: steps.rebase.outputs.result == 'manual' || steps.capable.outputs.ok == 'false'

.github/workflows/docs.yml

@@ -15,6 +15,7 @@ on:
       - 'python/lean_pool/quality.py'
       - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
+      - 'python/lean_pool/ci_cache.py'
       - 'python/lean_pool/rebase_fastpath.py'
       - 'scripts/exposition/**'
       - '.github/workflows/docs.yml'
@@ -38,6 +39,7 @@ on:
       - 'python/lean_pool/quality.py'
       - 'python/lean_pool/validation_cache.py'
       - 'python/lean_pool/ci_artifacts.py'
+      - 'python/lean_pool/ci_cache.py'
       - 'python/lean_pool/rebase_fastpath.py'
       - 'scripts/exposition/**'
       - '.github/workflows/notice.yml'
@@ -70,6 +72,7 @@ jobs:
     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:
@@ -78,6 +81,13 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: Identify compiled Lean sources
+        id: build-identity
+        run: |
+          set -euo pipefail
+          revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)
+          echo "revision=$revision" >> "$GITHUB_OUTPUT"
+
       - name: Detect README-only change
         id: scope
         env:
@@ -194,6 +204,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build exposition site
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -208,10 +221,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.preflight.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -234,6 +248,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
@@ -271,6 +286,17 @@ jobs:
           path: .lake/exposition-cache/v1
           key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
 
+      - name: Prune old copies of project extraction cache
+        if: steps.extraction-cache.outputs.cache-hit != 'true' && 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
@@ -318,6 +344,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build Mathlib documentation data
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -401,6 +430,17 @@ 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
@@ -411,6 +451,9 @@ jobs:
        (github.event_name == 'workflow_dispatch' && inputs.preview))
     runs-on: ubuntu-latest
     name: Build doc-gen4 site
+    permissions:
+      contents: read
+      actions: write
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
@@ -425,10 +468,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ needs.preflight.outputs.build_revision }}
           restore-keys: |
             LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
@@ -446,7 +490,7 @@ jobs:
             .lake/packages/UnicodeBasic
             .lake/packages/BibtexQuery
             .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') }}-${{ github.sha }}
+          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 }}
           restore-keys: |
             DocsInfo-v3-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lakefile.toml', 'lake-manifest.json', 'docbuild/lean-toolchain', 'docbuild/lakefile.toml', 'docbuild/lake-manifest.json') }}-
 
@@ -483,6 +527,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
@@ -526,7 +571,18 @@ jobs:
             .lake/packages/UnicodeBasic
             .lake/packages/BibtexQuery
             .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') }}-${{ github.sha }}
+          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

.github/workflows/exposition-verify.yml

@@ -35,6 +35,10 @@ jobs:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
+      - name: Identify compiled Lean sources
+        id: build-identity
+        run: echo "revision=$(PYTHONPATH=python python3 -m lean_pool.ci_cache revision)" >> "$GITHUB_OUTPUT"
+
       # Match Lean Action CI's cache lookup exactly. This workflow only needs
       # compiled Lean artifacts; restoring doc-gen output here used to make a
       # broad fallback pull an incompatible cache after every toolchain bump.
@@ -48,10 +52,11 @@ jobs:
           key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Restore pool build
+        id: pool-build
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: .lake/build
-          key: LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-${{ github.sha }}
+          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') }}-
 
@@ -74,6 +79,7 @@ jobs:
           fi
 
       - name: Reuse matching Lean CI build
+        if: steps.pool-build.outputs.cache-hit != 'true' && github.event_name != 'pull_request'
         env:
           GH_TOKEN: ${{ github.token }}
           BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}