From 842a552c23a3a0abd438c8f7454fb6ab96168bc8 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 27 Sep 2026 14:46:53 -0700 Subject: [PATCH 1/8] Allow solution-only Lean Pool dependencies --- EvalTools/CheckEvalWorkflow.lean | 10 +++- EvalTools/CheckProblemBuild.lean | 2 + EvalTools/Generate.lean | 50 +++++++++++++++++ EvalTools/Main.lean | 2 +- EvalTools/ModuleCoverage.lean | 3 + EvalTools/RunEval.lean | 2 +- EvalTools/SolutionDependencies.lean | 56 +++++++++++++++++++ README.md | 12 ++++ SECURITY.md | 1 + lake-manifest.json | 10 ++++ lakefile.toml | 7 +++ tests/lean/EvalToolsTests/GenerateTest.lean | 41 ++++++++++++++ .../EvalToolsTests/ModuleCoverageTest.lean | 20 +++++++ 13 files changed, 213 insertions(+), 3 deletions(-) create mode 100644 EvalTools/SolutionDependencies.lean diff --git a/EvalTools/CheckEvalWorkflow.lean b/EvalTools/CheckEvalWorkflow.lean index f42636fd..f0bd22f9 100644 --- a/EvalTools/CheckEvalWorkflow.lean +++ b/EvalTools/CheckEvalWorkflow.lean @@ -85,7 +85,7 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do -- catalog-wide generation check. CI validates and builds the full catalog -- independently; repeating that work here used to dominate the workflow. try - generate root (selectedProblemId := some TWO_PLUS_TWO_ID) (check := true) + generateSolutionWorkspaces root (selectedProblemId := some TWO_PLUS_TWO_ID) (check := true) catch e => throw <| IO.userError <| "The generated two_plus_two smoke-test workspace is stale.\n" ++ @@ -112,6 +112,14 @@ 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. + 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) diff --git a/EvalTools/CheckProblemBuild.lean b/EvalTools/CheckProblemBuild.lean index 94aa45f6..a4a14f24 100644 --- a/EvalTools/CheckProblemBuild.lean +++ b/EvalTools/CheckProblemBuild.lean @@ -1,4 +1,5 @@ import EvalTools.Manifest +import EvalTools.SolutionDependencies namespace EvalTools @@ -26,6 +27,7 @@ def runCheckProblemBuild (root : System.FilePath) let modules ← selectManifestModules entries requestedModules let mut disallowed := [] for moduleName in modules do + checkProblemSolutionImports root moduleName let output ← runCmdCheckedCaptured "lake" #["build", moduleName] root s!"Problem module '{moduleName}' build failed" let combined := diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index d6ec44bc..a818a2fd 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -1,5 +1,55 @@ import LeanEvalGenerator.Core.Generate +import EvalTools.SolutionDependencies namespace EvalTools +open Lean LeanEvalGenerator.Core + +set_option autoImplicit false + +/-- Repository orchestration around the generic renderer, with lean-eval's +solution-only dependency policy applied identically in write and check modes. -/ +def generateSolutionWorkspaces (root : System.FilePath) + (selectedProblemId : Option String) (check : Bool) : IO Unit := do + let problems ← loadManifest root + let selectedProblems ← + match selectedProblemId with + | some id => + let filtered := problems.filter (·.id == id) + if filtered.isEmpty then + throw <| IO.userError s!"Unknown problem id '{id}'" + pure filtered + | none => + validateManifestAgainstInventory root problems + let selectedIds : Std.HashSet String := problems.foldl (fun acc p => acc.insert p.id) {} + let mismatches ← syncUnknownProblemDirs root selectedIds check + if !mismatches.isEmpty then + throw <| IO.userError <| "\n".intercalate mismatches.toList + pure problems + for entry in selectedProblems do + checkProblemSolutionImports root entry.moduleName + validateHoleShape root selectedProblems + let toolchain ← IO.FS.readFile (root / "lean-toolchain") + let deps ← loadRootDependencies root + buildExtractor root selectedProblems + let workspaceTest ← loadWorkspaceTestTemplate root + let mut mismatches : Array String := #[] + for entry in selectedProblems do + let extracteds ← entry.holes.mapM (extractOne root entry) + let files ← renderSolutionWorkspace root entry extracteds toolchain deps workspaceTest + let problemDir := root / "generated" / entry.id + if check then + mismatches := mismatches ++ (← checkWorkspace problemDir s!"generated/{entry.id}" files) + else + writeWorkspace problemDir files + if selectedProblemId.isNone then + mismatches := mismatches ++ + (← writeOrCheckIndex root (problems.map generatedIndexEntry) check) + if !mismatches.isEmpty then + throw <| IO.userError <| "\n".intercalate mismatches.toList + if check then + IO.println "Generated workspaces are up to date." + else + IO.println s!"Generated {selectedProblems.size} problem workspace(s)." + end EvalTools diff --git a/EvalTools/Main.lean b/EvalTools/Main.lean index 85e9c910..54662418 100644 --- a/EvalTools/Main.lean +++ b/EvalTools/Main.lean @@ -64,7 +64,7 @@ def runGenerateCmd (p : Parsed) : IO UInt32 := do let problem? : Option String := p.flag? "problem" |>.map fun f => f.as! String let check := p.hasFlag "check" try - LeanEvalGenerator.Core.generate root problem? check + generateSolutionWorkspaces root problem? check return 0 catch e => IO.eprintln (toString e) diff --git a/EvalTools/ModuleCoverage.lean b/EvalTools/ModuleCoverage.lean index 0666b70f..bd713f81 100644 --- a/EvalTools/ModuleCoverage.lean +++ b/EvalTools/ModuleCoverage.lean @@ -1,5 +1,6 @@ import Lean import EvalTools.Markers +import EvalTools.SolutionDependencies open Lean @@ -107,6 +108,8 @@ so it costs no build time and runs before the inventory cross-check. -/ def checkProblemModuleCoverage (root : System.FilePath) (entries : Array EvalProblemMetadata) : IO Unit := do let sources ← loadProblemSourceModules root + for source in sources do + checkProblemSolutionImports root source.name.toString let known := sources.foldl (fun s source => s.insert source.name) (∅ : Std.HashSet Name) let missing := entries.filterMap fun entry => if known.contains (parseModuleName entry.moduleName) then none diff --git a/EvalTools/RunEval.lean b/EvalTools/RunEval.lean index b98700bd..2550de87 100644 --- a/EvalTools/RunEval.lean +++ b/EvalTools/RunEval.lean @@ -89,7 +89,7 @@ def scoreProblems (root : System.FilePath) (problems : Array EvalProblemMetadata for hole in entry.holes do let e ← extractOne root entry hole extracteds := extracteds.push e - let expectedFiles ← renderWorkspace root entry extracteds toolchain deps workspaceTest + let expectedFiles ← renderSolutionWorkspace root entry extracteds toolchain deps workspaceTest let workspace ← workspacePathForProblem root entry.id workspacesRoot let relDisplay := let wsStr := workspace.toString diff --git a/EvalTools/SolutionDependencies.lean b/EvalTools/SolutionDependencies.lean new file mode 100644 index 00000000..b256abaa --- /dev/null +++ b/EvalTools/SolutionDependencies.lean @@ -0,0 +1,56 @@ +import LeanEvalGenerator.Core.Generate + +namespace EvalTools + +open Lean LeanEvalGenerator.Core + +set_option autoImplicit false + +/-- Lean Pool's libraries are available to proofs, but must never enter a +trusted statement's import closure. Follow repository-local helpers as well. -/ +def checkProblemSolutionImports (root : System.FilePath) (moduleName : String) : IO Unit := do + for imported in (← problemWorkspaceImports root moduleName) do + let name := parseModuleName imported + if #[`LeanPool, `Challenge, `Solution].any (·.isPrefixOf name) then + throw <| IO.userError + s!"Problem module '{moduleName}' depends on solution-only module '{imported}'. \ + Lean Pool may be imported by Submission files, not problem statements or their helpers." + +/-- Add the pinned solution library before the statement's dependencies, keeping +Mathlib last so its shared transitive pins win during `lake update`. -/ +def solutionWorkspaceRequires (deps : RootDependencies) (imports : Array String) : + Except String (Array DependencySpec) := do + let pool := deps.extras.filter (·.name == "lean-pool") + unless pool.size == 1 do + throw "Expected exactly one pinned lean-pool root dependency for solution workspaces" + let pool ← pool[0]!.toSpec + let statementDeps ← workspaceRequires deps imports + return #[pool] ++ statementDeps.filter (·.name != pool.name) + +/-- Apply lean-eval's solution dependency policy to the generic generator output. +Only the Lake configuration and solver instructions change; statement imports and +the comparator's trusted environment remain those emitted by the generator. -/ +def withSolutionDependencies (root : System.FilePath) (entry : EvalProblemMetadata) + (deps : RootDependencies) (files : Array (String × String)) : + IO (Array (String × String)) := do + checkProblemSolutionImports root entry.moduleName + let requires ← IO.ofExcept <| + solutionWorkspaceRequires deps (← problemWorkspaceImports root entry.moduleName) + let hasChallengeDeps := files.any (·.1 == "ChallengeDeps.lean") + return files.map fun (path, content) => + if path == "lakefile.toml" then + (path, lakefileToml entry.id requires hasChallengeDeps) + else if path == "README.md" then + (path, content ++ "\nLean Pool is available to solutions at the pinned revision in `lakefile.toml`.\n" ++ + "Import individual `LeanPool.*` modules in `Submission.lean` or `Submission/` helpers.\n" ++ + "Problem statements and trusted helpers must not depend on Lean Pool.\n") + else (path, content) + +/-- Shared renderer for generation and scoring's pristine-workspace comparison. -/ +def renderSolutionWorkspace (root : System.FilePath) (entry : EvalProblemMetadata) + (extracteds : Array ExtractedTheorem) (toolchain : String) + (deps : RootDependencies) (workspaceTest : String) : IO (Array (String × String)) := do + let files ← renderWorkspace root entry extracteds toolchain deps workspaceTest + withSolutionDependencies root entry deps files + +end EvalTools diff --git a/README.md b/README.md index 3ae1adff..2ca27bb4 100644 --- a/README.md +++ b/README.md @@ -206,6 +206,18 @@ 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 individual `LeanPool.*` modules from +[Lean Pool](https://github.com/Vilin97/lean-pool) in `Submission.lean` or helpers +under `Submission/`. Generated workspaces include a pinned `lean-pool` dependency; +you do not need to edit `lakefile.toml`. Only modules you import are built. +The usual comparator and nanoda checks still apply to the resulting proof. + +Lean Pool is **solution-only**: problem statements under `LeanEval/` and their +local helpers may not import it. Both manifest validation and workspace generation +reject these imports, including indirect imports through local helpers. The root +dependency exists to share the pinned package cache with solver workspaces, not to +extend the benchmark's statement vocabulary. + ### 5. Run comparator locally ```bash diff --git a/SECURITY.md b/SECURITY.md index 386aeda9..5b14b123 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -215,6 +215,7 @@ time, the upstream publisher controls our supply chain. | 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 | +| lean-pool | Vilin97/lean-pool | `20fb00c51334c79a2b75ed548dea093774ad62b0` | solution-only library; forbidden in trusted problem imports | 2026-09-27 | | lean4-cli | leanprover/lean4-cli | `e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204` | command-line parsing | 2026-09-16 | | landrun | zouuup/landrun | `5ed4a3db3a4ad930d577215c6b9abaa19df7f99f` | Linux landlock sandbox | 2026-05-04 | | lean4export | leanprover/lean4export | `076e8e57707e813375e8f9da8bf989799ace9680` | exports olean to text | 2026-09-16 | diff --git a/lake-manifest.json b/lake-manifest.json index 6e78c9e9..38b9dd2b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -41,6 +41,16 @@ "inputRev": "23bfe9bc742f8713b58ce40b155f994848ae8a5e", "inherited": false, "configFile": "lakefile.toml"}, + {"url": "https://github.com/Vilin97/lean-pool.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "20fb00c51334c79a2b75ed548dea093774ad62b0", + "name": "«lean-pool»", + "manifestFile": "lake-manifest.json", + "inputRev": "20fb00c51334c79a2b75ed548dea093774ad62b0", + "inherited": false, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, diff --git a/lakefile.toml b/lakefile.toml index 3f7f8af5..615d5a76 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,6 +4,13 @@ defaultTargets = ["LeanEval"] [leanOptions] autoImplicit = false +# Available to generated solutions only. Problem-source validation rejects +# 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 = "20fb00c51334c79a2b75ed548dea093774ad62b0" + # 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 diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 813768a6..2c0c5052 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -71,6 +71,47 @@ def main : IO UInt32 := do let passes ← IO.mkRef 0 let fails ← IO.mkRef 0 + check "solution dependencies preserve statement dependencies and put Mathlib last" passes fails do + let deps : RootDependencies := { + mathlib := { name := "mathlib", git := "mathlib-url", rev := "mathlib-pin" } + extras := #[ + { name := "TauCeti", git := some "tau-url", rev := some "tau-pin" }, + { name := "lean-pool", git := some "pool-url", rev := some "pool-pin" }, + { name := "Cli" }] + } + let specs ← IO.ofExcept (solutionWorkspaceRequires deps #["TauCeti.Foo", "Mathlib"]) + pure <| assertEq "dependency order" (specs.map (·.name)) #["lean-pool", "TauCeti", "mathlib"] + |>.or (assertEq "pool pin" specs[0]!.rev "pool-pin") + + check "solution dependencies reject a missing or unpinned pool" passes fails do + let deps : RootDependencies := { + mathlib := { name := "mathlib", git := "mathlib-url", rev := "mathlib-pin" } + } + pure <| assertEq "missing pin rejected" + (solutionWorkspaceRequires deps #[]).isOk false + |>.or (assertEq "empty pin rejected" + (solutionWorkspaceRequires { deps with extras := #[{ name := "lean-pool" }] } #[]).isOk false) + + check "solution policy changes only the lakefile and solver documentation" passes fails do + let root ← IO.currentDir + let deps ← loadRootDependencies root + let entry : EvalProblemMetadata := { + id := "two_plus_two", title := "test", group := "test", status := "draft", + visible := true, statementRevision := 1, tags := #[], + moduleName := "LeanEval.EasyProblems", holes := #["two_plus_two"], submitter := "tester" + } + let files := #[ + ("Challenge.lean", "trusted statement"), ("ChallengeDeps.lean", "trusted helpers"), + ("Solution.lean", "trusted bridge"), ("config.json", "trusted config"), + ("Submission.lean", "solver proof"), ("lakefile.toml", "old lakefile"), + ("README.md", "instructions\n")] + let updated ← withSolutionDependencies root entry deps files + let trusted := files.filter fun (path, _) => path != "lakefile.toml" && path != "README.md" + let lakefile := (updated.find? (·.1 == "lakefile.toml")).get!.2 + pure <| assertEq "trusted files unchanged" (updated.extract 0 5) trusted + |>.or (assertContains "pool available" lakefile "name = \"lean-pool\"") + |>.or (assertContains "helper library retained" lakefile "name = \"ChallengeDeps\"") + check "validateGeneratedCatalog accepts a coherent generated tree" passes fails do withGeneratedCatalog fun root => do validateGeneratedCatalog root diff --git a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean index 05b21c7a..b0b02c58 100644 --- a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean +++ b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean @@ -74,6 +74,26 @@ def main : IO UInt32 := do let passes ← IO.mkRef 0 let fails ← IO.mkRef 0 + check "problem coverage rejects solution-only imports, including through helpers" passes fails do + for imported in #["LeanPool.Basic", "LeanPool", "«LeanPool».Basic", "Challenge.Foo", "Solution.Foo"] do + let result ← withFakeRepo #[ + ("LeanEval/Claimed.lean", "import LeanEval.Helper\n"), + ("LeanEval/Helper.lean", s!"import {imported}\n") + ] fun root => do + match ← (checkProblemModuleCoverage root #[problem "p" "LeanEval.Claimed"]).toBaseIO with + | .ok _ => pure (some s!"accepted forbidden import {imported}") + | .error err => pure <| assertContains "error explains policy" (toString err) "solution-only" + if result.isSome then return result + return none + + check "problem coverage ignores commented imports and similarly named modules" passes fails do + withFakeRepo #[ + ("LeanEval/Claimed.lean", + "/- import LeanPool.Basic -/\nimport LeanPoolish.Basic\nimport Mathlib\n") + ] fun root => do + checkProblemModuleCoverage root #[problem "p" "LeanEval.Claimed"] + pure none + -- Regression for https://github.com/leanprover/lean-eval/issues/519: a module -- no manifest reaches is never compiled, so a broken statement leaves CI green. check "unreachableModules reports a module no root reaches" passes fails do From b0a3ce776a22eaaef845fa38e05b2a19edf082a1 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 27 Sep 2026 15:13:34 -0700 Subject: [PATCH 2/8] Use shared generator support for solution dependencies --- .github/workflows/notify-leaderboard.yml | 1 + .github/workflows/regenerate-main.yml | 1 + EvalTools/CheckEvalWorkflow.lean | 5 +- EvalTools/CheckProblemBuild.lean | 2 - EvalTools/Generate.lean | 50 ----------------- EvalTools/Main.lean | 2 +- EvalTools/ModuleCoverage.lean | 3 - EvalTools/RunEval.lean | 2 +- EvalTools/SolutionDependencies.lean | 56 ------------------- README.md | 16 ++---- lake-manifest.json | 6 +- lakefile.toml | 9 +-- scripts/generate_projects_external.py | 4 ++ scripts/select_ci_problems.py | 4 +- solution-dependencies.json | 1 + tests/lean/EvalToolsTests/GenerateTest.lean | 41 -------------- .../EvalToolsTests/ModuleCoverageTest.lean | 20 ------- tests/python/test_select_ci_problems.py | 5 ++ 18 files changed, 33 insertions(+), 195 deletions(-) delete mode 100644 EvalTools/SolutionDependencies.lean create mode 100644 solution-dependencies.json diff --git a/.github/workflows/notify-leaderboard.yml b/.github/workflows/notify-leaderboard.yml index 35277179..937f3375 100644 --- a/.github/workflows/notify-leaderboard.yml +++ b/.github/workflows/notify-leaderboard.yml @@ -17,6 +17,7 @@ on: - 'manifests/**' - 'generated/**' - 'lakefile.toml' + - 'solution-dependencies.json' - 'lean-toolchain' workflow_dispatch: diff --git a/.github/workflows/regenerate-main.yml b/.github/workflows/regenerate-main.yml index 4ded3cdd..ef5678a2 100644 --- a/.github/workflows/regenerate-main.yml +++ b/.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: diff --git a/EvalTools/CheckEvalWorkflow.lean b/EvalTools/CheckEvalWorkflow.lean index f0bd22f9..aa8e8edf 100644 --- a/EvalTools/CheckEvalWorkflow.lean +++ b/EvalTools/CheckEvalWorkflow.lean @@ -85,7 +85,7 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do -- catalog-wide generation check. CI validates and builds the full catalog -- independently; repeating that work here used to dominate the workflow. try - generateSolutionWorkspaces root (selectedProblemId := some TWO_PLUS_TWO_ID) (check := true) + generate root (selectedProblemId := some TWO_PLUS_TWO_ID) (check := true) catch e => throw <| IO.userError <| "The generated two_plus_two smoke-test workspace is stale.\n" ++ @@ -114,6 +114,9 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do 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" diff --git a/EvalTools/CheckProblemBuild.lean b/EvalTools/CheckProblemBuild.lean index a4a14f24..94aa45f6 100644 --- a/EvalTools/CheckProblemBuild.lean +++ b/EvalTools/CheckProblemBuild.lean @@ -1,5 +1,4 @@ import EvalTools.Manifest -import EvalTools.SolutionDependencies namespace EvalTools @@ -27,7 +26,6 @@ def runCheckProblemBuild (root : System.FilePath) let modules ← selectManifestModules entries requestedModules let mut disallowed := [] for moduleName in modules do - checkProblemSolutionImports root moduleName let output ← runCmdCheckedCaptured "lake" #["build", moduleName] root s!"Problem module '{moduleName}' build failed" let combined := diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean index a818a2fd..d6ec44bc 100644 --- a/EvalTools/Generate.lean +++ b/EvalTools/Generate.lean @@ -1,55 +1,5 @@ import LeanEvalGenerator.Core.Generate -import EvalTools.SolutionDependencies namespace EvalTools -open Lean LeanEvalGenerator.Core - -set_option autoImplicit false - -/-- Repository orchestration around the generic renderer, with lean-eval's -solution-only dependency policy applied identically in write and check modes. -/ -def generateSolutionWorkspaces (root : System.FilePath) - (selectedProblemId : Option String) (check : Bool) : IO Unit := do - let problems ← loadManifest root - let selectedProblems ← - match selectedProblemId with - | some id => - let filtered := problems.filter (·.id == id) - if filtered.isEmpty then - throw <| IO.userError s!"Unknown problem id '{id}'" - pure filtered - | none => - validateManifestAgainstInventory root problems - let selectedIds : Std.HashSet String := problems.foldl (fun acc p => acc.insert p.id) {} - let mismatches ← syncUnknownProblemDirs root selectedIds check - if !mismatches.isEmpty then - throw <| IO.userError <| "\n".intercalate mismatches.toList - pure problems - for entry in selectedProblems do - checkProblemSolutionImports root entry.moduleName - validateHoleShape root selectedProblems - let toolchain ← IO.FS.readFile (root / "lean-toolchain") - let deps ← loadRootDependencies root - buildExtractor root selectedProblems - let workspaceTest ← loadWorkspaceTestTemplate root - let mut mismatches : Array String := #[] - for entry in selectedProblems do - let extracteds ← entry.holes.mapM (extractOne root entry) - let files ← renderSolutionWorkspace root entry extracteds toolchain deps workspaceTest - let problemDir := root / "generated" / entry.id - if check then - mismatches := mismatches ++ (← checkWorkspace problemDir s!"generated/{entry.id}" files) - else - writeWorkspace problemDir files - if selectedProblemId.isNone then - mismatches := mismatches ++ - (← writeOrCheckIndex root (problems.map generatedIndexEntry) check) - if !mismatches.isEmpty then - throw <| IO.userError <| "\n".intercalate mismatches.toList - if check then - IO.println "Generated workspaces are up to date." - else - IO.println s!"Generated {selectedProblems.size} problem workspace(s)." - end EvalTools diff --git a/EvalTools/Main.lean b/EvalTools/Main.lean index 54662418..85e9c910 100644 --- a/EvalTools/Main.lean +++ b/EvalTools/Main.lean @@ -64,7 +64,7 @@ def runGenerateCmd (p : Parsed) : IO UInt32 := do let problem? : Option String := p.flag? "problem" |>.map fun f => f.as! String let check := p.hasFlag "check" try - generateSolutionWorkspaces root problem? check + LeanEvalGenerator.Core.generate root problem? check return 0 catch e => IO.eprintln (toString e) diff --git a/EvalTools/ModuleCoverage.lean b/EvalTools/ModuleCoverage.lean index bd713f81..0666b70f 100644 --- a/EvalTools/ModuleCoverage.lean +++ b/EvalTools/ModuleCoverage.lean @@ -1,6 +1,5 @@ import Lean import EvalTools.Markers -import EvalTools.SolutionDependencies open Lean @@ -108,8 +107,6 @@ so it costs no build time and runs before the inventory cross-check. -/ def checkProblemModuleCoverage (root : System.FilePath) (entries : Array EvalProblemMetadata) : IO Unit := do let sources ← loadProblemSourceModules root - for source in sources do - checkProblemSolutionImports root source.name.toString let known := sources.foldl (fun s source => s.insert source.name) (∅ : Std.HashSet Name) let missing := entries.filterMap fun entry => if known.contains (parseModuleName entry.moduleName) then none diff --git a/EvalTools/RunEval.lean b/EvalTools/RunEval.lean index 2550de87..b98700bd 100644 --- a/EvalTools/RunEval.lean +++ b/EvalTools/RunEval.lean @@ -89,7 +89,7 @@ def scoreProblems (root : System.FilePath) (problems : Array EvalProblemMetadata for hole in entry.holes do let e ← extractOne root entry hole extracteds := extracteds.push e - let expectedFiles ← renderSolutionWorkspace root entry extracteds toolchain deps workspaceTest + let expectedFiles ← renderWorkspace root entry extracteds toolchain deps workspaceTest let workspace ← workspacePathForProblem root entry.id workspacesRoot let relDisplay := let wsStr := workspace.toString diff --git a/EvalTools/SolutionDependencies.lean b/EvalTools/SolutionDependencies.lean deleted file mode 100644 index b256abaa..00000000 --- a/EvalTools/SolutionDependencies.lean +++ /dev/null @@ -1,56 +0,0 @@ -import LeanEvalGenerator.Core.Generate - -namespace EvalTools - -open Lean LeanEvalGenerator.Core - -set_option autoImplicit false - -/-- Lean Pool's libraries are available to proofs, but must never enter a -trusted statement's import closure. Follow repository-local helpers as well. -/ -def checkProblemSolutionImports (root : System.FilePath) (moduleName : String) : IO Unit := do - for imported in (← problemWorkspaceImports root moduleName) do - let name := parseModuleName imported - if #[`LeanPool, `Challenge, `Solution].any (·.isPrefixOf name) then - throw <| IO.userError - s!"Problem module '{moduleName}' depends on solution-only module '{imported}'. \ - Lean Pool may be imported by Submission files, not problem statements or their helpers." - -/-- Add the pinned solution library before the statement's dependencies, keeping -Mathlib last so its shared transitive pins win during `lake update`. -/ -def solutionWorkspaceRequires (deps : RootDependencies) (imports : Array String) : - Except String (Array DependencySpec) := do - let pool := deps.extras.filter (·.name == "lean-pool") - unless pool.size == 1 do - throw "Expected exactly one pinned lean-pool root dependency for solution workspaces" - let pool ← pool[0]!.toSpec - let statementDeps ← workspaceRequires deps imports - return #[pool] ++ statementDeps.filter (·.name != pool.name) - -/-- Apply lean-eval's solution dependency policy to the generic generator output. -Only the Lake configuration and solver instructions change; statement imports and -the comparator's trusted environment remain those emitted by the generator. -/ -def withSolutionDependencies (root : System.FilePath) (entry : EvalProblemMetadata) - (deps : RootDependencies) (files : Array (String × String)) : - IO (Array (String × String)) := do - checkProblemSolutionImports root entry.moduleName - let requires ← IO.ofExcept <| - solutionWorkspaceRequires deps (← problemWorkspaceImports root entry.moduleName) - let hasChallengeDeps := files.any (·.1 == "ChallengeDeps.lean") - return files.map fun (path, content) => - if path == "lakefile.toml" then - (path, lakefileToml entry.id requires hasChallengeDeps) - else if path == "README.md" then - (path, content ++ "\nLean Pool is available to solutions at the pinned revision in `lakefile.toml`.\n" ++ - "Import individual `LeanPool.*` modules in `Submission.lean` or `Submission/` helpers.\n" ++ - "Problem statements and trusted helpers must not depend on Lean Pool.\n") - else (path, content) - -/-- Shared renderer for generation and scoring's pristine-workspace comparison. -/ -def renderSolutionWorkspace (root : System.FilePath) (entry : EvalProblemMetadata) - (extracteds : Array ExtractedTheorem) (toolchain : String) - (deps : RootDependencies) (workspaceTest : String) : IO (Array (String × String)) := do - let files ← renderWorkspace root entry extracteds toolchain deps workspaceTest - withSolutionDependencies root entry deps files - -end EvalTools diff --git a/README.md b/README.md index 2ca27bb4..c10698ea 100644 --- a/README.md +++ b/README.md @@ -206,17 +206,11 @@ 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 individual `LeanPool.*` modules from -[Lean Pool](https://github.com/Vilin97/lean-pool) in `Submission.lean` or helpers -under `Submission/`. Generated workspaces include a pinned `lean-pool` dependency; -you do not need to edit `lakefile.toml`. Only modules you import are built. -The usual comparator and nanoda checks still apply to the resulting proof. - -Lean Pool is **solution-only**: problem statements under `LeanEval/` and their -local helpers may not import it. Both manifest validation and workspace generation -reject these imports, including indirect imports through local helpers. The root -dependency exists to share the pinned package cache with solver workspaces, not to -extend the benchmark's statement vocabulary. +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 diff --git a/lake-manifest.json b/lake-manifest.json index 38b9dd2b..90b08f26 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/lean-eval-generator.git", + [{"url": "https://github.com/Vilin97/lean-eval-generator.git", "type": "git", "subDir": null, "scope": "", - "rev": "2de74049bd91d2c592e7009df8f5e5968599a272", + "rev": "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "2de74049bd91d2c592e7009df8f5e5968599a272", + "inputRev": "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 615d5a76..7331418f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,8 +4,8 @@ defaultTargets = ["LeanEval"] [leanOptions] autoImplicit = false -# Available to generated solutions only. Problem-source validation rejects -# imports from lean-pool; keep this before Mathlib so Mathlib owns shared pins. +# 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" @@ -34,8 +34,9 @@ rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" [[require]] name = "lean-eval-generator" -git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "2de74049bd91d2c592e7009df8f5e5968599a272" +# Upstream: leanprover/lean-eval-generator#9; use its pinned fork until merged. +git = "https://github.com/Vilin97/lean-eval-generator.git" +rev = "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1" [[lean_lib]] name = "LeanEval" diff --git a/scripts/generate_projects_external.py b/scripts/generate_projects_external.py index 5c5e928a..08c9b909 100644 --- a/scripts/generate_projects_external.py +++ b/scripts/generate_projects_external.py @@ -83,6 +83,10 @@ 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"], + "solutionDependencies": json.loads( + (ROOT / "solution-dependencies.json").read_text(encoding="utf-8") + ), "templates": { "workspaceTest": (ROOT / "templates/WorkspaceTest.lean").read_text( encoding="utf-8" diff --git a/scripts/select_ci_problems.py b/scripts/select_ci_problems.py index 4e83a0d5..178800bf 100644 --- a/scripts/select_ci_problems.py +++ b/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) diff --git a/solution-dependencies.json b/solution-dependencies.json new file mode 100644 index 00000000..d7a619ee --- /dev/null +++ b/solution-dependencies.json @@ -0,0 +1 @@ +[{"name": "lean-pool", "moduleRoots": ["LeanPool", "Challenge", "Solution"]}] diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean index 2c0c5052..813768a6 100644 --- a/tests/lean/EvalToolsTests/GenerateTest.lean +++ b/tests/lean/EvalToolsTests/GenerateTest.lean @@ -71,47 +71,6 @@ def main : IO UInt32 := do let passes ← IO.mkRef 0 let fails ← IO.mkRef 0 - check "solution dependencies preserve statement dependencies and put Mathlib last" passes fails do - let deps : RootDependencies := { - mathlib := { name := "mathlib", git := "mathlib-url", rev := "mathlib-pin" } - extras := #[ - { name := "TauCeti", git := some "tau-url", rev := some "tau-pin" }, - { name := "lean-pool", git := some "pool-url", rev := some "pool-pin" }, - { name := "Cli" }] - } - let specs ← IO.ofExcept (solutionWorkspaceRequires deps #["TauCeti.Foo", "Mathlib"]) - pure <| assertEq "dependency order" (specs.map (·.name)) #["lean-pool", "TauCeti", "mathlib"] - |>.or (assertEq "pool pin" specs[0]!.rev "pool-pin") - - check "solution dependencies reject a missing or unpinned pool" passes fails do - let deps : RootDependencies := { - mathlib := { name := "mathlib", git := "mathlib-url", rev := "mathlib-pin" } - } - pure <| assertEq "missing pin rejected" - (solutionWorkspaceRequires deps #[]).isOk false - |>.or (assertEq "empty pin rejected" - (solutionWorkspaceRequires { deps with extras := #[{ name := "lean-pool" }] } #[]).isOk false) - - check "solution policy changes only the lakefile and solver documentation" passes fails do - let root ← IO.currentDir - let deps ← loadRootDependencies root - let entry : EvalProblemMetadata := { - id := "two_plus_two", title := "test", group := "test", status := "draft", - visible := true, statementRevision := 1, tags := #[], - moduleName := "LeanEval.EasyProblems", holes := #["two_plus_two"], submitter := "tester" - } - let files := #[ - ("Challenge.lean", "trusted statement"), ("ChallengeDeps.lean", "trusted helpers"), - ("Solution.lean", "trusted bridge"), ("config.json", "trusted config"), - ("Submission.lean", "solver proof"), ("lakefile.toml", "old lakefile"), - ("README.md", "instructions\n")] - let updated ← withSolutionDependencies root entry deps files - let trusted := files.filter fun (path, _) => path != "lakefile.toml" && path != "README.md" - let lakefile := (updated.find? (·.1 == "lakefile.toml")).get!.2 - pure <| assertEq "trusted files unchanged" (updated.extract 0 5) trusted - |>.or (assertContains "pool available" lakefile "name = \"lean-pool\"") - |>.or (assertContains "helper library retained" lakefile "name = \"ChallengeDeps\"") - check "validateGeneratedCatalog accepts a coherent generated tree" passes fails do withGeneratedCatalog fun root => do validateGeneratedCatalog root diff --git a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean index b0b02c58..05b21c7a 100644 --- a/tests/lean/EvalToolsTests/ModuleCoverageTest.lean +++ b/tests/lean/EvalToolsTests/ModuleCoverageTest.lean @@ -74,26 +74,6 @@ def main : IO UInt32 := do let passes ← IO.mkRef 0 let fails ← IO.mkRef 0 - check "problem coverage rejects solution-only imports, including through helpers" passes fails do - for imported in #["LeanPool.Basic", "LeanPool", "«LeanPool».Basic", "Challenge.Foo", "Solution.Foo"] do - let result ← withFakeRepo #[ - ("LeanEval/Claimed.lean", "import LeanEval.Helper\n"), - ("LeanEval/Helper.lean", s!"import {imported}\n") - ] fun root => do - match ← (checkProblemModuleCoverage root #[problem "p" "LeanEval.Claimed"]).toBaseIO with - | .ok _ => pure (some s!"accepted forbidden import {imported}") - | .error err => pure <| assertContains "error explains policy" (toString err) "solution-only" - if result.isSome then return result - return none - - check "problem coverage ignores commented imports and similarly named modules" passes fails do - withFakeRepo #[ - ("LeanEval/Claimed.lean", - "/- import LeanPool.Basic -/\nimport LeanPoolish.Basic\nimport Mathlib\n") - ] fun root => do - checkProblemModuleCoverage root #[problem "p" "LeanEval.Claimed"] - pure none - -- Regression for https://github.com/leanprover/lean-eval/issues/519: a module -- no manifest reaches is never compiled, so a broken statement leaves CI green. check "unreachableModules reports a module no root reaches" passes fails do diff --git a/tests/python/test_select_ci_problems.py b/tests/python/test_select_ci_problems.py index 6c930ecc..5f7c14ef 100644 --- a/tests/python/test_select_ci_problems.py +++ b/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") From 876d4bf588e445740695d5e0c98274840a853575 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 27 Sep 2026 18:25:35 -0500 Subject: [PATCH 3/8] Update generator with isolated solution dependency tests --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 90b08f26..79725bd1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1", + "rev": "bd54907811ed256e67e0f67f785d8d1a2b8981df", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1", + "inputRev": "bd54907811ed256e67e0f67f785d8d1a2b8981df", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 7331418f..d38233e9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -36,7 +36,7 @@ rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" name = "lean-eval-generator" # Upstream: leanprover/lean-eval-generator#9; use its pinned fork until merged. git = "https://github.com/Vilin97/lean-eval-generator.git" -rev = "bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1" +rev = "bd54907811ed256e67e0f67f785d8d1a2b8981df" [[lean_lib]] name = "LeanEval" From 3ee7cbf968fdd580e9268edf65e117803485c095 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sun, 27 Sep 2026 18:43:50 -0500 Subject: [PATCH 4/8] Use shared solution policy without extending JSON requests --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- scripts/generate_projects_external.py | 3 --- 3 files changed, 3 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 79725bd1..04ff85f8 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bd54907811ed256e67e0f67f785d8d1a2b8981df", + "rev": "0c9c5ce33933c5d19e817abfd918f552e6db60fe", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "bd54907811ed256e67e0f67f785d8d1a2b8981df", + "inputRev": "0c9c5ce33933c5d19e817abfd918f552e6db60fe", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index d38233e9..3986ec72 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -36,7 +36,7 @@ rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" name = "lean-eval-generator" # Upstream: leanprover/lean-eval-generator#9; use its pinned fork until merged. git = "https://github.com/Vilin97/lean-eval-generator.git" -rev = "bd54907811ed256e67e0f67f785d8d1a2b8981df" +rev = "0c9c5ce33933c5d19e817abfd918f552e6db60fe" [[lean_lib]] name = "LeanEval" diff --git a/scripts/generate_projects_external.py b/scripts/generate_projects_external.py index 08c9b909..8e18881d 100644 --- a/scripts/generate_projects_external.py +++ b/scripts/generate_projects_external.py @@ -84,9 +84,6 @@ def request_for(problem_id: str) -> dict[str, object]: "leanToolchain": (ROOT / "lean-toolchain").read_text(encoding="utf-8"), "mathlib": mathlib[0], "dependencies": [item for item in lakefile["require"] if item["name"] != "mathlib"], - "solutionDependencies": json.loads( - (ROOT / "solution-dependencies.json").read_text(encoding="utf-8") - ), "templates": { "workspaceTest": (ROOT / "templates/WorkspaceTest.lean").read_text( encoding="utf-8" From 8566881ffb4fa4ab7e30c272eb42e7dd9d6061d9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 04:16:14 +0000 Subject: [PATCH 5/8] chore: pin merged upstream solution-dependency generator --- lake-manifest.json | 6 +++--- lakefile.toml | 5 ++--- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 04ff85f8..fc99adcc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,14 +1,14 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/Vilin97/lean-eval-generator.git", + [{"url": "https://github.com/leanprover/lean-eval-generator.git", "type": "git", "subDir": null, "scope": "", - "rev": "0c9c5ce33933c5d19e817abfd918f552e6db60fe", + "rev": "2dadd718ff613587716e22df726ad370147680da", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "0c9c5ce33933c5d19e817abfd918f552e6db60fe", + "inputRev": "2dadd718ff613587716e22df726ad370147680da", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.toml b/lakefile.toml index 3986ec72..ec8f3993 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -34,9 +34,8 @@ rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" [[require]] name = "lean-eval-generator" -# Upstream: leanprover/lean-eval-generator#9; use its pinned fork until merged. -git = "https://github.com/Vilin97/lean-eval-generator.git" -rev = "0c9c5ce33933c5d19e817abfd918f552e6db60fe" +git = "https://github.com/leanprover/lean-eval-generator.git" +rev = "2dadd718ff613587716e22df726ad370147680da" [[lean_lib]] name = "LeanEval" From 6f51fc5e9acb2a437016be9795b22631962ce382 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 04:59:20 +0000 Subject: [PATCH 6/8] Pin the validated Lean 4.35-compatible LeanPool revision --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index e03e2354..5236efa5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "20fb00c51334c79a2b75ed548dea093774ad62b0", + "rev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", "name": "«lean-pool»", "manifestFile": "lake-manifest.json", - "inputRev": "20fb00c51334c79a2b75ed548dea093774ad62b0", + "inputRev": "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.toml b/lakefile.toml index 8dd263f3..57217db9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,7 +9,7 @@ autoImplicit = false [[require]] name = "lean-pool" git = "https://github.com/Vilin97/lean-pool.git" -rev = "20fb00c51334c79a2b75ed548dea093774ad62b0" +rev = "e9d53e9cbcff8dfd0cc816ba94db7a26b082929f" # TauCeti supplies the definitions in the classification of finite simple groups # problem. It is listed before Mathlib because Lake takes shared transitive From f71b14af3713479ce35b33bff0d35a919a31bc6d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 05:04:41 +0000 Subject: [PATCH 7/8] Use module-system imports in the LeanPool scoring probe --- EvalTools/CheckEvalWorkflow.lean | 8 +++++--- README.md | 4 ++++ 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/EvalTools/CheckEvalWorkflow.lean b/EvalTools/CheckEvalWorkflow.lean index aa8e8edf..3cbaaa01 100644 --- a/EvalTools/CheckEvalWorkflow.lean +++ b/EvalTools/CheckEvalWorkflow.lean @@ -118,9 +118,11 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do 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!) + ("module\npublic import LeanPool.Basic\n" ++ + ((replaceFirst pristineSubmission " sorry\n" + " cases (show hello = \"world\" from rfl)\n norm_num\n").get! + |>.replace "import " "public import " + |>.replace "theorem " "public theorem ")) let poolSummary ← summarizeAtRoot root problems workspacesRoot assertCounts poolSummary 1 1 "Correct attempt importing Lean Pool" IO.println "Eval workflow check passed." diff --git a/README.md b/README.md index c10698ea..0d7a8299 100644 --- a/README.md +++ b/README.md @@ -212,6 +212,10 @@ all generated workspaces via `solution-dependencies.json`. Problem statements an their local helpers may not import it; workspace generation rejects these imports. Comparator and nanoda checks apply as usual. +Lean Pool uses Lean's module system. Start a submission file importing it with +`module`, use `public import` for dependencies needed in exported theorem statements, +and mark the submitted theorem `public theorem` so the `Solution.lean` bridge can use it. + ### 5. Run comparator locally ```bash From 78a3333884d386a486896a0303c57ccfb76813d5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 28 Sep 2026 05:22:36 +0000 Subject: [PATCH 8/8] Pin legacy workspace compatibility and refresh dependency documentation --- EvalTools/CheckEvalWorkflow.lean | 8 +++----- README.md | 4 ---- SECURITY.md | 11 ++++++----- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 5 files changed, 12 insertions(+), 17 deletions(-) diff --git a/EvalTools/CheckEvalWorkflow.lean b/EvalTools/CheckEvalWorkflow.lean index 3cbaaa01..aa8e8edf 100644 --- a/EvalTools/CheckEvalWorkflow.lean +++ b/EvalTools/CheckEvalWorkflow.lean @@ -118,11 +118,9 @@ def runCheckEvalWorkflow (root : System.FilePath) : IO UInt32 := do let _ ← runCmdCheckedCaptured "lake" #["build", "LeanPool.Basic"] root "Failed to prepare the Lean Pool smoke-test dependency" IO.FS.writeFile (workspace / "Submission.lean") - ("module\npublic import LeanPool.Basic\n" ++ - ((replaceFirst pristineSubmission " sorry\n" - " cases (show hello = \"world\" from rfl)\n norm_num\n").get! - |>.replace "import " "public import " - |>.replace "theorem " "public theorem ")) + ("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." diff --git a/README.md b/README.md index 0d7a8299..c10698ea 100644 --- a/README.md +++ b/README.md @@ -212,10 +212,6 @@ all generated workspaces via `solution-dependencies.json`. Problem statements an their local helpers may not import it; workspace generation rejects these imports. Comparator and nanoda checks apply as usual. -Lean Pool uses Lean's module system. Start a submission file importing it with -`module`, use `public import` for dependencies needed in exported theorem statements, -and mark the submitted theorem `public theorem` so the `Solution.lean` bridge can use it. - ### 5. Run comparator locally ```bash diff --git a/SECURITY.md b/SECURITY.md index 5b14b123..fd56f9b6 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -212,11 +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 | -| lean-pool | Vilin97/lean-pool | `20fb00c51334c79a2b75ed548dea093774ad62b0` | solution-only library; forbidden in trusted problem imports | 2026-09-27 | -| 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 | diff --git a/lake-manifest.json b/lake-manifest.json index 5236efa5..f15e8b70 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "2dadd718ff613587716e22df726ad370147680da", + "rev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "2dadd718ff613587716e22df726ad370147680da", + "inputRev": "0b8cc2d141710a18515c53448f006c971dd8eeb4", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index 57217db9..b4172838 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -30,7 +30,7 @@ rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22" [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "2dadd718ff613587716e22df726ad370147680da" +rev = "0b8cc2d141710a18515c53448f006c971dd8eeb4" [[lean_lib]] name = "LeanEval"