Cache exposition extraction and reuse Lean CI builds for docs

.github/workflows/challenge-verify.yml

@@ -65,16 +65,22 @@ jobs:
       - name: Load tool pins
         run: cat scripts/challenge/pins.env | grep -E '^[A-Z0-9_]+=' >> "$GITHUB_ENV"
 
-      - name: Restore caches
+      - name: Restore Lean dependencies
+        id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+
+      - name: Restore 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 }}
           restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
       - name: Install Lean
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9

.github/workflows/docs.yml

@@ -13,6 +13,8 @@ on:
       - 'lean-toolchain'
       - 'docbuild/**'
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/ci_artifacts.py'
+      - 'scripts/exposition/**'
       - '.github/workflows/docs.yml'
   pull_request:
     branches:
@@ -32,6 +34,8 @@ on:
       - 'lean-toolchain'
       - 'docbuild/**'
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/ci_artifacts.py'
+      - 'scripts/exposition/**'
       - '.github/workflows/notice.yml'
       - '.github/workflows/docs.yml'
   workflow_dispatch:
@@ -106,21 +110,17 @@ jobs:
             exit 1
           fi
 
-      # This is deliberately identical to Lean Action CI's cache lookup (key,
-      # paths, and ordering). Documentation can therefore start from the
-      # root build that CI already produced instead of compiling the
-      # entire pool again under a separate cache namespace.
-      - name: Restore Lean build cache
+      # Preflight needs the toolchain and dependencies, not the pool build.
+      # Stable dependencies are shared with CI without a new copy per commit.
+      - name: Restore Lean dependencies
+        id: dependency-cache
         if: steps.scope.outputs.readme_only != 'true'
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
       - name: Install Lean
         if: steps.scope.outputs.readme_only != 'true'
@@ -154,29 +154,32 @@ jobs:
   # never saves it — Lean Action CI owns that cache, while the documentation
   # jobs own doc-gen's separate caches.
   exposition:
-    # On a cold toolchain boundary, Mathlib docInfo gives Lean Action CI time
-    # to seed the new root cache before this job restores it. Without that
-    # boundary, exposition's pool rebuild plus extraction approached six hours.
-    needs:
-      - preflight
-      - mathlib_doc_info
+    # Exposition consumes compiled Lean, not doc-gen's Mathlib SQLite data.
+    # Reuse the matching CI artifact directly instead of waiting for docInfo.
+    needs: preflight
     if: needs.preflight.outputs.readme_only != 'true'
     runs-on: ubuntu-latest
     name: Build exposition site
     steps:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
-      - name: Restore Lean build cache
+      - name: Restore Lean dependencies
+        id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+
+      - name: Restore 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 }}
           restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
       - name: Install Lean
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
@@ -196,9 +199,27 @@ jobs:
             exit 1
           fi
 
+      - name: Reuse matching Lean CI build
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
+          BUILD_EVENT: ${{ github.event_name }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore
+          --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+
       - name: Build pool
         run: ~/.elan/bin/lake build LeanPool
 
+      - name: Restore project extraction cache
+        id: extraction-cache
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/exposition-cache/v1
+          key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }}
+          restore-keys: |
+            Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-
+
       - name: Extract declarations
         # Per-project environments (see extract-all.sh); 2-way parallel to
         # stay inside the runner's memory.
@@ -209,6 +230,25 @@ jobs:
           ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh
           exposition-dump.jsonl exposition-commands.jsonl
 
+      - name: Save project extraction cache
+        if: steps.extraction-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/exposition-cache/v1
+          key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
+
+      - name: Upload extraction timings and logs
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: exposition-extraction-diagnostics
+          path: |
+            .lake/exposition-timings.json
+            .lake/exposition-cache/v1/**/extract.log
+            .lake/exposition-cache/v1/**/failed.log
+          include-hidden-files: true
+          retention-days: 7
+
       - name: Install uv
         uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
         with:
@@ -245,19 +285,17 @@ jobs:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
-      - name: Restore Lean build cache
+      - name: Restore Lean dependencies
+        id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
-          restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
 
