Allow solutions to depend on Lean Pool

.github/workflows/notify-leaderboard.yml

@@ -17,6 +17,7 @@ on:
       - 'manifests/**'
       - 'generated/**'
       - 'lakefile.toml'
+      - 'solution-dependencies.json'
       - 'lean-toolchain'
   workflow_dispatch:
 

.github/workflows/regenerate-main.yml

@@ -12,6 +12,7 @@ on:
       - 'manifests/**'
       - '.github/workflows/regenerate-main.yml'
       - 'lakefile.toml'
+      - 'solution-dependencies.json'
       - 'lean-toolchain'
   workflow_dispatch:
 

EvalTools/CheckEvalWorkflow.lean

@@ -112,6 +112,17 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do
         (replaceFirst pristineSubmission "  sorry\n" "  norm_num\n").get!
       let correctSummary ← summarizeAtRoot root problems workspacesRoot
       assertCounts correctSummary 1 1 "Correct two_plus_two attempt"
+      -- Exercise the solution-only package through the real scoring path. Its
+      -- Basic module has no Mathlib imports, keeping this smoke test small.
+      -- Shared package caches are read-only inside comparator's sandbox.
+      let _ ← runCmdCheckedCaptured "lake" #["build", "LeanPool.Basic"] root
+        "Failed to prepare the Lean Pool smoke-test dependency"
+      IO.FS.writeFile (workspace / "Submission.lean")
+        ("import LeanPool.Basic\n" ++
+          (replaceFirst pristineSubmission "  sorry\n"
+            "  cases (show hello = \"world\" from rfl)\n  norm_num\n").get!)
+      let poolSummary ← summarizeAtRoot root problems workspacesRoot
+      assertCounts poolSummary 1 1 "Correct attempt importing Lean Pool"
       IO.println "Eval workflow check passed."
       IO.FS.removeDirAll tempDir
       return (0 : UInt32)

README.md

@@ -206,6 +206,12 @@ 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.
+
 ### 5. Run comparator locally
 
 ```bash

SECURITY.md

@@ -212,10 +212,12 @@ time, the upstream publisher controls our supply chain.
 
 | Dependency | Repo | Pinned to | Purpose | Last bumped |
 |---|---|---|---|---|
-| Lean toolchain | leanprover/lean4 | `v4.34.0` | compiler and Lake | 2026-09-16 |
-| mathlib | leanprover-community/mathlib4 | `db1c5741da0acf96c97584de6ccf0e3bfbc0ae99` | theorem library (the pin of TauCeti `23bfe9b`) | 2026-09-26 |
-| TauCeti | TauCetiProject/TauCeti | `23bfe9bc742f8713b58ce40b155f994848ae8a5e` | definitions used by `classification_finite_simple_groups`; oleans from its public Lake cache | 2026-09-26 |
-| lean4-cli | leanprover/lean4-cli | `e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204` | command-line parsing | 2026-09-16 |
+| Lean toolchain | leanprover/lean4 | `v4.35.0-rc3` | compiler and Lake | 2026-09-28 |
+| mathlib | leanprover-community/mathlib4 | `5e0c4e5239cb0a2d86d68a884bf52cfd963fce22` | theorem library (the pin of TauCeti `522706e`) | 2026-09-28 |
+| TauCeti | TauCetiProject/TauCeti | `522706e83ca349c3d6bde045e56778d17354ae8d` | definitions used by `classification_finite_simple_groups`; oleans from its public Lake cache | 2026-09-28 |
+| lean-pool | Vilin97/lean-pool | `e9d53e9cbcff8dfd0cc816ba94db7a26b082929f` | solution-only library; forbidden in trusted problem imports | 2026-09-28 |
+| lean-eval-generator | leanprover/lean-eval-generator | `0b8cc2d141710a18515c53448f006c971dd8eeb4` | workspace generation and solution-dependency policy | 2026-09-28 |
+| lean4-cli | leanprover/lean4-cli | `843844fa601dd56767b1eb22b7ada5b64d5e567a` | command-line parsing | 2026-09-28 |
 | landrun | zouuup/landrun | `5ed4a3db3a4ad930d577215c6b9abaa19df7f99f` | Linux landlock sandbox | 2026-05-04 |
 | lean4export | leanprover/lean4export | `076e8e57707e813375e8f9da8bf989799ace9680` | exports olean to text | 2026-09-16 |
 | comparator | leanprover/comparator | `d03acab154d269c06e60e4de7e4cc85deebff94b` | the verifier | 2026-09-16 |

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6",
+   "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
    "name": "«lean-eval-generator»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6",
+   "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
@@ -31,6 +31,16 @@
    "inputRev": "522706e83ca349c3d6bde045e56778d17354ae8d",
    "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,

lakefile.toml

@@ -4,6 +4,13 @@ defaultTargets = ["LeanEval"]
 [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"
+
 # 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
@@ -23,7 +30,7 @@ rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22"
 [[require]]
 name = "lean-eval-generator"
 git = "https://github.com/leanprover/lean-eval-generator.git"
-rev = "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6"
+rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4"
 
 [[lean_lib]]
 name = "LeanEval"

scripts/generate_projects_external.py

@@ -83,6 +83,7 @@ def request_for(problem_id: str) -> dict[str, object]:
         "contextRoot": str(ROOT),
         "leanToolchain": (ROOT / "lean-toolchain").read_text(encoding="utf-8"),
         "mathlib": mathlib[0],
+        "dependencies": [item for item in lakefile["require"] if item["name"] != "mathlib"],
         "templates": {
             "workspaceTest": (ROOT / "templates/WorkspaceTest.lean").read_text(
                 encoding="utf-8"

scripts/select_ci_problems.py

@@ -186,7 +186,7 @@ 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 in {"lakefile.toml", "lake-manifest.json", "lean-toolchain"}
+        or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"}
     )
 
 
@@ -206,7 +206,7 @@ def select(
     changed_paths = [path for change in changes for path in change.paths]
     source_changed = any(
         path.startswith(("LeanEval/", "EvalTools/", "templates/", "manifests/"))
-        or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain"}
+        or path in {"lakefile.toml", "lake-manifest.json", "lean-toolchain", "solution-dependencies.json"}
         for path in changed_paths
     )
     generated_changed = any(path.startswith("generated/") for path in changed_paths)

solution-dependencies.json

@@ -0,0 +1 @@
+[{"name": "lean-pool", "moduleRoots": ["LeanPool", "Challenge", "Solution"]}]

tests/python/test_select_ci_problems.py

@@ -77,6 +77,11 @@ def test_generator_change_is_a_full_catalog_sentinel(self):
         self.assertEqual(selection.mode, "full")
         self.assertEqual(selection.problems, ("a", "b", "b_second", "c"))
 
+    def test_solution_dependency_change_regenerates_every_workspace(self):
+        selection = self.select((Change("M", ("solution-dependencies.json",)),))
+        self.assertEqual(selection.mode, "full")
+        self.assertTrue(selection.source_changed)
+
     def test_tag_registry_change_is_a_full_catalog_sentinel(self):
         selection = self.select((Change("M", ("manifests/tags.toml",)),))
         self.assertEqual(selection.mode, "full")