diff --git a/.github/workflows/cache-restoration.yml b/.github/workflows/cache-restoration.yml
index a66fcf1d2..0ad778661 100644
--- a/.github/workflows/cache-restoration.yml
+++ b/.github/workflows/cache-restoration.yml
@@ -4,26 +4,41 @@ on:
   pull_request:
     paths:
       - scripts/fetch_dependency_caches.sh
+      - scripts/fetch_dependency_caches.py
+      - scripts/dependency_imports.lean
       - scripts/lake_cache_curl.py
       - tests/python/test_lake_cache_*.py
       - tests/python/test_fetch_dependency_caches.py
       - .github/workflows/cache-restoration.yml
       - lean-toolchain
+      - supported-toolchains.json
+      - toolchains/**
+      - scripts/prepare_toolchain.py
   push:
     branches: [main]
     paths:
       - scripts/fetch_dependency_caches.sh
+      - scripts/fetch_dependency_caches.py
+      - scripts/dependency_imports.lean
       - scripts/lake_cache_curl.py
       - tests/python/test_lake_cache_*.py
       - tests/python/test_fetch_dependency_caches.py
       - .github/workflows/cache-restoration.yml
       - lean-toolchain
+      - supported-toolchains.json
+      - toolchains/**
+      - scripts/prepare_toolchain.py
 
 permissions:
   contents: read
 
 jobs:
-  restore:
+  restore_toolchains:
+    name: restore (${{ matrix.configuration }})
+    strategy:
+      fail-fast: false
+      matrix:
+        configuration: [rc, stable]
     runs-on: ubuntu-24.04
     timeout-minutes: 10
     steps:
@@ -31,6 +46,9 @@ jobs:
         with:
           persist-credentials: false
 
+      - name: Select benchmark configuration
+        run: python scripts/prepare_toolchain.py "${{ matrix.configuration }}" --apply
+
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
         with:
           build: false
@@ -46,3 +64,14 @@ jobs:
           export ELAN_TOOLCHAIN="$(cat lean-toolchain)"
           python -m unittest discover -v -s tests/python -p 'test_lake_cache_*.py'
           python -m unittest discover -v -s tests/python -p test_fetch_dependency_caches.py
+
+  restore:
+    if: always()
+    needs: restore_toolchains
+    runs-on: ubuntu-24.04
+    timeout-minutes: 2
+    steps:
+      - name: Require both toolchain cache checks
+        env:
+          RESULT: ${{ needs.restore_toolchains.result }}
+        run: test "$RESULT" = success
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 771873099..c788bbd44 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -18,7 +18,7 @@ jobs:
   classify:
     name: Classify changes
     runs-on: ubuntu-latest
-    timeout-minutes: 5
+    timeout-minutes: 15
     outputs:
       source_changed: ${{ steps.changes.outputs.source_changed }}
       generated_changed: ${{ steps.changes.outputs.generated_changed }}
@@ -29,6 +29,19 @@ jobs:
       selected_modules: ${{ steps.changes.outputs.selected_modules }}
       matrix: ${{ steps.changes.outputs.matrix }}
     steps:
+      - name: Free up disk space
+        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
+        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
+        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
+        with:
+          tool-cache: false
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
       # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
@@ -44,7 +57,10 @@ jobs:
       # a pin they reject breaks every server-dispatched evaluation while this
       # repository's CI stays green (v4.35.0-rc3, 2026-09-30 to 2026-10-07).
       - name: Check the pipeline accepts the pinned toolchain
-        run: python scripts/check_pipeline_toolchain_contract.py
+        run: |
+          python scripts/check_pipeline_toolchain_contract.py
+          python scripts/check_pipeline_toolchain_contract.py \
+            --toolchain-file toolchains/v4.35.0/lean-toolchain
 
       # Install the pinned Lean toolchain without building the project. The
       # dependency selector consumes a graph produced by Lean's header parser;
@@ -60,9 +76,9 @@ jobs:
       - name: Export Lean import graph
         run: |
           set -euo pipefail
-          mkdir -p .ci
-          lake build EvalTools.CIImportGraph
-          lake env lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json
+          mkdir -p .ci/EvalTools
+          lean -o .ci/EvalTools/ProblemSources.olean EvalTools/ProblemSources.lean
+          LEAN_PATH="$PWD/.ci" lean --run EvalTools/CIImportGraph.lean > .ci/import-graph.json
 
       - name: Select affected catalog problems
         id: changes
@@ -105,10 +121,17 @@ jobs:
           fetch-depth: 0
           persist-credentials: false
 
+      - name: Prepare solution-only package metadata
+        run: python scripts/prepare_ci_dependencies.py
+
       # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
         with:
           use-mathlib-cache: true
+          # Keep the CI-only sparse package checkouts intact. Published
+          # Mathlib and TauCeti caches supply artifacts without restoring a
+          # previous job's multi-gigabyte source/package tree over them.
+          use-github-cache: false
           # Nothing here needs the whole library built, and building it would
           # compile TauCeti; the catalog shards build problem modules from its
           # cache.
@@ -176,12 +199,16 @@ jobs:
       - name: Run Python unit tests
         run: python -m unittest discover -s tests/python -p 'test_*.py'
 
-  security:
-    name: Security and scoring smoke tests
+  security_toolchains:
+    name: Security and scoring smoke tests (${{ matrix.configuration }})
     needs: classify
     if: needs.classify.outputs.run_checks == 'true'
     runs-on: ubuntu-latest
     timeout-minutes: 60
+    strategy:
+      fail-fast: false
+      matrix:
+        configuration: [rc, stable]
     steps:
       - name: Free up disk space
         # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
@@ -202,10 +229,20 @@ jobs:
           fetch-depth: 0
           persist-credentials: false
 
+      - name: Select benchmark configuration
+        run: python scripts/prepare_toolchain.py "${{ matrix.configuration }}" --apply
+
+      - name: Prepare solution-only package metadata
+        run: python scripts/prepare_ci_dependencies.py
+
       # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
         with:
           use-mathlib-cache: true
+          # Keep the CI-only sparse package checkouts intact. Published
+          # Mathlib and TauCeti caches supply artifacts without restoring a
+          # previous job's multi-gigabyte source/package tree over them.
+          use-github-cache: false
           # Nothing here needs the whole library built, and building it would
           # compile TauCeti; the catalog shards build problem modules from its
           # cache.
@@ -245,6 +282,19 @@ jobs:
       - name: Run eval workflow smoke test
         run: lake exe lean-eval check-eval-workflow
 
+  security:
+    name: Security and scoring smoke tests
+    if: always()
+    needs: security_toolchains
+    runs-on: ubuntu-latest
+    timeout-minutes: 2
+    steps:
+      - name: Require both toolchain sandbox and scoring checks
+        env:
+          RESULT: ${{ needs.security_toolchains.result }}
+        run: |
+          case "$RESULT" in success|skipped) ;; *) exit 1 ;; esac
+
   catalog:
     name: Catalog validation (shard ${{ matrix.shard }}/${{ matrix.shard_count }})
     needs: classify
@@ -274,17 +324,27 @@ jobs:
           fetch-depth: 0
           persist-credentials: false
 
+      - name: Prepare solution-only package metadata
+        run: python scripts/prepare_ci_dependencies.py
+
       # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
         with:
           use-mathlib-cache: true
+          # Keep the CI-only sparse package checkouts intact. Published
+          # Mathlib and TauCeti caches supply artifacts without restoring a
+          # previous job's multi-gigabyte source/package tree over them.
+          use-github-cache: false
           build: false
           test: false
           lint: false
 
-      - name: Fetch TauCeti's build cache
-        # Problem modules that import TauCeti download its published oleans
-        # instead of compiling it; see scripts/fetch_dependency_caches.sh.
+      - name: Fetch imported dependency build caches
+        env:
+          STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }}
+          STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }}
+        # Imported large libraries download their published oleans
+        # without compiling on a cache miss; see scripts/fetch_dependency_caches.sh.
         run: bash scripts/fetch_dependency_caches.sh --restore .
 
       - name: Clear cached problem-module artifacts
@@ -371,22 +431,118 @@ jobs:
           if-no-files-found: error
           retention-days: 1
 
+  stable_catalog:
+    name: Stable catalog compilation (shard ${{ matrix.shard }}/${{ matrix.shard_count }})
+    needs: classify
+    if: needs.classify.outputs.run_catalog == 'true'
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    strategy:
+      fail-fast: false
+      matrix: ${{ fromJSON(needs.classify.outputs.matrix) }}
+    steps:
+      - name: Free up disk space
+        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
+        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
+        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
+        with:
+          tool-cache: false
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
+      # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+
+      - name: Select stable toolchain and dependency pins
+        run: python scripts/prepare_toolchain.py stable --apply
+
+      - name: Prepare solution-only package metadata
+        run: python scripts/prepare_ci_dependencies.py
+
+      # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
+        with:
+          use-mathlib-cache: true
+          # Keep the CI-only sparse package checkouts intact. Published
+          # Mathlib and TauCeti caches supply artifacts without restoring a
+          # previous job's multi-gigabyte source/package tree over them.
+          use-github-cache: false
+          build: false
+          test: false
+          lint: false
+
+      - name: Fetch imported dependency build caches
+        env:
+          STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }}
+          STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }}
+        # Imported large libraries download their published oleans
+        # without compiling on a cache miss; see scripts/fetch_dependency_caches.sh.
+        run: bash scripts/fetch_dependency_caches.sh --restore .
+
+      - name: Clear cached problem-module artifacts
+        run: |
+          set -euo pipefail
+          artifact_dir=.lake/build/lib/lean/LeanEval
+          if [ -d "$artifact_dir" ]; then
+            find "$artifact_dir" \( -type f -o -type l \) -delete
+          fi
+
+      - name: Build problem modules without warnings
+        env:
+          MODULES: ${{ matrix.modules }}
+          SHARD_INDEX: ${{ matrix.shard }}
+        run: |
+          set -euo pipefail
+          IFS=',' read -r -a modules <<< "$MODULES"
+          module_args=()
+          for module in "${modules[@]}"; do
+            module_args+=(--module "$module")
+          done
+          lake exe lean-eval check-problem-build "${module_args[@]}"
+
   catalog_inventory:
     name: Manifest inventory aggregate
     needs: [classify, catalog]
     if: needs.classify.outputs.run_catalog == 'true'
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    timeout-minutes: 30
     steps:
+      - name: Free up disk space
+        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
+        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
+        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
+        with:
+          tool-cache: false
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
       # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
           persist-credentials: false
 
+      - name: Prepare solution-only package metadata
+        run: python scripts/prepare_ci_dependencies.py
+
       # leanprover/lean-action pinned to 38fbc41a (= refs/tags/v1.5.0, also v1 HEAD as of 2026-05-04).
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9
         with:
           use-mathlib-cache: true
+          # Keep the CI-only sparse package checkouts intact. Published
+          # Mathlib and TauCeti caches supply artifacts without restoring a
+          # previous job's multi-gigabyte source/package tree over them.
+          use-github-cache: false
           build: false
           test: false
           lint: false
@@ -417,7 +573,7 @@ jobs:
   verify:
     name: verify
     if: always()
-    needs: [classify, checks, security, catalog, catalog_inventory]
+    needs: [classify, checks, security, catalog, stable_catalog, catalog_inventory]
     runs-on: ubuntu-latest
     timeout-minutes: 2
     steps:
@@ -427,11 +583,12 @@ jobs:
           CHECKS_RESULT: ${{ needs.checks.result }}
           SECURITY_RESULT: ${{ needs.security.result }}
           CATALOG_RESULT: ${{ needs.catalog.result }}
+          STABLE_CATALOG_RESULT: ${{ needs.stable_catalog.result }}
           CATALOG_INVENTORY_RESULT: ${{ needs.catalog_inventory.result }}
         run: |
           set -euo pipefail
           for result in "$CLASSIFY_RESULT" "$CHECKS_RESULT" \
-              "$SECURITY_RESULT" "$CATALOG_RESULT" \
+              "$SECURITY_RESULT" "$CATALOG_RESULT" "$STABLE_CATALOG_RESULT" \
               "$CATALOG_INVENTORY_RESULT"; do
             if [ "$result" != success ] && [ "$result" != skipped ]; then
               echo "A required CI branch ended with: $result" >&2
diff --git a/.github/workflows/regenerate-main.yml b/.github/workflows/regenerate-main.yml
index ef5678a2d..e0d14ef2c 100644
--- a/.github/workflows/regenerate-main.yml
+++ b/.github/workflows/regenerate-main.yml
@@ -27,6 +27,19 @@ jobs:
   regenerate:
     runs-on: ubuntu-latest
     steps:
+      - name: Free up disk space
+        # jlumbroso/free-disk-space pinned to 54081f13 (= refs/tags/v1.3.1, also main HEAD as of 2026-05-04).
+        # Bump procedure: SECURITY.md > "Bumping pinned dependencies".
+        uses: jlumbroso/free-disk-space@54081f138730dfa15788a46383842cd2f914a1be
+        with:
+          tool-cache: false
+          android: true
+          dotnet: true
+          haskell: true
+          large-packages: true
+          docker-images: true
+          swap-storage: true
+
       # actions/checkout pinned to 3d3c42e5 (= refs/tags/v7.0.1 as of 2026-07-30).
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
         with:
@@ -47,6 +60,9 @@ jobs:
           lint: false
 
       - name: Regenerate against a stable main
+        env:
+          STACKS_ARTIFACT_ENDPOINT: ${{ vars.STACKS_ARTIFACT_ENDPOINT }}
+          STACKS_REVISION_ENDPOINT: ${{ vars.STACKS_REVISION_ENDPOINT }}
         # A merge can land during the hour-long full-catalog generation. Repeat
         # from the new main instead of rebasing stale generated output over it.
         # Three attempts bound runner use during an unusually busy merge burst.
@@ -57,8 +73,8 @@ jobs:
             git fetch origin main
             git reset --hard origin/main
             git clean -ffd generated/
-            # Problem modules that import TauCeti restore its published oleans
-            # instead of compiling it, at the pins of this checkout; see
+            # Imported large libraries restore their published oleans
+            # without compiling on a cache miss, at the pins of this checkout; see
             # scripts/fetch_dependency_caches.sh.
             # Check out the dependencies this revision pins before comparing
             # them, and drop the previous attempt's cache settings.
diff --git a/EvalTools/CIImportGraph.lean b/EvalTools/CIImportGraph.lean
index 2b10c9f3f..cb677b03e 100644
--- a/EvalTools/CIImportGraph.lean
+++ b/EvalTools/CIImportGraph.lean
@@ -1,4 +1,4 @@
-import EvalTools.ModuleCoverage
+import EvalTools.ProblemSources
 
 open Lean
 
diff --git a/EvalTools/ModuleCoverage.lean b/EvalTools/ModuleCoverage.lean
index 0666b70f0..342e96a82 100644
--- a/EvalTools/ModuleCoverage.lean
+++ b/EvalTools/ModuleCoverage.lean
@@ -1,4 +1,4 @@
-import Lean
+import EvalTools.ProblemSources
 import EvalTools.Markers
 
 open Lean
@@ -9,26 +9,6 @@ open LeanEvalGenerator.Core
 
 set_option autoImplicit false
 
-/-- Directory holding the trusted problem sources, relative to the repository
-root. Its module prefix is the directory name. -/
-def problemSourceRelativePath : System.FilePath := "LeanEval"
-
-/-- A `.lean` file under `LeanEval/`, together with the modules its header
-imports.
-
-Module identity is a `Name`, not a string: `LeanEval/Foo/Bar.lean` is
-`LeanEval.Foo.Bar` while `LeanEval/Foo.Bar.lean` is `LeanEval.«Foo.Bar»`, and
-flattening either to text would conflate two distinct files. -/
-structure ProblemSourceModule where
-  /-- Fully qualified module name, for example
-  `LeanEval.Geometry.JacobianChallenge`. -/
-  name : Name
-  /-- Path of the file, relative to the repository root. -/
-  path : String
-  /-- The modules named in the file's `import` header. -/
-  imports : Array Name
-  deriving Inhabited, Repr
-
 private def sourcesByName (sources : Array ProblemSourceModule) :
     Std.HashMap Name ProblemSourceModule :=
   sources.foldl (fun m source => m.insert source.name source) ∅
@@ -55,45 +35,6 @@ def unreachableModules (sources : Array ProblemSourceModule) (roots : Array Name
   sources.filterMap fun source =>
     if reached.contains source.name then none else some source.name
 
-/-- Recursively collect the `.lean` files under `dir`, reading each header for
-its imports. `relDir` and `modulePrefix` describe `dir` itself. -/
-private partial def collectSourceModules (dir : System.FilePath) (relDir : String)
-    (modulePrefix : Name) : IO (Array ProblemSourceModule) := do
-  let entries := (← dir.readDir).qsort fun a b => a.fileName < b.fileName
-  let mut out : Array ProblemSourceModule := #[]
-  for entry in entries do
-    let relPath := s!"{relDir}/{entry.fileName}"
-    -- `symlinkMetadata` rather than `isDir`: the latter follows links, so a
-    -- directory symlink could duplicate a subtree under a second module prefix,
-    -- or point at an ancestor and recurse forever.
-    match (← entry.path.symlinkMetadata).type with
-    | .symlink =>
-        throw <| IO.userError
-          s!"`{relPath}` is a symbolic link. Problem sources must be regular files and \
-             directories, so that a file's path determines its module name."
-    | .dir =>
-        out := out ++ (← collectSourceModules entry.path relPath (modulePrefix.str entry.fileName))
-    | _ =>
-        if entry.path.extension == some "lean" then
-          let stem := (entry.fileName.dropEnd 5).toString
-          let header ← parseImports' (← IO.FS.readFile entry.path) entry.path.toString
-          out := out.push
-            { name := modulePrefix.str stem
-              path := relPath
-              imports := header.imports.map (·.module) }
-  return out
-
-/-- Load every source module under `LeanEval/`, using Lean's own module-header
-parser to identify imports. This is shared by module-coverage validation and
-the CI dependency selector so they cannot disagree about Lean import syntax. -/
-def loadProblemSourceModules (root : System.FilePath) : IO (Array ProblemSourceModule) := do
-  let sourceRoot := root / problemSourceRelativePath
-  unless ← sourceRoot.isDir do
-    throw <| IO.userError
-      s!"Problem source directory `{sourceRoot}` does not exist or is not a directory."
-  let prefixName := problemSourceRelativePath.toString
-  collectSourceModules sourceRoot prefixName (.str .anonymous prefixName)
-
 /-- Fail unless every `.lean` file under `LeanEval/` is reachable from the
 manifest: either named by some entry's `module` field, or imported (directly or
 transitively) by a module that is.
diff --git a/EvalTools/ProblemSources.lean b/EvalTools/ProblemSources.lean
new file mode 100644
index 000000000..da4f11491
--- /dev/null
+++ b/EvalTools/ProblemSources.lean
@@ -0,0 +1,71 @@
+import Lean
+
+open Lean
+
+namespace EvalTools
+
+set_option autoImplicit false
+
+/-- Directory holding the trusted problem sources, relative to the repository
+root. Its module prefix is the directory name. -/
+def problemSourceRelativePath : System.FilePath := "LeanEval"
+
+/-- A `.lean` file under `LeanEval/`, together with the modules its header
+imports.
+
+Module identity is a `Name`, not a string: `LeanEval/Foo/Bar.lean` is
+`LeanEval.Foo.Bar` while `LeanEval/Foo.Bar.lean` is `LeanEval.«Foo.Bar»`, and
+flattening either to text would conflate two distinct files. -/
+structure ProblemSourceModule where
+  /-- Fully qualified module name, for example
+  `LeanEval.Geometry.JacobianChallenge`. -/
+  name : Name
+  /-- Path of the file, relative to the repository root. -/
+  path : String
+  /-- The modules named in the file's `import` header. -/
+  imports : Array Name
+  deriving Inhabited, Repr
+
+/-- Recursively collect the `.lean` files under `dir`, reading each header for
+its imports. `relDir` and `modulePrefix` describe `dir` itself. -/
+private partial def collectSourceModules (dir : System.FilePath) (relDir : String)
+    (modulePrefix : Name) : IO (Array ProblemSourceModule) := do
+  let entries := (← dir.readDir).qsort fun a b => a.fileName < b.fileName
+  let mut out : Array ProblemSourceModule := #[]
+  for entry in entries do
+    let relPath := s!"{relDir}/{entry.fileName}"
+    -- `symlinkMetadata` rather than `isDir`: the latter follows links, so a
+    -- directory symlink could duplicate a subtree under a second module prefix,
+    -- or point at an ancestor and recurse forever.
+    match (← entry.path.symlinkMetadata).type with
+    | .symlink =>
+        throw <| IO.userError
+          s!"`{relPath}` is a symbolic link. Problem sources must be regular files and \
+             directories, so that a file's path determines its module name."
+    | .dir =>
+        out := out ++ (← collectSourceModules entry.path relPath (modulePrefix.str entry.fileName))
+    | _ =>
+        if entry.path.extension == some "lean" then
+          let stem := (entry.fileName.dropEnd 5).toString
+          let (header, _, messages) ← Lean.Elab.parseImports (← IO.FS.readFile entry.path)
+            entry.path.toString
+          if messages.hasErrors then
+            throw <| IO.userError s!"Invalid import header in {relPath}: {← messages.toList.toArray.mapM (·.toString)}"
+          out := out.push
+            { name := modulePrefix.str stem
+              path := relPath
+              imports := header.map (·.module) }
+  return out
+
+/-- Load every source module under `LeanEval/`, using Lean's own module-header
+parser to identify imports. This is shared by module-coverage validation and
+the CI dependency selector so they cannot disagree about Lean import syntax. -/
+def loadProblemSourceModules (root : System.FilePath) : IO (Array ProblemSourceModule) := do
+  let sourceRoot := root / problemSourceRelativePath
+  unless ← sourceRoot.isDir do
+    throw <| IO.userError
+      s!"Problem source directory `{sourceRoot}` does not exist or is not a directory."
+  let prefixName := problemSourceRelativePath.toString
+  collectSourceModules sourceRoot prefixName (.str .anonymous prefixName)
+
+end EvalTools
diff --git a/LeanEval/AlgebraicGeometry/Bezout.lean b/LeanEval/AlgebraicGeometry/Bezout.lean
index 606701a0f..eaef7dfe1 100644
--- a/LeanEval/AlgebraicGeometry/Bezout.lean
+++ b/LeanEval/AlgebraicGeometry/Bezout.lean
@@ -43,11 +43,11 @@ def vanishingSet {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) :
 
 /-- A chosen index `i : Fin (n+1)` with `p.rep i ≠ 0`. -/
 noncomputable def chartIndex {n : ℕ} (p : ProjSpace K n) : Fin (n + 1) :=
-  Classical.choose (Function.ne_iff.mp p.rep_nonzero)
+  Classical.choose (Function.ne_iff.mp p.out.property)
 
 lemma chartIndex_rep_ne_zero {n : ℕ} (p : ProjSpace K n) :
     Projectivization.rep p (chartIndex p) ≠ 0 :=
-  Classical.choose_spec (Function.ne_iff.mp p.rep_nonzero)
+  Classical.choose_spec (Function.ne_iff.mp p.out.property)
 
 /-- Affine cone coordinates of `p` on the chart `X_{chartIndex p} = 1`. -/
 noncomputable def affineConeCoord {n : ℕ} (p : ProjSpace K n) :
diff --git a/LeanEval/Analysis/FractalUncertainty.lean b/LeanEval/Analysis/FractalUncertainty.lean
index 019cc5827..932067f09 100644
--- a/LeanEval/Analysis/FractalUncertainty.lean
+++ b/LeanEval/Analysis/FractalUncertainty.lean
@@ -38,7 +38,8 @@ def PorousOnLines (ν α₀ α₁ : ℝ) (X : Set ℝᵈ) : Prop :=
     ∃ x ∈ segment ℝ y₁ y₂, closedBall x (ν * R) ∩ X = ∅
 
 /-- Given `a b : ℝ`, the cube `[a,b]ᵈ` in `ℝᵈ`. -/
-abbrev cube (a b : ℝ) : Set ℝᵈ := EuclideanSpace.equiv (Fin d) ℝ ⁻¹' Set.univ.pi fun _ ↦ Set.Icc a b
+noncomputable abbrev cube (a b : ℝ) : Set ℝᵈ :=
+  EuclideanSpace.equiv (Fin d) ℝ ⁻¹' Set.univ.pi fun _ ↦ Set.Icc a b
 
 /--
 Statement of Theorem 1.1:
diff --git a/LeanEval/ConvexGeometry/Ulam.lean b/LeanEval/ConvexGeometry/Ulam.lean
index 7f4338e0c..6e94635d5 100644
--- a/LeanEval/ConvexGeometry/Ulam.lean
+++ b/LeanEval/ConvexGeometry/Ulam.lean
@@ -31,7 +31,7 @@ local notation "ℝᵈ" => EuclideanSpace ℝ (Fin d)
 
 variable (d) in
 /-- The unit sphere in `ℝᵈ`, centered at the origin. This is denoted `Sᵈ⁻¹` in the paper. -/
-abbrev S : Set ℝᵈ := Metric.sphere 0 1
+noncomputable abbrev S : Set ℝᵈ := Metric.sphere 0 1
 
 /-- A subset `K ⊆ ℝᵈ` is called origin-symmetric if `K = -K`. -/
 abbrev IsOriginSymmetric (K : Set ℝᵈ) : Prop :=
diff --git a/LeanEval/Geometry/MostowRigidity.lean b/LeanEval/Geometry/MostowRigidity.lean
index dd31f3a60..11bf18b90 100644
--- a/LeanEval/Geometry/MostowRigidity.lean
+++ b/LeanEval/Geometry/MostowRigidity.lean
@@ -87,7 +87,10 @@ instance [Star α] [ContinuousStar α] : IsTopologicalRing (MatrixSum p q α) :=
 variable [StarRing α] [ContinuousStar α]
 
 instance : ContinuousStar (MatrixSum p q α) where
-  continuous_star := by rw [star]; fun_prop
+  continuous_star := by
+    change Continuous (fun A : MatrixSum p q α =>
+      MatrixSum.ofMatrix (pmOneMat * (MatrixSum.ofMatrix.symm A).conjTranspose * pmOneMat))
+    fun_prop
 
 theorem MatrixSum.isClosed_unitary [T1Space α] :
     IsClosed (SetLike.coe <| unitary (MatrixSum p q α)) :=
diff --git a/LeanEval/KnotTheory/Slice.lean b/LeanEval/KnotTheory/Slice.lean
index 7f32373a0..9e04eea86 100644
--- a/LeanEval/KnotTheory/Slice.lean
+++ b/LeanEval/KnotTheory/Slice.lean
@@ -178,7 +178,7 @@ structure PLKnot where
   three_le : 3 ≤ vertices.length
 
 /-- The image of the PL knot in `ℝ³` (the trace of the polyline). -/
-def PLKnot.image (K : PLKnot) : Set R3 :=
+noncomputable def PLKnot.image (K : PLKnot) : Set R3 :=
   plCurve K.vertices '' Set.Ico (0 : ℝ) (K.vertices.length : ℝ)
 
 /-- The polyline is a *simple closed curve*: the periodic parametrization is
diff --git a/LeanEval/LinearAlgebra/TraceNewton.lean b/LeanEval/LinearAlgebra/TraceNewton.lean
index 2cec2b8fe..7d89f7fd7 100644
--- a/LeanEval/LinearAlgebra/TraceNewton.lean
+++ b/LeanEval/LinearAlgebra/TraceNewton.lean
@@ -28,7 +28,7 @@ stated uniformly for all positive `k`. -/
 noncomputable def charpolyDescendingCoeff {R : Type*} [CommRing R]
     (A : Matrix n n R) (k : ℕ) : R :=
   if k ≤ Fintype.card n then
-    Polynomial.coeff A.charpoly (Fintype.card n - k)
+    A.charpoly.coeff (Fintype.card n - k)
   else
     0
 
diff --git a/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean b/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean
index c2aea8f13..cdc2d8616 100644
--- a/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean
+++ b/LeanEval/NumberTheory/ZagierHoffmanPositiveChar.lean
@@ -52,25 +52,25 @@ noncomputable def 𝒵 (w : ℕ) : Submodule (RatFunc F) (CompletionAtInfty F) :
 
 /-- Let `q` be the size of the finite field `F`. `𝒯_aux w r` is the set of `ζ_A(s_1, ..., s_r)` of
 weight `w`, with `1 ≤ s_i ≤ q` for `1 ≤ i ≤ r − 1` and `1 ≤ s_r < q`. -/
-def 𝒯_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) :=
+noncomputable def 𝒯_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) :=
   let q := Nat.card F
   let 𝔖'_w := {𝔰 ∈ 𝔖_w w r | (∀ i : Fin r, i < (r - 1 : ℕ) → 𝔰 i ≤ q) ∧ 𝔰 ⟨r - 1, by simp⟩ < q}
   {ζ_A F s | s ∈ 𝔖'_w}
 
 /-- Let `q` be the size of the finite field `F`. `𝒯_w` is the set of `ζ_A(s_1,..., s_r)` of weight
 `w`, with `1 ≤ s_i ≤ q` for `1 ≤ i ≤ r − 1` and `1 ≤ s_r < q`, as `r` varies. -/
-def 𝒯 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯_aux F w r
+noncomputable def 𝒯 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯_aux F w r
 
 /-- Let `q` be the size of the finite field `F`. `𝒯0_aux` is the set of `ζ_A(s_1,..., s_r)` of
 weight `w`, with `1 ≤ s_i < q` for all `i`. -/
-def 𝒯0_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) :=
+noncomputable def 𝒯0_aux (w : ℕ) (r : ℕ+) : Set (CompletionAtInfty F) :=
   let q := Nat.card F
   let 𝔖'_w := {𝔰 ∈ 𝔖_w w r | ∀ i, 𝔰 i < q}
   {ζ_A F s | s ∈ 𝔖'_w}
 
 /-- Let `q` be the size of the finite field `F`. `𝒯0 w` is the set of `ζ_A(s_1,..., s_r)` of weight
 `w`, with `1 ≤ s_i < q` for all `i`, as `r` varies. -/
-def 𝒯0 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯0_aux F w r
+noncomputable def 𝒯0 (w : ℕ) : Set (CompletionAtInfty F) := ⋃ r : ℕ+, 𝒯0_aux F w r
 
 /-- The sequence `d(w)` from Conjecture 1.5 and Theorems A and D. -/
 noncomputable def d (w : ℕ) : ℕ :=
diff --git a/LeanEval/RepresentationTheory/SchurWeyl.lean b/LeanEval/RepresentationTheory/SchurWeyl.lean
index b2aa47e83..58a9be361 100644
--- a/LeanEval/RepresentationTheory/SchurWeyl.lean
+++ b/LeanEval/RepresentationTheory/SchurWeyl.lean
@@ -28,13 +28,16 @@ def symAction (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] (k :
   toFun σ := (PiTensorProduct.reindex R (fun _ : Fin k => M) σ).toLinearMap
   map_one' := by
     ext x
-    simp only [LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap, Function.comp_apply,
-      PiTensorProduct.reindex_tprod, Module.End.one_apply]
+    change PiTensorProduct.reindex R (fun _ : Fin k => M) 1 (PiTensorProduct.tprod R x) =
+      PiTensorProduct.tprod R x
+    simp only [PiTensorProduct.reindex_tprod]
     rfl
   map_mul' σ τ := by
     ext x
-    simp only [Module.End.mul_apply, LinearEquiv.coe_coe, LinearMap.coe_compMultilinearMap,
-      Function.comp_apply, PiTensorProduct.reindex_tprod]
+    change PiTensorProduct.reindex R (fun _ : Fin k => M) (σ * τ) (PiTensorProduct.tprod R x) =
+      PiTensorProduct.reindex R (fun _ : Fin k => M) σ
+        (PiTensorProduct.reindex R (fun _ : Fin k => M) τ (PiTensorProduct.tprod R x))
+    simp only [PiTensorProduct.reindex_tprod]
     rfl
 
 /-- The general linear group `GL(V)` acts diagonally on `V^⊗k`:
diff --git a/LeanEval/Topology/AnnulusBase.lean b/LeanEval/Topology/AnnulusBase.lean
index 0ee95c9b1..ed5167f23 100644
--- a/LeanEval/Topology/AnnulusBase.lean
+++ b/LeanEval/Topology/AnnulusBase.lean
@@ -52,7 +52,7 @@ embedding, and nothing of Kirby's torus trick or Quinn's 4-dimensional work.
 abbrev Amb (n : ℕ) : Type := EuclideanSpace ℝ (Fin n)
 
 /-- The unit `(n-1)`-sphere `Sⁿ⁻¹ ⊂ ℝⁿ`. -/
-abbrev Sph (n : ℕ) : Set (Amb n) := sphere (0 : Amb n) 1
+noncomputable abbrev Sph (n : ℕ) : Set (Amb n) := sphere (0 : Amb n) 1
 
 /-- The model hyperplane `{x | x₀ = 0}` in `ℝⁿ`, the local model for a flatly
 embedded sphere. -/
diff --git a/LeanEval/Topology/Hurewicz.lean b/LeanEval/Topology/Hurewicz.lean
index 42eded5d4..0b6568de4 100644
--- a/LeanEval/Topology/Hurewicz.lean
+++ b/LeanEval/Topology/Hurewicz.lean
@@ -25,7 +25,7 @@ abelianization of `π₁(X, x)`. -/
 @[eval_problem]
 theorem hurewicz_h1_abelianization
     (X : Type) [TopologicalSpace X] [PathConnectedSpace X] (x : X) :
-    Nonempty (Additive (Abelianization (FundamentalGroup X x)) ≃+
+    Nonempty (Additive ((FundamentalGroup X x) ⧸ commutator (FundamentalGroup X x)) ≃+
       (IntegralHomology 1 X : Type)) := by
   sorry
 
diff --git a/README.md b/README.md
index 561b4262e..ef665eb35 100644
--- a/README.md
+++ b/README.md
@@ -10,6 +10,31 @@ tooling generates one comparator workspace per problem under `generated/`.
 A submission is scored entirely by comparator results: a problem counts as solved iff
 comparator accepts the submitted solution.
 
+LeanEval supports **Lean v4.35.0** and **Lean v4.36.0-rc2**. The latter is the
+default checkout. Each configuration in `supported-toolchains.json` pins its own
+Mathlib, TauCeti, and transitive dependencies. CI requires the shared problem
+statements to compile on both toolchains without unexpected warnings; it does
+not compare their elaborated meanings across dependency versions.
+
+To work on the stable configuration in an isolated directory:
+
+```bash
+python scripts/prepare_toolchain.py stable --destination /tmp/lean-eval-stable
+cd /tmp/lean-eval-stable
+lake exe cache get
+cache_env="$(bash scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env"
+lake exe lean-eval generate --problem two_plus_two
+lake exe lean-eval start-problem two_plus_two
+```
+
+Use `rc` instead of `stable` for the default configuration. Existing build outputs
+are excluded from these copies. After selecting a configuration, regenerate each
+workspace you use so its pins and extracted statements match that configuration.
+The submission service reads the closest `lean-toolchain` at or above each
+submitted workspace and selects the corresponding approved configuration. Omit
+the file to use the default. Submit workspaces for different toolchains separately.
+Result verification receipts and archive sidecars record the selected toolchain and exact benchmark commit.
+
 The main user-facing entrypoint is:
 
 ```bash
@@ -206,11 +231,37 @@ Trusted files you should not edit in the normal solver workflow are:
 `Challenge.lean` contains the benchmark statement. `Solution.lean` is the fixed bridge
 that tells comparator to check your theorem from the `Submission` namespace.
 
-Solutions may import `LeanPool.*` modules from [Lean Pool](https://github.com/Vilin97/lean-pool)
-in `Submission.lean` or `Submission/` helpers. The pinned dependency is included in
-all generated workspaces via `solution-dependencies.json`. Problem statements and
-their local helpers may not import it; workspace generation rejects these imports.
-Comparator and nanoda checks apply as usual.
+Solutions may import modules from [Lean Pool](https://github.com/Vilin97/lean-pool),
+[CFSG](https://github.com/AxiomMath/CFSG), and
+[Stacks](https://github.com/AxiomMath/Stacks) in `Submission.lean` or `Submission/`
+helpers. These pinned dependencies are included in generated workspaces via
+`solution-dependencies.json`. Problem statements and their local helpers may not
+import them; workspace generation rejects these imports. Comparator and NanoDa
+checks apply as usual.
+
+After fetching the workspace dependencies, prepare the libraries it imports:
+
+```bash
+cache_env="$(bash /path/to/lean-eval/scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env"
+```
+
+This parses Lean import headers, fetches each required library's revision mappings,
+and restores only the imported modules and their transitive dependencies. It uses
+`lake --no-build`, so missing artifacts fail rather than starting a large rebuild.
+Each library must match the workspace's Lean toolchain and all transitive dependency
+pins. Unused libraries require no artifact downloads.
+
+The public CFSG pin still uses v4.35.0-rc3. Stacks uses v4.35.0 with Mathlib
+`56a00585`, while LeanEval's stable configuration uses Mathlib `07406378` to
+match TauCeti's stable release. These library imports fail the cache compatibility
+check until matching dependency builds are published, including the Mathlib pin.
+Unused solution libraries do not prevent evaluation on either toolchain. The helper
+uses the published [CFSG cache](https://cfsg-downloads.axiommath.workers.dev/lake/lake-cache-get-fast.sh)
+and [Stacks cache](https://stacks-cache.axiommath.workers.dev/lake/lake-cache-get-fast.sh)
+endpoints by default. Set `STACKS_ARTIFACT_ENDPOINT` and `STACKS_REVISION_ENDPOINT`
+to override the Stacks endpoints; corresponding overrides are available as
+`CFSG_*` and `TAUCETI_*`. CI and the submission runner accept the Stacks overrides
+from repository variables with those same names; empty variables use the defaults.
 
 ### 5. Run comparator locally
 
@@ -352,8 +403,8 @@ In practice, solvers should normally work in `Submission.lean` and `Submission/`
 
 ## End-To-End Repo Checks
 
-`bash scripts/fetch_dependency_caches.sh --restore .` restores imported TauCeti
-modules without permitting compilation. Downloads have bounded retries and
+`bash scripts/fetch_dependency_caches.sh --restore .` restores imported TauCeti,
+CFSG, and Stacks modules without permitting compilation. Downloads have bounded retries and
 timeouts and use temporary files to keep interrupted transfers out of the
 artifact cache. Cache-only restoration is retried once; if it still fails, the
 script prints verbose diagnostics before stopping. Verify the pinned versions
diff --git a/SECURITY.md b/SECURITY.md
index c05654915..0f04e17a3 100644
--- a/SECURITY.md
+++ b/SECURITY.md
@@ -92,9 +92,12 @@ an empty environment. It preserves Lake's other arguments and settings.
 Mounts come from trusted root state, never submission input. Private local
 workspaces do not need this visibility adapter.
 
-Existing trusted root builds finish dependency setup before evaluation, including
-ProofWidgets metadata that cannot be updated in a read-only cache. Shared source
-and cached artifacts remain read-only during submission builds. The submissions
+Trusted root builds prepare dependencies before evaluation, including ProofWidgets
+metadata that cannot be updated in a read-only cache. After overlaying solver files,
+the submissions adapter can restore additional publisher artifacts selected by
+registered library imports and pinned cache mappings. It parses headers without
+elaborating solver code and permits no compilation during restoration. Shared
+source and cached artifacts remain read-only during submission builds. The submissions
 adapter gives Lean Pool its own writable build outputs in each workspace while
 sharing its pinned source read-only; one submission must never supply writable
 artifacts to another.
@@ -119,8 +122,26 @@ in both benchmark and submission installers. Review the actual sandbox behavior,
 not just the reported version. No standalone comparator/exporter/NanoDa build or
 Landrun pin is required by this benchmark.
 
-The generator rejects Lean Pool imports in trusted statements and helpers while
-making its pinned source available to solutions. Maintain that separation.
+`supported-toolchains.json` selects only benchmark-owned configurations under
+`toolchains/`. Keep the default configuration identical to the root Lake files.
+Each configuration has separate package checkouts and build outputs. Source
+`lean-toolchain` files request a configuration; they cannot authorize arbitrary
+toolchains, dependency pins, Lake code, or build commands. Selection reads the
+archived tar stream without extracting or executing submission code. The archive
+lane retains invalid requests; evaluation rejects them after archival. Regenerate
+selected pristine workspaces from trusted sources before overlaying solver files.
+CI checks compilation under both supported configurations, without asserting
+equivalence of their elaborated problem statements.
+
+The generator rejects Lean Pool, CFSG, and Stacks imports in trusted statements
+and helpers while making their pinned source available to solutions. Cache
+preparation parses submission headers without elaborating them and restores only
+registered library targets with `lake --no-build`. Maintain that separation.
+Benchmark CI checks out only package metadata for the solution-only CFSG and
+Stacks dependencies using `scripts/prepare_ci_dependencies.py`. Their real
+pinned Lake configuration and manifests remain available; the generator's
+statement-import prohibition remains enforced. Submission evaluation uses full
+source checkouts and never invokes this CI-only preparation helper.
 Historical replay locks and instrumentation are versioned independently; do not
 silently change their verifier or metric semantics.
 
diff --git a/lake-manifest.json b/lake-manifest.json
index be874ffb4..50817ff4e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,20 +15,40 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24",
+   "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b63f6e8a68d220e3b3bc4f3792bb53650d375f24",
+   "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/TauCetiProject/TauCeti",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380",
+   "rev": "be86813dc92e6bac8614c2c2dd34572145df09c0",
    "name": "TauCeti",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380",
+   "inputRev": "be86813dc92e6bac8614c2c2dd34572145df09c0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/AxiomMath/Stacks.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+   "name": "Stacks",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/AxiomMath/CFSG.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
+   "name": "cfsg",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/Vilin97/lean-pool.git",
@@ -45,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b",
+   "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3",
+   "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "10a2cfff285e1c7c2ebc49c0ba22cab0f3c58ee5",
+   "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1",
+   "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea",
+   "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -95,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9",
+   "rev": "b0256621cb88178e9ad932a53633077b3029e621",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b",
+   "rev": "4af7237d146261353907b06a01b6f3fc06cfa067",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,10 +135,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc3",
+   "inputRev": "v4.36.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«lean-eval»",
diff --git a/lakefile.toml b/lakefile.toml
index b54b07d77..5e17c52ac 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,7 @@
 name = "lean-eval"
 defaultTargets = ["LeanEval"]
+# Generated benchmark statements retain legacy visibility rules.
+allowNonModules = true
 
 [leanOptions]
 autoImplicit = false
@@ -11,6 +13,20 @@ name = "lean-pool"
 git = "https://github.com/Vilin97/lean-pool.git"
 rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f"
 
+# Large solution libraries. Their caches are fetched only when imported.
+# Keep these before TauCeti and Mathlib so the benchmark owns shared pins.
+# Their published pins currently predate this toolchain; cache preparation
+# rejects imports until the publishers provide matching builds (see README).
+[[require]]
+name = "cfsg"
+git = "https://github.com/AxiomMath/CFSG.git"
+rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33"
+
+[[require]]
+name = "Stacks"
+git = "https://github.com/AxiomMath/Stacks.git"
+rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b"
+
 # TauCeti supplies the definitions in the classification of finite simple groups
 # problem. It is listed before Mathlib because Lake takes shared transitive
 # dependencies (batteries, aesop, ...) from the later require, and those must be
@@ -20,12 +36,12 @@ rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f"
 [[require]]
 name = "TauCeti"
 git = "https://github.com/TauCetiProject/TauCeti"
-rev = "6e0c6acab5f4c6f42e5f5bab9bd5e4e84f74c380"
+rev = "be86813dc92e6bac8614c2c2dd34572145df09c0"
 
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "b63f6e8a68d220e3b3bc4f3792bb53650d375f24"
+rev = "2ddf59c8f14245864e6c0ed227a2dab76b9efea2"
 
 [[require]]
 name = "lean-eval-generator"
diff --git a/lean-toolchain b/lean-toolchain
index f0e00b333..0fc433692 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc3
+leanprover/lean4:v4.36.0-rc2
diff --git a/scripts/dependency_imports.lean b/scripts/dependency_imports.lean
new file mode 100644
index 000000000..08d3a8a85
--- /dev/null
+++ b/scripts/dependency_imports.lean
@@ -0,0 +1,25 @@
+import Lean
+
+/- Parse headers without loading the imported libraries or running submission code. -/
+def main (args : List String) : IO Unit := do
+  let [pathsFile] := args
+    | throw <| IO.userError "usage: dependency_imports.lean <JSON file of source paths>"
+  let paths ← IO.ofExcept <|
+    (Lean.Json.parse (← IO.FS.readFile pathsFile)).bind (Lean.fromJson? (α := Array String))
+  let mut imports : Array (String × Array String) := #[]
+  for path in paths do
+    let (header, _, messages) ← Lean.Elab.parseImports (← IO.FS.readFile path) path
+    if messages.hasErrors then
+      -- Comparator reports malformed solver headers as ordinary proof failures.
+      IO.eprintln s!"Skipping malformed import header in {path}; the Lean build will report it"
+      continue
+    for imp in header do
+      let name := imp.module.toString
+      unless imports.any (·.1 == name) do
+        let parts := imp.module.components.toArray.map fun component =>
+          match component with
+          | .str _ s => s
+          | .num _ n => toString n
+          | .anonymous => ""
+        imports := imports.push (name, parts)
+  IO.println <| Lean.Json.compress <| Lean.toJson imports
diff --git a/scripts/fetch_dependency_caches.py b/scripts/fetch_dependency_caches.py
new file mode 100644
index 000000000..6e6cd1e2f
--- /dev/null
+++ b/scripts/fetch_dependency_caches.py
@@ -0,0 +1,216 @@
+#!/usr/bin/env python3
+"""Restore published Lake artifacts for the large libraries a project imports."""
+from __future__ import annotations
+
+import argparse
+from dataclasses import dataclass
+import json
+import os
+from pathlib import Path
+import re
+import shlex
+import subprocess
+import sys
+import tempfile
+import time
+
+
+SCRIPTS = Path(__file__).resolve().parent
+
+
+@dataclass(frozen=True)
+class Library:
+    package: str
+    repo: str
+    roots: tuple[str, ...]
+    prefix: str
+    endpoint: str = ""
+
+
+LIBRARIES = (
+    Library("TauCeti", "TauCetiProject/TauCeti", ("TauCeti",), "TAUCETI",
+            "https://cache.taucetiproject.org"),
+    Library("cfsg", "AxiomMath/CFSG", ("CFSG", "CFSGWithCertificates", "Certificates", "Comparator"),
+            "CFSG", "https://cfsg-downloads.axiommath.workers.dev/lake"),
+    Library("Stacks", "AxiomMath/Stacks", ("Stacks", "StacksCore", "StacksFrontier"),
+            "STACKS", "https://stacks-cache.axiommath.workers.dev/lake"),
+)
+
+
+def manifest(path: Path) -> dict[str, dict]:
+    data = json.loads(path.read_text(encoding="utf-8"))
+    return {p["name"].strip("«»"): p for p in data["packages"]}
+
+
+def imported_modules(project: Path) -> dict[str, list[str]]:
+    paths = []
+
+    def unreadable(error: OSError) -> None:
+        raise error
+
+    for directory, subdirs, files in os.walk(project, onerror=unreadable):
+        subdirs[:] = sorted(d for d in subdirs if d not in {".lake", ".git"})
+        paths.extend(str(Path(directory) / f) for f in sorted(files) if f.endswith(".lean"))
+    with tempfile.TemporaryDirectory(prefix="lean-eval-imports-") as temporary:
+        source_list = Path(temporary) / "paths.json"
+        source_list.write_text(json.dumps(paths), encoding="utf-8")
+        result = subprocess.run(
+            ["lean", "-j2", "--run", str(SCRIPTS / "dependency_imports.lean"), str(source_list)],
+            cwd=project, text=True, capture_output=True, check=False,
+        )
+    if result.returncode:
+        raise RuntimeError(f"could not parse project imports:\n{result.stdout}{result.stderr}")
+    if result.stderr:
+        print(result.stderr, file=sys.stderr, end="")
+    return dict(json.loads(result.stdout))
+
+
+def belongs(module: str, library: Library) -> bool:
+    return any(module == root or module.startswith(root + ".") for root in library.roots)
+
+
+def retry(command: list[str], project: Path, env: dict[str, str], attempts: int) -> str:
+    for attempt in range(1, attempts + 1):
+        # Buffer only the diagnostics, not downloaded artifacts. Keep stdout
+        # reserved for the export line the shell caller evaluates.
+        result = subprocess.run(command, cwd=project, env=env, text=True,
+                                stdout=subprocess.PIPE, stderr=subprocess.STDOUT, check=False)
+        if result.returncode == 0:
+            return result.stdout
+        print(result.stdout, file=sys.stderr, end="")
+        if attempt < attempts:
+            print(f"::notice::dependency cache operation failed (attempt {attempt} of {attempts}); retrying",
+                  file=sys.stderr)
+            time.sleep(5)
+    raise RuntimeError("dependency cache restoration failed after bounded retries; no compilation "
+                       "was permitted. Check the pins and published cache coverage.")
+
+
+def prepare(project: Path, restore: bool) -> dict[str, str]:
+    packages = manifest(project / "lake-manifest.json")
+    available = [lib for lib in LIBRARIES if lib.package in packages]
+    if not available:
+        print("fetch_dependency_caches: no supported packages in the manifest; nothing to fetch",
+              file=sys.stderr)
+        return {}
+    modules = imported_modules(project)
+    for module, parts in list(modules.items()):
+        library = next((lib for lib in available if belongs(module, lib)), None)
+        if library is None:
+            continue
+        directory = project / ".lake/packages" / library.package
+        # Invalid/missing solver imports belong to comparator's verdict, not
+        # an infrastructure failure for every problem in the submission.
+        # Restrict CLI targets as well: quoted components can contain path
+        # separators or dots, which Lake's target parser treats differently.
+        plain = module == ".".join(parts) and all(
+            part and all(c.isalnum() or c in "_'" for c in part) for part in parts)
+        source = directory.joinpath(*parts[:-1], parts[-1] + ".lean")
+        if not plain or ((directory / "lake-manifest.json").is_file() and not source.is_file()):
+            print(f"fetch_dependency_caches: leaving unresolved import {module} to comparator",
+                  file=sys.stderr)
+            del modules[module]
+    needed = [lib for lib in available if any(belongs(m, lib) for m in modules)]
+    # CFSG's artifacts depend on TauCeti, even if the submission does not import
+    # TauCeti directly. Register every supported transitive cache as well.
+    directories = {}
+    index = 0
+    while index < len(needed):
+        library = needed[index]
+        index += 1
+        directory = project / ".lake/packages" / library.package
+        if not (directory / "lake-manifest.json").is_file():
+            raise RuntimeError(f"{directory} is not checked out; fetch the dependencies first")
+        directories[library.package] = directory
+        dependencies = manifest(directory / "lake-manifest.json")
+        for other in available:
+            if other.package in dependencies and other not in needed:
+                needed.append(other)
+    if not needed:
+        print("fetch_dependency_caches: no supported library imports; nothing to fetch", file=sys.stderr)
+        return {}
+
+    toolchain = (project / "lean-toolchain").read_text().strip()
+    services = []
+    # Validate every library before fetching anything: a different transitive
+    # pin changes build traces just as a different Mathlib pin does.
+    for library in needed:
+        directory = directories[library.package]
+        their_toolchain = (directory / "lean-toolchain").read_text().strip()
+        dependencies = manifest(directory / "lake-manifest.json")
+        mismatches = [name for name, dep in dependencies.items()
+                      if name not in packages or packages[name].get("rev") != dep.get("rev")]
+        if toolchain != their_toolchain or mismatches:
+            raise RuntimeError(
+                f"{library.package} {packages[library.package]['rev']} was built with {their_toolchain}; "
+                f"this project pins {toolchain}. Different dependency pins: {', '.join(mismatches) or 'none'}. "
+                "Pin the same toolchain and Mathlib (and other transitive dependencies) as the library "
+                "commit so its build cache applies.")
+        artifacts = (os.environ.get(f"{library.prefix}_ARTIFACT_ENDPOINT") or
+                     (f"{library.endpoint}/artifacts" if library.endpoint else ""))
+        revisions = (os.environ.get(f"{library.prefix}_REVISION_ENDPOINT") or
+                     (f"{library.endpoint}/revisions" if library.endpoint else ""))
+        if not artifacts or not revisions:
+            raise RuntimeError(f"set {library.prefix}_ARTIFACT_ENDPOINT and "
+                               f"{library.prefix}_REVISION_ENDPOINT to the publisher's public cache URLs")
+        services.append((library, artifacts, revisions))
+
+    descriptor, config_name = tempfile.mkstemp(
+        prefix="lean-eval-dependency-cache.", dir=os.environ.get("RUNNER_TEMP") or None)
+    config = Path(config_name)
+    try:
+        with os.fdopen(descriptor, "w", encoding="utf-8") as output:
+            for library, artifacts, revisions in services:
+                # JSON strings are valid TOML basic strings. Each fetched
+                # mapping records its service, so multiple caches coexist.
+                output.write('[[cache.service]]\n')
+                output.write(f'name = "{library.prefix.lower()}-public"\nkind = "s3"\n')
+                output.write(f"artifactEndpoint = {json.dumps(artifacts)}\n")
+                output.write(f"revisionEndpoint = {json.dumps(revisions)}\n")
+        settings = {"LAKE_CONFIG": str(config), "LAKE_ARTIFACT_CACHE": "true",
+                    "CURL": str(SCRIPTS / "lake_cache_curl.py")}
+        env = dict(os.environ, **settings, LAKE_RESTORE_ARTIFACTS="true")
+        for library, _, _ in services:
+            retry(["lake", "-v", "cache", "get", "--service", f"{library.prefix.lower()}-public",
+                   "--repo", library.repo, "--package", library.package,
+                   "--rev", packages[library.package]["rev"], "--mappings-only"], project, env, 3)
+        if restore:
+            targets = sorted({m for m in modules if any(belongs(m, lib) for lib in needed)})
+            print(f"fetch_dependency_caches: restoring {len(targets)} imported library module(s) "
+                  "and their dependencies", file=sys.stderr)
+            # `+` selects a module even when a library has the same name;
+            # a bare name could otherwise restore every module of that library.
+            log = retry(["lake", "-v", "--no-build", "build", *("+" + m for m in targets)],
+                        project, env, 2)
+            roots = "|".join(re.escape(root) for lib in needed for root in lib.roots)
+            if re.search(rf"Built (?:{roots})(?:[.\s]|$)", log):
+                raise RuntimeError("a dependency module was compiled instead of downloaded:\n" + log)
+        return settings
+    except BaseException:
+        config.unlink(missing_ok=True)
+        raise
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--restore", action="store_true")
+    parser.add_argument("project", type=Path)
+    args = parser.parse_args()
+    try:
+        settings = prepare(args.project.resolve(), args.restore)
+        if settings:
+            if github_env := os.environ.get("GITHUB_ENV"):
+                with open(github_env, "a", encoding="utf-8") as output:
+                    for name, value in settings.items():
+                        output.write(f"{name}={value}\n")
+            else:
+                print("export " + " ".join(f"{name}={shlex.quote(value)}"
+                                           for name, value in settings.items()))
+        return 0
+    except (OSError, ValueError, RuntimeError) as error:
+        print(f"::error::fetch_dependency_caches: {error}", file=sys.stderr)
+        return 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/fetch_dependency_caches.sh b/scripts/fetch_dependency_caches.sh
index 0a1462719..1519b27bd 100644
--- a/scripts/fetch_dependency_caches.sh
+++ b/scripts/fetch_dependency_caches.sh
@@ -1,166 +1,12 @@
 #!/usr/bin/env bash
-# Prepare a lean-eval checkout (or a project that reuses its dependencies) to download TauCeti's
-# build outputs instead of compiling TauCeti.
-#
 # Usage: bash scripts/fetch_dependency_caches.sh [--restore] <project-dir>
-#
-# TauCeti publishes the oleans of every main commit to a public Lake artifact cache. Lake only
-# reuses them if TauCeti is built here exactly as TauCeti's CI built it, so this script first
-# checks that the project pins the same Lean toolchain and Mathlib revision as the pinned TauCeti
-# commit, and fails if not. It then downloads the (small) input-to-output mappings for the
-# pinned TauCeti revision and writes a Lake configuration naming TauCeti's cache service. Builds
-# that run with LAKE_CONFIG pointing at that file and LAKE_ARTIFACT_CACHE=true fetch the TauCeti
-# artifacts they need.
-#
-# With --restore, the script also builds every TauCeti module that a `.lean` file of the project
-# imports, restoring the downloaded outputs into TauCeti's build directory. --no-build prevents
-# compilation on a cache miss. Verbose diagnostics retain artifact errors; a curl wrapper adds
-# bounded retries and publishes downloads atomically so interrupted transfers cannot poison
-# later cache attempts.
-# Later builds then find those modules up to date even without the cache settings.
-#
-# Under GitHub Actions the cache and curl settings are appended to $GITHUB_ENV. Otherwise,
-# when GITHUB_ENV is unset or empty, stdout is a single `export` line for the caller:
-#
-#   cache_env="$(bash scripts/fetch_dependency_caches.sh .)" && eval "$cache_env"
-#
-# (Assign first: `eval "$(...)"` would hide a failure of the script.)
-#
-# A project whose manifest has no TauCeti package needs nothing, and the script exits cleanly.
-# The dependencies must already be checked out (for example by `lake exe cache get`).
+# Dependencies must already be checked out (e.g. by `lake exe cache get`).
+# --restore downloads imported library modules and their dependencies with
+# `lake --no-build`, refusing to compile on a cache miss. Without --restore,
+# fetch only revision mappings. See README.md for supported public libraries.
+#
+# In GitHub Actions, settings are appended to GITHUB_ENV. Otherwise stdout is
+# one shell export line, suitable for:
+# cache_env="$(bash scripts/fetch_dependency_caches.sh --restore .)" && eval "$cache_env"
 set -euo pipefail
-# Stdout carries only the final `export` line, so it can be passed to `eval`.
-exec 3>&1 1>&2
-
-RESTORE=0
-if [ "${1:-}" = "--restore" ]; then
-  RESTORE=1
-  shift
-fi
-PROJECT_DIR="$(cd "${1:?usage: fetch_dependency_caches.sh [--restore] <project-dir>}" && pwd)"
-CACHE_CURL="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/lake_cache_curl.py"
-ARTIFACT_ENDPOINT="${TAUCETI_ARTIFACT_ENDPOINT:-https://cache.taucetiproject.org/artifacts}"
-REVISION_ENDPOINT="${TAUCETI_REVISION_ENDPOINT:-https://cache.taucetiproject.org/revisions}"
-
-manifest_rev() {
-  # manifest_rev <lake-manifest.json> <package>: the pinned rev, or nothing.
-  python3 - "$1" "$2" <<'PY'
-import json, sys
-with open(sys.argv[1], encoding="utf-8") as f:
-    packages = json.load(f)["packages"]
-print(next((p["rev"] for p in packages if p["name"] == sys.argv[2]), ""))
-PY
-}
-
-TAUCETI_REV="$(manifest_rev "$PROJECT_DIR/lake-manifest.json" TauCeti)"
-if [ -z "$TAUCETI_REV" ]; then
-  echo "fetch_dependency_caches: no TauCeti package in the manifest; nothing to fetch"
-  exit 0
-fi
-
-TAUCETI_DIR="$PROJECT_DIR/.lake/packages/TauCeti"
-if [ ! -f "$TAUCETI_DIR/lake-manifest.json" ]; then
-  echo "::error::fetch_dependency_caches: $TAUCETI_DIR is not checked out; fetch the dependencies first"
-  exit 1
-fi
-
-# TauCeti's published outputs are keyed by the toolchain and by the traces of the Mathlib it was
-# built against, so any difference here turns every lookup into a miss and a full rebuild.
-ours_toolchain="$(tr -d '[:space:]' < "$PROJECT_DIR/lean-toolchain")"
-their_toolchain="$(tr -d '[:space:]' < "$TAUCETI_DIR/lean-toolchain")"
-ours_mathlib="$(manifest_rev "$PROJECT_DIR/lake-manifest.json" mathlib)"
-their_mathlib="$(manifest_rev "$TAUCETI_DIR/lake-manifest.json" mathlib)"
-if [ "$ours_toolchain" != "$their_toolchain" ] || [ "$ours_mathlib" != "$their_mathlib" ]; then
-  echo "::error::fetch_dependency_caches: TauCeti $TAUCETI_REV was built with $their_toolchain and Mathlib $their_mathlib, but this project pins $ours_toolchain and Mathlib $ours_mathlib. Pin the same toolchain and Mathlib as the TauCeti commit so its build cache applies."
-  exit 1
-fi
-
-CONFIG="$(mktemp "${RUNNER_TEMP:-${TMPDIR:-/tmp}}/lean-eval-dependency-cache.XXXXXX")"
-python3 - "$CONFIG" "$ARTIFACT_ENDPOINT" "$REVISION_ENDPOINT" <<'PY'
-import json, sys
-path, artifacts, revisions = sys.argv[1:]
-with open(path, "w", encoding="utf-8") as f:
-    # JSON strings are valid TOML basic strings.
-    f.write('cache.defaultService = "tauceti-public"\n')
-    f.write('[[cache.service]]\n')
-    f.write('name = "tauceti-public"\n')
-    f.write('kind = "s3"\n')
-    f.write(f"artifactEndpoint = {json.dumps(artifacts)}\n")
-    f.write(f"revisionEndpoint = {json.dumps(revisions)}\n")
-PY
-
-fetched=0
-for attempt in 1 2 3; do
-  if (cd "$PROJECT_DIR" && CURL="$CACHE_CURL" LAKE_CONFIG="$CONFIG" lake -v cache get --service tauceti-public \
-        --repo TauCetiProject/TauCeti --package TauCeti --rev "$TAUCETI_REV" --mappings-only); then
-    fetched=1
-    break
-  fi
-  echo "::notice::fetching TauCeti's cache mappings failed (attempt $attempt of 3)"
-  sleep 5
-done
-if [ "$fetched" != 1 ]; then
-  echo "::error::fetch_dependency_caches: could not fetch TauCeti's cache mappings for $TAUCETI_REV"
-  exit 1
-fi
-
-if [ "$RESTORE" = 1 ]; then
-  # Every TauCeti module a `.lean` file of the project (outside .lake) imports, one per line.
-  # Lean's header syntax is `[public] [meta] import [all] Module`; a file that cannot be read
-  # makes this fail rather than silently restore less.
-  modules="$(python3 - "$PROJECT_DIR" <<'PY'
-import pathlib, re, sys
-root = pathlib.Path(sys.argv[1])
-pattern = re.compile(
-    r"^\s*(?:public\s+)?(?:meta\s+)?import\s+(?:all\s+)?(TauCeti(?:\.[^\s.-]+)*)", re.M)
-found = set()
-for path in root.rglob("*.lean"):
-    if ".lake" in path.relative_to(root).parts:
-        continue
-    found.update(pattern.findall(path.read_text(encoding="utf-8")))
-print("\n".join(sorted(found)))
-PY
-)"
-  if [ -n "$modules" ]; then
-    count="$(printf '%s\n' "$modules" | wc -l)"
-    echo "fetch_dependency_caches: restoring $count imported TauCeti module(s) and their dependencies"
-    log="$(mktemp)"
-    restored=0
-    for attempt in 1 2; do
-      # shellcheck disable=SC2086 # one module name per word; no whitespace
-      if (cd "$PROJECT_DIR" && CURL="$CACHE_CURL" LAKE_CONFIG="$CONFIG" LAKE_ARTIFACT_CACHE=true \
-            LAKE_RESTORE_ARTIFACTS=true lake -v --no-build build $modules) > "$log" 2>&1; then
-        restored=1
-        break
-      fi
-      cat "$log"
-      if [ "$attempt" = 1 ]; then
-        echo "::notice::cache-only restoration failed (attempt 1 of 2); retrying without compiling dependencies"
-        sleep 5
-      fi
-    done
-    if [ "$restored" != 1 ]; then
-      rm -f "$log"
-      echo "::error::fetch_dependency_caches: dependency cache restoration failed after bounded retries; no compilation was permitted. Inspect the diagnostics above for unavailable artifacts or out-of-date dependencies, and check the pins and published cache coverage."
-      exit 1
-    fi
-    compiled="$(grep -cE 'Built TauCeti(\.|$| )' "$log" || true)"
-    if [ "$compiled" != 0 ]; then
-      grep -m 20 -E 'Built TauCeti(\.|$| )' "$log" || true
-      rm -f "$log"
-      echo "::error::fetch_dependency_caches: $compiled TauCeti module(s) were compiled instead of downloaded; TauCeti's cache does not cover this pin"
-      exit 1
-    fi
-    rm -f "$log"
-  fi
-fi
-
-if [ -n "${GITHUB_ENV:-}" ]; then
-  {
-    echo "LAKE_CONFIG=$CONFIG"
-    echo "LAKE_ARTIFACT_CACHE=true"
-    echo "CURL=$CACHE_CURL"
-  } >> "$GITHUB_ENV"
-else
-  printf 'export LAKE_CONFIG=%q LAKE_ARTIFACT_CACHE=true CURL=%q\n' "$CONFIG" "$CACHE_CURL" >&3
-fi
+exec python3 "$(dirname "${BASH_SOURCE[0]}")/fetch_dependency_caches.py" "$@"
diff --git a/scripts/prepare_ci_dependencies.py b/scripts/prepare_ci_dependencies.py
new file mode 100644
index 000000000..6dc2d6e31
--- /dev/null
+++ b/scripts/prepare_ci_dependencies.py
@@ -0,0 +1,67 @@
+#!/usr/bin/env python3
+"""Materialize only package metadata for solution-only CFSG/Stacks CI dependencies.
+
+Trusted problem sources cannot import these packages. Their source trees are
+therefore unnecessary for catalog generation, statement builds, and verifier
+probes. Lake still reads their real, pinned package configuration and manifest.
+This helper is for benchmark CI only; submission preparation uses full sources.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+import re
+import subprocess
+import sys
+
+
+PACKAGES = frozenset({"cfsg", "Stacks"})
+METADATA = ("lakefile.toml", "lakefile.lean", "lake-manifest.json", "lean-toolchain")
+
+
+def git(directory: Path, *arguments: str) -> None:
+    subprocess.run(["git", "-C", str(directory), *arguments], check=True)
+
+
+def prepare(root: Path) -> None:
+    policy = json.loads((root / "solution-dependencies.json").read_text())
+    allowed = {entry["name"] for entry in policy}
+    if not PACKAGES <= allowed:
+        raise ValueError("metadata-only packages must be forbidden in trusted statement imports")
+    manifest = json.loads((root / "lake-manifest.json").read_text())
+    packages = {p["name"].strip("«»"): p for p in manifest["packages"]}
+    for name in sorted(PACKAGES):
+        package = packages[name]
+        revision = package["rev"]
+        if re.fullmatch(r"[0-9a-f]{40}", revision) is None:
+            raise ValueError(f"{name} is not pinned to an exact commit")
+        destination = root / ".lake/packages" / name
+        if destination.exists() or destination.is_symlink():
+            raise ValueError(f"expected a fresh CI checkout; {destination} already exists")
+        destination.mkdir(parents=True)
+        git(destination, "init", "--quiet", "--initial-branch=main")
+        git(destination, "remote", "add", "origin", package["url"])
+        git(destination, "sparse-checkout", "set", "--no-cone",
+            *("/" + name for name in METADATA))
+        git(destination, "fetch", "--quiet", "--filter=tree:0", "--depth=1", "--no-tags",
+            "origin", revision)
+        git(destination, "checkout", "--quiet", "--detach", revision)
+        if not (destination / "lake-manifest.json").is_file():
+            raise ValueError(f"{name} does not publish its dependency manifest")
+        print(f"Prepared {name} package metadata at {revision}")
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--root", type=Path, default=Path(__file__).resolve().parents[1])
+    args = parser.parse_args()
+    try:
+        prepare(args.root)
+    except (OSError, ValueError, KeyError, subprocess.CalledProcessError) as error:
+        parser.exit(1, f"prepare_ci_dependencies: {error}\n")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/prepare_toolchain.py b/scripts/prepare_toolchain.py
new file mode 100644
index 000000000..4a44b2fb2
--- /dev/null
+++ b/scripts/prepare_toolchain.py
@@ -0,0 +1,80 @@
+#!/usr/bin/env python3
+"""Select a benchmark-owned toolchain configuration in an isolated checkout.
+
+Use --destination to create a separate working copy, or --apply in a fresh CI
+checkout before fetching dependencies. Regenerate selected workspaces afterwards;
+generated statements and build outputs must come from the selected configuration.
+"""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+import shutil
+import sys
+
+
+ROOT = Path(__file__).resolve().parents[1]
+FILES = ("lean-toolchain", "lakefile.toml", "lake-manifest.json")
+
+
+def configurations(root: Path) -> tuple[str, dict[str, Path]]:
+    data = json.loads((root / "supported-toolchains.json").read_text())
+    result = {}
+    for toolchain, relative in data["configurations"].items():
+        path = (root / relative).resolve()
+        if not path.is_relative_to(root.resolve()):
+            raise ValueError("toolchain configuration escapes the benchmark")
+        if (path / "lean-toolchain").read_text().strip() != toolchain:
+            raise ValueError(f"toolchain configuration disagrees with its pin: {toolchain}")
+        for name in FILES:
+            if (path / name).is_symlink() or not (path / name).is_file():
+                raise ValueError(f"missing regular configuration file: {path / name}")
+        result[toolchain] = path
+    if data["default"] not in result or data["stable"] not in result:
+        raise ValueError("default or stable toolchain has no configuration")
+    return data["default"], result
+
+
+def prepare(root: Path, toolchain: str, destination: Path | None = None) -> Path:
+    default, supported = configurations(root)
+    stable = json.loads((root / "supported-toolchains.json").read_text())["stable"]
+    toolchain = {"stable": stable, "default": default,
+                 "rc": default}.get(toolchain, toolchain)
+    if toolchain not in supported:
+        raise ValueError(f"unsupported toolchain {toolchain!r}; choose {', '.join(supported)}")
+    # Read everything before mutation, including when the chosen configuration
+    # is the root itself. Build artifacts are never reused between toolchains.
+    contents = {name: (supported[toolchain] / name).read_bytes() for name in FILES}
+    target = root if destination is None else destination.resolve()
+    if destination is None:
+        if (root / ".lake").exists() or (root / ".lake").is_symlink():
+            raise ValueError("--apply requires a fresh checkout without .lake; use --destination")
+    else:
+        if target.exists():
+            raise ValueError(f"destination already exists: {target}")
+        if target.is_relative_to(root.resolve()) and ".lake" not in target.relative_to(root).parts:
+            raise ValueError("an in-tree destination must be under .lake")
+        shutil.copytree(root, target, ignore=shutil.ignore_patterns(
+            ".git", ".lake", ".cache", "build", "workspaces", "__pycache__"))
+    for name, content in contents.items():
+        (target / name).write_bytes(content)
+    return target
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("toolchain")
+    mode = parser.add_mutually_exclusive_group(required=True)
+    mode.add_argument("--destination", type=Path)
+    mode.add_argument("--apply", action="store_true")
+    args = parser.parse_args()
+    try:
+        print(prepare(ROOT, args.toolchain, args.destination))
+    except (OSError, ValueError, KeyError) as error:
+        parser.exit(1, f"prepare_toolchain: {error}\n")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/scripts/select_ci_problems.py b/scripts/select_ci_problems.py
index 178800bff..85e439a85 100644
--- a/scripts/select_ci_problems.py
+++ b/scripts/select_ci_problems.py
@@ -186,6 +186,11 @@ def is_full_catalog_sentinel(path: str) -> bool:
         or path == ".github/workflows/ci.yml"
         or path == "manifests/tags.toml"
         or path == "scripts/select_ci_problems.py"
+        or path == "scripts/prepare_toolchain.py"
+        or path == "scripts/prepare_ci_dependencies.py"
+        or path == "scripts/select_submission_toolchain.py"
+        or path == "supported-toolchains.json"
+        or path.startswith("toolchains/")
         or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"}
     )
 
@@ -205,7 +210,8 @@ def select(
 
     changed_paths = [path for change in changes for path in change.paths]
     source_changed = any(
-        path.startswith(("LeanEval/", "EvalTools/", "templates/", "manifests/"))
+        path.startswith(("LeanEval/", "EvalTools/", "templates/", "manifests/", "toolchains/"))
+        or path in {"supported-toolchains.json", "scripts/prepare_toolchain.py"}
         or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"}
         for path in changed_paths
     )
diff --git a/scripts/select_submission_toolchain.py b/scripts/select_submission_toolchain.py
new file mode 100644
index 000000000..8f073f102
--- /dev/null
+++ b/scripts/select_submission_toolchain.py
@@ -0,0 +1,149 @@
+#!/usr/bin/env python3
+"""Read toolchain requests from archived source without extracting or executing it.
+
+The closest lean-toolchain at or above each submitted workspace selects an
+approved benchmark configuration. Missing pins use the default. One archive
+must select one toolchain. Archive mode retains invalid requests using the
+default; evaluation rejects them after the source has been durably archived.
+"""
+from __future__ import annotations
+
+import argparse
+from pathlib import Path, PurePosixPath
+import subprocess
+import sys
+import tarfile
+import tomllib
+
+from prepare_toolchain import ROOT, configurations, prepare
+
+
+class ToolchainRequestError(ValueError):
+    """Archived source cannot select an approved evaluation configuration."""
+
+
+def source_requests(archive: Path, root: Path, default: str,
+                    problem: str | None = None) -> dict[str, str | None]:
+    known = {p.stem for p in (root / "manifests/problems").glob("*.toml")}
+    if problem is not None:
+        if problem not in known:
+            raise ValueError(f"unknown problem: {problem}")
+        known = {problem}
+    pins: dict[PurePosixPath, str | ValueError] = {}
+    workspaces: dict[PurePosixPath, str] = {}
+    submissions: dict[PurePosixPath, bytes | None] = {}
+    # Sequential traversal also handles compressed archives without creating
+    # a second extracted copy alongside the encrypted archive job's source.
+    seen = set()
+    with tarfile.open(archive, mode="r|gz") as source:
+        for member in source:
+            path = PurePosixPath(member.name)
+            if path.is_absolute() or ".." in path.parts:
+                raise ValueError("source archive contains an escaping path")
+            if path.name not in {"lean-toolchain", "lakefile.toml", "Submission.lean"}:
+                continue
+            if path in seen:
+                raise ValueError(f"duplicate source configuration: {path}")
+            seen.add(path)
+            if not member.isfile():
+                if path.name == "lean-toolchain":
+                    pins[path.parent] = ValueError(f"lean-toolchain must be a regular file: {path}")
+                continue
+            handle = source.extractfile(member)
+            if path.name == "lean-toolchain":
+                if member.size > 256:
+                    pins[path.parent] = ValueError(f"oversized lean-toolchain: {path}")
+                    continue
+                try:
+                    pins[path.parent] = handle.read().decode("ascii").strip()
+                except UnicodeError:
+                    pins[path.parent] = ValueError(f"lean-toolchain is not ASCII: {path}")
+            elif path.name == "lakefile.toml":
+                if member.size > 1024 * 1024:
+                    continue
+                try:
+                    name = tomllib.loads(handle.read().decode("utf-8")).get("name")
+                except (ValueError, UnicodeError):
+                    continue
+                if isinstance(name, str) and name in known:
+                    workspaces[path.parent] = name
+            else:
+                # Stubs are small. Larger submissions can never equal a
+                # pristine stub, so do not retain their contents in memory.
+                submissions[path.parent] = handle.read(65537)
+    result = {}
+    for directory, name in workspaces.items():
+        if directory not in submissions:
+            continue
+        stub = root / "generated" / name / "Submission.lean"
+        if stub.is_file() and submissions[directory] == stub.read_bytes():
+            continue
+        requested = next((pins[parent] for parent in [directory, *directory.parents]
+                          if parent in pins), None)
+        if isinstance(requested, ValueError):
+            raise requested
+        previous = result.get(name)
+        if name in result and (default if previous is None else previous) != (
+                default if requested is None else requested):
+            raise ValueError(f"multiple toolchains requested for {name}")
+        result[name] = requested
+    return result
+
+
+def select(archive: Path, root: Path, problem: str | None = None) -> tuple[str, list[str]]:
+    default, supported = configurations(root)
+    try:
+        requests = source_requests(archive, root, default, problem)
+    except Exception as error:
+        # TOML and archive readers can also raise RecursionError or resource
+        # errors on malformed source. No source parser failure may block its
+        # archival, and evaluation treats it as a terminal input rejection.
+        raise ToolchainRequestError(str(error)) from error
+    requested = {pin if pin is not None else default for pin in requests.values()}
+    if not requested:
+        requested = {default}
+    if len(requested) != 1:
+        raise ToolchainRequestError("one submission must use one toolchain; submit the workspaces separately")
+    toolchain = requested.pop()
+    if toolchain not in supported:
+        raise ToolchainRequestError(f"unsupported requested toolchain {toolchain!r}; choose {', '.join(supported)}")
+    return toolchain, sorted(requests)
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--source-tar", required=True, type=Path)
+    parser.add_argument("--problem")
+    parser.add_argument("--archive", action="store_true")
+    parser.add_argument("--expected")
+    parser.add_argument("--apply", action="store_true")
+    parser.add_argument("--regenerate", action="store_true")
+    args = parser.parse_args()
+    try:
+        try:
+            toolchain, problems = select(args.source_tar, ROOT, args.problem)
+        except ToolchainRequestError as error:
+            if not args.archive:
+                raise
+            print(f"Retaining invalid toolchain request for evaluation to reject: {error}", file=sys.stderr)
+            toolchain, problems = configurations(ROOT)[0], []
+        if args.expected is not None and args.expected != toolchain:
+            raise ValueError("source toolchain disagrees with the archived evaluation toolchain")
+        if args.apply:
+            prepare(ROOT, toolchain)
+        if args.regenerate:
+            if (ROOT / "lean-toolchain").read_text().strip() != toolchain:
+                raise ValueError("select the requested configuration before regenerating")
+            for problem in problems:
+                subprocess.run(["lake", "exe", "lean-eval", "generate", "--problem", problem],
+                               cwd=ROOT, check=True, stdout=sys.stderr)
+        print(toolchain)
+    except ToolchainRequestError as error:
+        parser.exit(3, f"select_submission_toolchain: {error}\n")
+    except (OSError, ValueError, UnicodeError, tarfile.TarError, subprocess.CalledProcessError) as error:
+        parser.exit(1, f"select_submission_toolchain: {error}\n")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/solution-dependencies.json b/solution-dependencies.json
index d7a619eee..eca594726 100644
--- a/solution-dependencies.json
+++ b/solution-dependencies.json
@@ -1 +1,27 @@
-[{"name": "lean-pool", "moduleRoots": ["LeanPool", "Challenge", "Solution"]}]
+[
+  {
+    "name": "lean-pool",
+    "moduleRoots": [
+      "LeanPool",
+      "Challenge",
+      "Solution"
+    ]
+  },
+  {
+    "name": "cfsg",
+    "moduleRoots": [
+      "CFSG",
+      "CFSGWithCertificates",
+      "Certificates",
+      "Comparator"
+    ]
+  },
+  {
+    "name": "Stacks",
+    "moduleRoots": [
+      "Stacks",
+      "StacksCore",
+      "StacksFrontier"
+    ]
+  }
+]
diff --git a/supported-toolchains.json b/supported-toolchains.json
new file mode 100644
index 000000000..c009fc34b
--- /dev/null
+++ b/supported-toolchains.json
@@ -0,0 +1,8 @@
+{
+  "default": "leanprover/lean4:v4.36.0-rc2",
+  "configurations": {
+    "leanprover/lean4:v4.36.0-rc2": "toolchains/v4.36.0-rc2",
+    "leanprover/lean4:v4.35.0": "toolchains/v4.35.0"
+  },
+  "stable": "leanprover/lean4:v4.35.0"
+}
diff --git a/tests/python/test_fetch_dependency_caches.py b/tests/python/test_fetch_dependency_caches.py
index 81d37dfa7..986fb8ede 100644
--- a/tests/python/test_fetch_dependency_caches.py
+++ b/tests/python/test_fetch_dependency_caches.py
@@ -8,6 +8,7 @@
 import sys
 import tempfile
 import unittest
+import tomllib
 
 
 ROOT = pathlib.Path(__file__).resolve().parents[2]
@@ -26,8 +27,10 @@ def setUp(self):
                                  {"name": "mathlib", "rev": "2" * 40}]}
         for path in [self.project, package]:
             (path / "lake-manifest.json").write_text(json.dumps(manifest))
-            (path / "lean-toolchain").write_text("leanprover/lean4:v4.35.0-rc3\n")
+            (path / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text())
         (self.project / "Main.lean").write_text("import TauCeti.Example\n")
+        (package / "TauCeti").mkdir()
+        (package / "TauCeti/Example.lean").write_text("def example := 1\n")
         self.calls = self.root / "calls.jsonl"
         tools = self.root / "bin"
         tools.mkdir()
@@ -37,13 +40,13 @@ def setUp(self):
             f"calls=pathlib.Path({str(self.calls)!r})\n"
             "previous=calls.read_text().splitlines() if calls.exists() else []\n"
             "with calls.open('a') as f: f.write(json.dumps({'args':sys.argv[1:],"
-            "'curl':os.environ.get('CURL')})+'\\n')\n"
+            "'curl':os.environ.get('CURL'), 'config':pathlib.Path(os.environ['LAKE_CONFIG']).read_text()})+'\\n')\n"
             "if 'build' in sys.argv:\n"
             " count=sum('build' in json.loads(p)['args'] for p in previous)\n"
             " if count < int(os.environ.get('FAIL_RESTORES','0')):\n"
             "  print('curl: (22) artifact service returned 503')\n"
             "  sys.exit(3)\n"
-            " print('Fetched TauCeti.Example')\n"
+            " print(os.environ.get('BUILD_MESSAGE', 'Fetched TauCeti.Example'))\n"
         )
         (tools / "lake").chmod(0o755)
         (tools / "sleep").write_text("#!/bin/sh\nexit 0\n")
@@ -52,9 +55,11 @@ def setUp(self):
                         GITHUB_ENV="", RUNNER_TEMP=str(self.root))
 
     def run_script(self, failures):
+        # Include Lean's parser startup and the deliberately exercised retry
+        # backoff, including on small hosted runners or a busy development host.
         return subprocess.run(["bash", str(SCRIPT), "--restore", str(self.project)],
                               env=dict(self.env, FAIL_RESTORES=str(failures)),
-                              capture_output=True, text=True, check=False, timeout=10)
+                              capture_output=True, text=True, check=False, timeout=90)
 
     def test_retries_cache_only_restore_and_exports_wrapper_for_later_builds(self):
         result = self.run_script(1)
@@ -86,5 +91,120 @@ def test_pin_mismatch_stops_before_any_lake_command(self):
         self.assertFalse(self.calls.exists())
 
 
+    def add_library(self, name, dependencies=None):
+        path = self.project / ".lake/packages" / name
+        path.mkdir(parents=True)
+        root_manifest = json.loads((self.project / "lake-manifest.json").read_text())
+        root_manifest["packages"].append({"name": name, "rev": "3" * 40})
+        (self.project / "lake-manifest.json").write_text(json.dumps(root_manifest))
+        (path / "lake-manifest.json").write_text(json.dumps({"packages": dependencies or [
+            {"name": "mathlib", "rev": "2" * 40}]}))
+        (path / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text())
+        for module in {"cfsg": ["CFSG", "CFSG/Real", "CFSG/Example", "Certificates/Data/Example"],
+                       "Stacks": ["Stacks", "StacksCore/Example", "StacksFrontier/Example"]}.get(name, []):
+            source = path / (module + ".lean")
+            source.parent.mkdir(parents=True, exist_ok=True)
+            source.write_text("def example := 1\n")
+        return path
+
+    def test_multiple_caches_and_transitive_tauceti_use_distinct_services(self):
+        self.add_library("cfsg", [{"name": "mathlib", "rev": "2" * 40},
+                                  {"name": "TauCeti", "rev": "1" * 40}])
+        self.add_library("Stacks")
+        self.env.update(STACKS_ARTIFACT_ENDPOINT="https://stacks.example/artifacts",
+                        STACKS_REVISION_ENDPOINT="https://stacks.example/revisions")
+        (self.project / "Main.lean").write_text(
+            "module\n/- outer /- import CFSG.Fake -/ comment -/\n"
+            "public import\n  CFSG.Real\nimport Certificates.Data.Example\n"
+            "meta import all StacksCore.Example\nimport StacksFrontier.Example\n")
+        result = self.run_script(0)
+        self.assertEqual(result.returncode, 0, result.stderr)
+        calls = [json.loads(line) for line in self.calls.read_text().splitlines()]
+        mappings = [c for c in calls if "cache" in c["args"]]
+        self.assertEqual({c["args"][c["args"].index("--package") + 1] for c in mappings},
+                         {"cfsg", "Stacks", "TauCeti"})
+        config = tomllib.loads(calls[0]["config"])
+        self.assertEqual({s["name"] for s in config["cache"]["service"]},
+                         {"cfsg-public", "stacks-public", "tauceti-public"})
+        build = next(c["args"] for c in calls if "build" in c["args"])
+        self.assertIn("+CFSG.Real", build)
+        self.assertIn("+Certificates.Data.Example", build)
+        self.assertIn("+StacksCore.Example", build)
+        self.assertIn("+StacksFrontier.Example", build)
+        self.assertNotIn("+CFSG.Fake", build)
+
+    def test_unused_libraries_need_no_cache_or_matching_toolchain(self):
+        stacks = self.add_library("Stacks")
+        (stacks / "lean-toolchain").write_text("leanprover/lean4:v4.34.0\n")
+        (self.project / "Main.lean").write_text("import Mathlib\n")
+        result = self.run_script(0)
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertEqual(result.stdout, "")
+        self.assertFalse(self.calls.exists())
+
+    def test_parsing_submission_headers_never_executes_solver_code(self):
+        marker = self.root / "solver-code-ran"
+        (self.project / "Main.lean").write_text(
+            f'import Lean\n#eval IO.FS.writeFile {json.dumps(str(marker))} "executed"\n')
+        result = self.run_script(0)
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertFalse(marker.exists())
+        self.assertFalse(self.calls.exists())
+
+    def test_bad_solver_imports_are_left_to_comparator_without_running_lake(self):
+        for header in ["import TauCeti.\n", "import TauCeti.Missing\n",
+                       "import TauCeti.«../../Submission/Evil»\n"]:
+            with self.subTest(header=header):
+                (self.project / "Main.lean").write_text(header)
+                result = self.run_script(0)
+                self.assertEqual(result.returncode, 0, result.stderr)
+                self.assertFalse(self.calls.exists())
+
+    def test_transitive_pin_mismatch_is_rejected_before_fetching(self):
+        self.add_library("cfsg", [{"name": "mathlib", "rev": "2" * 40},
+                                  {"name": "TauCeti", "rev": "0" * 40}])
+        (self.project / "Main.lean").write_text("import CFSG.Example\n")
+        result = self.run_script(0)
+        self.assertNotEqual(result.returncode, 0)
+        self.assertIn("Different dependency pins: TauCeti", result.stderr)
+        self.assertFalse(self.calls.exists())
+
+    def test_stacks_uses_published_endpoints_with_empty_workflow_overrides(self):
+        self.add_library("Stacks")
+        self.env.update(STACKS_ARTIFACT_ENDPOINT="", STACKS_REVISION_ENDPOINT="")
+        (self.project / "Main.lean").write_text("import Stacks\n")
+        result = self.run_script(0)
+        self.assertEqual(result.returncode, 0, result.stderr)
+        calls = [json.loads(line) for line in self.calls.read_text().splitlines()]
+        service = tomllib.loads(calls[0]["config"])["cache"]["service"][0]
+        self.assertEqual(service["artifactEndpoint"],
+                         "https://stacks-cache.axiommath.workers.dev/lake/artifacts")
+        self.assertEqual(service["revisionEndpoint"],
+                         "https://stacks-cache.axiommath.workers.dev/lake/revisions")
+
+    def test_missing_checkout_fails_before_fetching(self):
+        self.add_library("Stacks")
+        (self.project / ".lake/packages/Stacks/lake-manifest.json").unlink()
+        (self.project / "Main.lean").write_text("import Stacks\n")
+        result = self.run_script(0)
+        self.assertNotEqual(result.returncode, 0)
+        self.assertIn("fetch the dependencies first", result.stderr)
+        self.assertFalse(self.calls.exists())
+
+    def test_github_environment_and_no_build_defense(self):
+        environment = self.root / "github-env"
+        self.env["GITHUB_ENV"] = str(environment)
+        result = self.run_script(0)
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertEqual(result.stdout, "")
+        self.assertIn("LAKE_CONFIG=", environment.read_text())
+        self.env["BUILD_MESSAGE"] = "Built TauCeti.Example"
+        environment.unlink()
+        result = self.run_script(0)
+        self.assertNotEqual(result.returncode, 0)
+        self.assertIn("compiled instead of downloaded", result.stderr)
+        self.assertFalse(environment.exists())
+
+
 if __name__ == "__main__":
     unittest.main()
diff --git a/tests/python/test_lake_cache_restore.py b/tests/python/test_lake_cache_restore.py
index 34493ead9..d8ee9ab95 100644
--- a/tests/python/test_lake_cache_restore.py
+++ b/tests/python/test_lake_cache_restore.py
@@ -25,8 +25,11 @@ def test_failed_download_can_be_retried_without_compilation_or_poisoned_cache(se
             (root / "lakefile.toml").write_text(
                 'name = "cache-probe"\ndefaultTargets = ["CacheProbe"]\n'
                 '[[lean_lib]]\nname = "CacheProbe"\n'
+                '[[lean_lib]]\nname = "Precompiled"\nprecompileModules = true\n'
             )
-            (root / "CacheProbe.lean").write_text("def cacheProbe : Nat := 42\n")
+            (root / "Precompiled.lean").write_text("def precompiledValue : Nat := 41\n")
+            (root / "CacheProbe.lean").write_text(
+                "import Precompiled\ndef cacheProbe : Nat := precompiledValue + 1\n")
             (root / "UseCacheProbe.lean").write_text(
                 "import CacheProbe\nexample : cacheProbe = 42 := rfl\n"
             )
@@ -71,6 +74,10 @@ def lake(*args):
                 self.assertEqual(built.returncode, 0, built.stdout + built.stderr)
                 artifacts = cache / "artifacts"
                 self.assertTrue(list(artifacts.glob("*.olean")))
+                # CFSG uses precompiled libraries. Their linked native outputs
+                # must also restore without invoking a compiler or linker.
+                self.assertTrue(any(p.suffix in {".so", ".dylib", ".dll"}
+                                    for p in artifacts.iterdir()))
                 payloads.update({p.stem: p.read_bytes() for p in artifacts.iterdir()})
                 # Remote mappings imported by `lake cache get --mappings-only`
                 # bind their service and scope; locally produced mappings do not.
@@ -84,16 +91,17 @@ def lake(*args):
                 thread = threading.Thread(target=server.serve_forever, daemon=True)
                 thread.start()
                 try:
-                    failed = lake("-v", "--no-build", "build")
+                    failed = lake("-v", "--no-build", "build", "+CacheProbe")
                     self.assertNotEqual(failed.returncode, 0)
                     self.assertIn("curl", failed.stdout + failed.stderr)
                     self.assertTrue(requests)
                     self.assertFalse((root / ".lake/build/lib/lean/CacheProbe.olean").exists())
                     self.assertEqual(list(artifacts.iterdir()), [])
                     healthy = True
-                    restored = lake("-v", "--no-build", "build")
+                    restored = lake("-v", "--no-build", "build", "+CacheProbe")
                     self.assertEqual(restored.returncode, 0, restored.stdout + restored.stderr)
                     self.assertNotIn("Built CacheProbe", restored.stdout + restored.stderr)
+                    self.assertNotIn("Built Precompiled", restored.stdout + restored.stderr)
                     checked = lake("env", "lean", "UseCacheProbe.lean")
                     self.assertEqual(checked.returncode, 0, checked.stdout + checked.stderr)
                 finally:
diff --git a/tests/python/test_prepare_ci_dependencies.py b/tests/python/test_prepare_ci_dependencies.py
new file mode 100644
index 000000000..4b28909ae
--- /dev/null
+++ b/tests/python/test_prepare_ci_dependencies.py
@@ -0,0 +1,60 @@
+from __future__ import annotations
+
+import importlib.util
+import json
+from pathlib import Path
+import subprocess
+import tempfile
+import unittest
+
+
+ROOT = Path(__file__).resolve().parents[2]
+SPEC = importlib.util.spec_from_file_location("prepare_ci_dependencies",
+                                            ROOT / "scripts/prepare_ci_dependencies.py")
+MODULE = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(MODULE)
+
+
+class PrepareCIDependenciesTests(unittest.TestCase):
+    def test_pinned_metadata_is_real_and_solution_sources_are_not_materialized(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            source = root / "source"
+            source.mkdir()
+            subprocess.run(["git", "init", "--quiet", "--initial-branch=main", str(source)], check=True)
+            subprocess.run(["git", "-C", str(source), "config", "uploadpack.allowFilter", "true"], check=True)
+            (source / "lakefile.toml").write_text('name = "example"\n')
+            (source / "lake-manifest.json").write_text('{"packages": []}\n')
+            (source / "lean-toolchain").write_text("leanprover/lean4:v4.35.0\n")
+            (source / "Example.lean").write_text("def largeSolutionLibrary := 42\n")
+            subprocess.run(["git", "-C", str(source), "add", "."], check=True)
+            subprocess.run(["git", "-C", str(source), "-c", "user.name=Tests", "-c",
+                            "user.email=tests@example.invalid", "commit", "--quiet", "-m", "fixture"],
+                           check=True)
+            revision = subprocess.check_output(["git", "-C", str(source), "rev-parse", "HEAD"],
+                                               text=True).strip()
+            (root / "solution-dependencies.json").write_text(json.dumps([
+                {"name": name} for name in MODULE.PACKAGES]))
+            (root / "lake-manifest.json").write_text(json.dumps({"packages": [
+                {"name": name, "url": str(source), "rev": revision} for name in MODULE.PACKAGES]}))
+            MODULE.prepare(root)
+            for name in MODULE.PACKAGES:
+                package = root / ".lake/packages" / name
+                self.assertEqual((package / "lakefile.toml").read_bytes(),
+                                 (source / "lakefile.toml").read_bytes())
+                self.assertFalse((package / "Example.lean").exists())
+                self.assertEqual(subprocess.check_output(
+                    ["git", "-C", str(package), "rev-parse", "HEAD"], text=True).strip(), revision)
+            with self.assertRaisesRegex(ValueError, "fresh CI checkout"):
+                MODULE.prepare(root)
+
+    def test_only_solution_only_packages_may_have_their_sources_omitted(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            (root / "solution-dependencies.json").write_text("[]")
+            with self.assertRaisesRegex(ValueError, "trusted statement imports"):
+                MODULE.prepare(root)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_prepare_toolchain.py b/tests/python/test_prepare_toolchain.py
new file mode 100644
index 000000000..b2e566aab
--- /dev/null
+++ b/tests/python/test_prepare_toolchain.py
@@ -0,0 +1,76 @@
+from __future__ import annotations
+
+import importlib.util
+import json
+from pathlib import Path
+import tempfile
+import tomllib
+import unittest
+
+
+ROOT = Path(__file__).resolve().parents[2]
+SPEC = importlib.util.spec_from_file_location("prepare_toolchain", ROOT / "scripts/prepare_toolchain.py")
+MODULE = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(MODULE)
+
+
+class PrepareToolchainTests(unittest.TestCase):
+    def test_published_configurations_have_matching_dependency_pins(self):
+        default, profiles = MODULE.configurations(ROOT)
+        self.assertEqual(default, (ROOT / "lean-toolchain").read_text().strip())
+        self.assertEqual(set(profiles), {"leanprover/lean4:v4.35.0", default})
+        for name in MODULE.FILES:
+            self.assertEqual((profiles[default] / name).read_bytes(), (ROOT / name).read_bytes())
+        for profile in profiles.values():
+            lakefile = tomllib.loads((profile / "lakefile.toml").read_text())
+            packages = {p["name"].strip("«»"): p for p in json.loads(
+                (profile / "lake-manifest.json").read_text())["packages"]}
+            for dependency in lakefile["require"]:
+                self.assertEqual(dependency["rev"], packages[dependency["name"]]["rev"])
+
+    def fixture(self, root):
+        for relative, pin in [(".", "leanprover/lean4:v4.36.0-rc2"),
+                              ("stable", "leanprover/lean4:v4.35.0")]:
+            profile = root / relative
+            profile.mkdir(exist_ok=True)
+            (profile / "lean-toolchain").write_text(pin + "\n")
+            (profile / "lakefile.toml").write_text(relative)
+            (profile / "lake-manifest.json").write_text(relative)
+        (root / "supported-toolchains.json").write_text(json.dumps({
+            "default": "leanprover/lean4:v4.36.0-rc2", "stable": "leanprover/lean4:v4.35.0",
+            "configurations": {
+                "leanprover/lean4:v4.36.0-rc2": ".", "leanprover/lean4:v4.35.0": "stable"}}))
+
+    def test_isolated_copy_selects_stable_and_excludes_build_state(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary) / "benchmark"
+            root.mkdir()
+            self.fixture(root)
+            (root / ".lake").mkdir()
+            (root / ".lake/secret-cache").write_text("old artifacts")
+            destination = root / ".lake/stable-copy"
+            MODULE.prepare(root, "stable", destination)
+            self.assertEqual((destination / "lakefile.toml").read_text(), "stable")
+            self.assertFalse((destination / ".lake").exists())
+            self.assertEqual((root / "lakefile.toml").read_text(), ".")
+            with self.assertRaisesRegex(ValueError, "already exists"):
+                MODULE.prepare(root, "stable", destination)
+            with self.assertRaisesRegex(ValueError, "fresh checkout"):
+                MODULE.prepare(root, "stable")
+
+    def test_unsupported_toolchains_and_escaping_configurations_are_rejected(self):
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            self.fixture(root)
+            with self.assertRaisesRegex(ValueError, "unsupported"):
+                MODULE.prepare(root, "leanprover/lean4:nightly")
+            registry = root / "supported-toolchains.json"
+            value = json.loads(registry.read_text())
+            value["configurations"][value["default"]] = "../outside"
+            registry.write_text(json.dumps(value))
+            with self.assertRaisesRegex(ValueError, "escapes"):
+                MODULE.prepare(root, "stable")
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/tests/python/test_select_ci_problems.py b/tests/python/test_select_ci_problems.py
index 5f7c14efe..a6d5a9ff3 100644
--- a/tests/python/test_select_ci_problems.py
+++ b/tests/python/test_select_ci_problems.py
@@ -82,6 +82,15 @@ def test_solution_dependency_change_regenerates_every_workspace(self):
         self.assertEqual(selection.mode, "full")
         self.assertTrue(selection.source_changed)
 
+    def test_toolchain_configuration_changes_compile_the_full_catalog(self):
+        for path in ["supported-toolchains.json", "toolchains/v4.35.0/lake-manifest.json",
+                     "scripts/prepare_toolchain.py", "scripts/select_submission_toolchain.py",
+                     "scripts/prepare_ci_dependencies.py"]:
+            with self.subTest(path=path):
+                selection = self.select((Change("M", (path,)),))
+                self.assertEqual(selection.mode, "full")
+                self.assertEqual(selection.problems, ("a", "b", "b_second", "c"))
+
     def test_tag_registry_change_is_a_full_catalog_sentinel(self):
         selection = self.select((Change("M", ("manifests/tags.toml",)),))
         self.assertEqual(selection.mode, "full")
diff --git a/tests/python/test_select_submission_toolchain.py b/tests/python/test_select_submission_toolchain.py
new file mode 100644
index 000000000..5162a7f1f
--- /dev/null
+++ b/tests/python/test_select_submission_toolchain.py
@@ -0,0 +1,127 @@
+from __future__ import annotations
+
+import importlib.util
+import io
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tarfile
+import tempfile
+import unittest
+from unittest import mock
+
+
+ROOT = Path(__file__).resolve().parents[2]
+sys.path.insert(0, str(ROOT / "scripts"))
+SPEC = importlib.util.spec_from_file_location("select_submission_toolchain",
+                                            ROOT / "scripts/select_submission_toolchain.py")
+MODULE = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(MODULE)
+
+
+class SelectSubmissionToolchainTests(unittest.TestCase):
+    def setUp(self):
+        temporary = tempfile.TemporaryDirectory()
+        self.addCleanup(temporary.cleanup)
+        self.root = Path(temporary.name)
+        (self.root / "manifests/problems").mkdir(parents=True)
+        for problem in ("a", "b"):
+            (self.root / f"manifests/problems/{problem}.toml").write_text("")
+            (self.root / f"generated/{problem}").mkdir(parents=True)
+            (self.root / f"generated/{problem}/Submission.lean").write_text("-- stub\n")
+        for relative, pin in [("rc", "v4.36.0-rc2"), ("stable", "v4.35.0")]:
+            profile = self.root / relative
+            profile.mkdir()
+            for name in ["lean-toolchain", "lakefile.toml", "lake-manifest.json"]:
+                (profile / name).write_text("leanprover/lean4:" + pin if name == "lean-toolchain" else "{}")
+        (self.root / "supported-toolchains.json").write_text(json.dumps({
+            "default": "leanprover/lean4:v4.36.0-rc2", "stable": "leanprover/lean4:v4.35.0",
+            "configurations": {
+                "leanprover/lean4:v4.36.0-rc2": "rc", "leanprover/lean4:v4.35.0": "stable"}}))
+
+    def archive(self, files):
+        archive = self.root / "source.tar.gz"
+        with tarfile.open(archive, "w:gz") as output:
+            for name, value in files:
+                member = tarfile.TarInfo(name)
+                if value is None:
+                    member.type = tarfile.SYMTYPE
+                    member.linkname = "/etc/passwd"
+                    output.addfile(member)
+                else:
+                    data = value.encode()
+                    member.size = len(data)
+                    output.addfile(member, io.BytesIO(data))
+        return archive
+
+    def workspace(self, problem="a", prefix="source/generated/a"):
+        return [(prefix + "/lakefile.toml", f'name = "{problem}"'),
+                (prefix + "/Submission.lean", "-- proof\n")]
+
+    def test_root_pin_and_nearest_workspace_pin_select_approved_configurations(self):
+        files = [("source/lean-toolchain", "leanprover/lean4:v4.35.0")] + self.workspace()
+        selected, problems = MODULE.select(self.archive(files), self.root)
+        self.assertEqual(selected, "leanprover/lean4:v4.35.0")
+        self.assertEqual(problems, ["a"])
+        files.append(("source/generated/a/lean-toolchain", "leanprover/lean4:v4.36.0-rc2"))
+        self.assertEqual(MODULE.select(self.archive(files), self.root)[0],
+                         "leanprover/lean4:v4.36.0-rc2")
+
+    def test_pristine_workspaces_and_other_selected_problems_do_not_choose_toolchains(self):
+        files = self.workspace() + [("source/generated/a/lean-toolchain", "leanprover/lean4:v4.35.0")]
+        files += self.workspace("b", "source/generated/b")
+        files += [("source/generated/b/lean-toolchain", "leanprover/lean4:v4.36.0-rc2")]
+        archive = self.archive(files)
+        with self.assertRaisesRegex(ValueError, "one toolchain"):
+            MODULE.select(archive, self.root)
+        self.assertEqual(MODULE.select(archive, self.root, "a")[0], "leanprover/lean4:v4.35.0")
+        files = [(path, "-- stub\n" if path == "source/generated/b/Submission.lean" else content)
+                 for path, content in files]
+        self.assertEqual(MODULE.select(self.archive(files), self.root)[1], ["a"])
+
+    def test_an_implicit_and_explicit_default_are_the_same_configuration(self):
+        files = self.workspace() + self.workspace("a", "source/another-a")
+        files.append(("source/another-a/lean-toolchain", "leanprover/lean4:v4.36.0-rc2"))
+        self.assertEqual(MODULE.select(self.archive(files), self.root),
+                         ("leanprover/lean4:v4.36.0-rc2", ["a"]))
+
+    def test_unsupported_pins_escaping_paths_symlinks_and_duplicates_fail_closed(self):
+        cases = [self.workspace() + [("source/lean-toolchain", "leanprover/lean4:nightly")],
+                 [("../lean-toolchain", "ignored")], self.workspace() + [("source/lean-toolchain", None)],
+                 [("source/lean-toolchain", "a"), ("source/lean-toolchain", "b")],
+                 self.workspace() + [("source/lean-toolchain", "a" * 257)]]
+        for files in cases:
+            with self.subTest(files=files), self.assertRaises(ValueError):
+                MODULE.select(self.archive(files), self.root)
+
+    def test_archive_retains_unsupported_requests_but_evaluation_rejects_them(self):
+        scripts = self.root / "scripts"
+        scripts.mkdir()
+        for name in ["prepare_toolchain.py", "select_submission_toolchain.py"]:
+            shutil.copyfile(ROOT / "scripts" / name, scripts / name)
+        archive = self.archive(self.workspace() + [
+            ("source/lean-toolchain", "leanprover/lean4:nightly")])
+        command = [sys.executable, str(scripts / "select_submission_toolchain.py"),
+                   "--source-tar", str(archive)]
+        archived = subprocess.run([*command, "--archive"], capture_output=True, text=True)
+        self.assertEqual(archived.returncode, 0, archived.stderr)
+        self.assertEqual(archived.stdout.strip(), "leanprover/lean4:v4.36.0-rc2")
+        evaluated = subprocess.run([*command, "--expected", archived.stdout.strip()],
+                                   capture_output=True, text=True)
+        self.assertNotEqual(evaluated.returncode, 0)
+        self.assertIn("unsupported requested toolchain", evaluated.stderr)
+
+    def test_parser_recursion_is_an_input_rejection_and_unused_symlinks_are_ignored(self):
+        with mock.patch.object(MODULE, "source_requests", side_effect=RecursionError("nested TOML")):
+            with self.assertRaises(MODULE.ToolchainRequestError):
+                MODULE.select(self.root / "source.tar.gz", self.root)
+        files = self.workspace() + [("source/lean-toolchain", "leanprover/lean4:v4.35.0"),
+                                    ("source/vendor/lakefile.toml", None),
+                                    ("source/vendor/lean-toolchain", None)]
+        self.assertEqual(MODULE.select(self.archive(files), self.root)[0], "leanprover/lean4:v4.35.0")
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/toolchains/v4.35.0/lake-manifest.json b/toolchains/v4.35.0/lake-manifest.json
new file mode 100644
index 000000000..50c8e82ba
--- /dev/null
+++ b/toolchains/v4.35.0/lake-manifest.json
@@ -0,0 +1,177 @@
+{
+  "version": "1.3.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "074063781836922cb02701cd12943c9f51731afa",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "074063781836922cb02701cd12943c9f51731afa",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "4a174c490d8707121c4a9290800489f105d85e07",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.35.0",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean-eval-generator.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
+      "name": "\u00ablean-eval-generator\u00bb",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/TauCetiProject/TauCeti",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "1f9b4414105d86e487a4ac4c3d3397076a44d0d2",
+      "name": "TauCeti",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "1f9b4414105d86e487a4ac4c3d3397076a44d0d2",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/AxiomMath/Stacks.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+      "name": "Stacks",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/AxiomMath/CFSG.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
+      "name": "cfsg",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/Vilin97/lean-pool.git",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f",
+      "name": "\u00ablean-pool\u00bb",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f",
+      "inherited": false,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "\u00ablean-eval\u00bb",
+  "lakeDir": ".lake",
+  "fixedToolchain": false
+}
diff --git a/toolchains/v4.35.0/lakefile.toml b/toolchains/v4.35.0/lakefile.toml
new file mode 100644
index 000000000..8be7b072e
--- /dev/null
+++ b/toolchains/v4.35.0/lakefile.toml
@@ -0,0 +1,87 @@
+name = "lean-eval"
+defaultTargets = ["LeanEval"]
+# Generated benchmark statements retain legacy visibility rules.
+allowNonModules = true
+
+[leanOptions]
+autoImplicit = false
+
+# Available to generated solutions only. Generation rejects statement imports
+# from lean-pool; keep this before Mathlib so Mathlib owns shared pins.
+[[require]]
+name = "lean-pool"
+git = "https://github.com/Vilin97/lean-pool.git"
+rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f"
+
+# Large solution libraries. Their caches are fetched only when imported.
+# Keep these before TauCeti and Mathlib so the benchmark owns shared pins.
+# Their published pins currently predate this toolchain; cache preparation
+# rejects imports until the publishers provide matching builds (see README).
+[[require]]
+name = "cfsg"
+git = "https://github.com/AxiomMath/CFSG.git"
+rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33"
+
+[[require]]
+name = "Stacks"
+git = "https://github.com/AxiomMath/Stacks.git"
+rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b"
+
+# TauCeti supplies the definitions in the classification of finite simple groups
+# problem. It is listed before Mathlib because Lake takes shared transitive
+# dependencies (batteries, aesop, ...) from the later require, and those must be
+# Mathlib's. The toolchain and the Mathlib rev below must be exactly the ones the
+# pinned TauCeti commit uses, so that TauCeti's published build outputs apply;
+# scripts/fetch_dependency_caches.sh checks this and fetches them.
+[[require]]
+name = "TauCeti"
+git = "https://github.com/TauCetiProject/TauCeti"
+rev = "1f9b4414105d86e487a4ac4c3d3397076a44d0d2"
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "074063781836922cb02701cd12943c9f51731afa"
+
+[[require]]
+name = "lean-eval-generator"
+git = "https://github.com/leanprover/lean-eval-generator.git"
+rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4"
+
+[[lean_lib]]
+name = "LeanEval"
+
+[[lean_lib]]
+name = "EvalTools"
+
+[[lean_exe]]
+name = "extract_theorem"
+root = "EvalTools.ExtractTheorem"
+
+[[lean_exe]]
+name = "eval_inventory"
+root = "EvalTools.ProblemInventory"
+
+[[lean_exe]]
+name = "lean-eval"
+root = "EvalTools.Main"
+
+[[lean_exe]]
+name = "test_validate_submission"
+srcDir = "tests/lean"
+root = "EvalToolsTests.ValidateSubmissionTest"
+
+[[lean_exe]]
+name = "test_check_comparator_installation"
+srcDir = "tests/lean"
+root = "EvalToolsTests.CheckComparatorInstallationTest"
+
+[[lean_exe]]
+name = "test_generate"
+srcDir = "tests/lean"
+root = "EvalToolsTests.GenerateTest"
+
+[[lean_exe]]
+name = "test_module_coverage"
+srcDir = "tests/lean"
+root = "EvalToolsTests.ModuleCoverageTest"
diff --git a/toolchains/v4.35.0/lean-toolchain b/toolchains/v4.35.0/lean-toolchain
new file mode 100644
index 000000000..a6aff065d
--- /dev/null
+++ b/toolchains/v4.35.0/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.35.0
diff --git a/toolchains/v4.36.0-rc2/lake-manifest.json b/toolchains/v4.36.0-rc2/lake-manifest.json
new file mode 100644
index 000000000..50817ff4e
--- /dev/null
+++ b/toolchains/v4.36.0-rc2/lake-manifest.json
@@ -0,0 +1,146 @@
+{"version": "1.3.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/lean-eval-generator.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
+   "name": "«lean-eval-generator»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/TauCetiProject/TauCeti",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "be86813dc92e6bac8614c2c2dd34572145df09c0",
+   "name": "TauCeti",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "be86813dc92e6bac8614c2c2dd34572145df09c0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/AxiomMath/Stacks.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+   "name": "Stacks",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "c496df0d9beea9deaeabcea8492605f9a0a2313b",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/AxiomMath/CFSG.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
+   "name": "cfsg",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/Vilin97/lean-pool.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f",
+   "name": "«lean-pool»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "b0256621cb88178e9ad932a53633077b3029e621",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "4af7237d146261353907b06a01b6f3fc06cfa067",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.36.0-rc2",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "«lean-eval»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/toolchains/v4.36.0-rc2/lakefile.toml b/toolchains/v4.36.0-rc2/lakefile.toml
new file mode 100644
index 000000000..5e17c52ac
--- /dev/null
+++ b/toolchains/v4.36.0-rc2/lakefile.toml
@@ -0,0 +1,87 @@
+name = "lean-eval"
+defaultTargets = ["LeanEval"]
+# Generated benchmark statements retain legacy visibility rules.
+allowNonModules = true
+
+[leanOptions]
+autoImplicit = false
+
+# Available to generated solutions only. Generation rejects statement imports
+# from lean-pool; keep this before Mathlib so Mathlib owns shared pins.
+[[require]]
+name = "lean-pool"
+git = "https://github.com/Vilin97/lean-pool.git"
+rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f"
+
+# Large solution libraries. Their caches are fetched only when imported.
+# Keep these before TauCeti and Mathlib so the benchmark owns shared pins.
+# Their published pins currently predate this toolchain; cache preparation
+# rejects imports until the publishers provide matching builds (see README).
+[[require]]
+name = "cfsg"
+git = "https://github.com/AxiomMath/CFSG.git"
+rev = "5437cdc31389dd9aeaa5c2a9465a4e164f8dea33"
+
+[[require]]
+name = "Stacks"
+git = "https://github.com/AxiomMath/Stacks.git"
+rev = "c496df0d9beea9deaeabcea8492605f9a0a2313b"
+
+# TauCeti supplies the definitions in the classification of finite simple groups
+# problem. It is listed before Mathlib because Lake takes shared transitive
+# dependencies (batteries, aesop, ...) from the later require, and those must be
+# Mathlib's. The toolchain and the Mathlib rev below must be exactly the ones the
+# pinned TauCeti commit uses, so that TauCeti's published build outputs apply;
+# scripts/fetch_dependency_caches.sh checks this and fetches them.
+[[require]]
+name = "TauCeti"
+git = "https://github.com/TauCetiProject/TauCeti"
+rev = "be86813dc92e6bac8614c2c2dd34572145df09c0"
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "2ddf59c8f14245864e6c0ed227a2dab76b9efea2"
+
+[[require]]
+name = "lean-eval-generator"
+git = "https://github.com/leanprover/lean-eval-generator.git"
+rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4"
+
+[[lean_lib]]
+name = "LeanEval"
+
+[[lean_lib]]
+name = "EvalTools"
+
+[[lean_exe]]
+name = "extract_theorem"
+root = "EvalTools.ExtractTheorem"
+
+[[lean_exe]]
+name = "eval_inventory"
+root = "EvalTools.ProblemInventory"
+
+[[lean_exe]]
+name = "lean-eval"
+root = "EvalTools.Main"
+
+[[lean_exe]]
+name = "test_validate_submission"
+srcDir = "tests/lean"
+root = "EvalToolsTests.ValidateSubmissionTest"
+
+[[lean_exe]]
+name = "test_check_comparator_installation"
+srcDir = "tests/lean"
+root = "EvalToolsTests.CheckComparatorInstallationTest"
+
+[[lean_exe]]
+name = "test_generate"
+srcDir = "tests/lean"
+root = "EvalToolsTests.GenerateTest"
+
+[[lean_exe]]
+name = "test_module_coverage"
+srcDir = "tests/lean"
+root = "EvalToolsTests.ModuleCoverageTest"
diff --git a/toolchains/v4.36.0-rc2/lean-toolchain b/toolchains/v4.36.0-rc2/lean-toolchain
new file mode 100644
index 000000000..0fc433692
--- /dev/null
+++ b/toolchains/v4.36.0-rc2/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.36.0-rc2