-      # Only doc-gen's own state is cached here. Root oleans stay in the
-      # Lean Action cache above, so the two namespaces do not duplicate them.
+      # Mathlib's compiled artifacts come from the dependency cache; doc-gen's
+      # SQLite data and extra dependencies have their own checkpoint.
       - name: Restore Mathlib documentation checkpoint
         id: mathlib-doc-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
@@ -337,16 +375,22 @@ jobs:
       - name: Checkout project
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd
 
-      - name: Restore Lean build cache
+      - name: Restore Lean dependencies
+        id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+
+      - name: Restore 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 }}
           restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
       # Prefer the latest complete docInfo database from this compatibility
       # boundary. On a cold boundary, the preceding job has just produced the
@@ -398,6 +442,15 @@ jobs:
             exit 1
           fi
 
+      - name: Reuse matching Lean CI build
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
+          BUILD_EVENT: ${{ github.event_name }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore
+          --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+
       # This incrementally extends either a previous pool checkpoint or the
       # Mathlib checkpoint produced by the preceding job. doc-gen serializes
       # writes through one WAL database, so these targets intentionally share a
@@ -501,7 +554,7 @@ jobs:
             echo "deploy=true" >> "$GITHUB_OUTPUT"
           fi
 
-  # The two expensive sites build in parallel after the Mathlib checkpoint.
+  # The two expensive sites build independently after preflight.
   # Let the dependency graph join them instead of racing one job against a
   # polling timeout. If either build fails, no incomplete tree is deployed.
   deploy:

.github/workflows/exposition-verify.yml

@@ -15,6 +15,7 @@ on:
       - main
     paths:
       - 'python/lean_pool/exposition/**'
+      - 'python/lean_pool/ci_artifacts.py'
       - 'scripts/exposition/**'
       - '.github/workflows/exposition-verify.yml'
 
@@ -24,6 +25,7 @@ concurrency:
 
 permissions:
   contents: read
+  actions: read
 
 jobs:
   verify:
@@ -36,16 +38,22 @@ jobs:
       # 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.
-      - name: Restore Lean build cache
+      - name: Restore Lean dependencies
+        id: dependency-cache
         uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
         with:
           path: |
             ~/.elan
             .lake/packages
-            .lake/build
-          key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          key: LeanDependencies-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}
+
+      - name: Restore 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 }}
           restore-keys: |
-            Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-
+            LeanPoolBuild-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml') }}-
 
       - name: Install Lean
         uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
@@ -65,9 +73,27 @@ jobs:
             exit 1
           fi
 
+      - name: Reuse matching Lean CI build
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BUILD_HEAD: ${{ github.event.pull_request.head.sha || github.sha }}
+          BUILD_EVENT: ${{ github.event_name }}
+        run: >-
+          PYTHONPATH=python python3 -m lean_pool.ci_artifacts restore
+          --head "$BUILD_HEAD" --event "$BUILD_EVENT"
+
       - name: Build pool
         run: ~/.elan/bin/lake build LeanPool
 
+      - name: Restore project extraction cache
+        id: extraction-cache
+        uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/exposition-cache/v1
+          key: Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-${{ github.sha }}
+          restore-keys: |
+            Exposition-v1-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json', 'lakefile.toml', 'scripts/exposition/**', 'python/lean_pool/exposition/extract.py', 'python/lean_pool/exposition/source_text.py') }}-
+
       - name: Extract declarations
         env:
           LEAN_CMD: /home/runner/.elan/bin/lean
@@ -76,6 +102,25 @@ jobs:
           ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh
           exposition-dump.jsonl exposition-commands.jsonl
 
+      - name: Save project extraction cache
+        if: steps.extraction-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@27d5ce7f107fe9357f9df03efb73ab90386fccae
+        with:
+          path: .lake/exposition-cache/v1
+          key: ${{ steps.extraction-cache.outputs.cache-primary-key }}
+
+      - name: Upload extraction timings and logs
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: exposition-extraction-diagnostics
+          path: |
+            .lake/exposition-timings.json
+            .lake/exposition-cache/v1/**/extract.log
+            .lake/exposition-cache/v1/**/failed.log
+          include-hidden-files: true
+          retention-days: 7
+
       - name: Install uv
         uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff
         with: