From bade61dfb1cdbeb3d5fcde0fa4dac5fca29e38c1 Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sun, 27 Sep 2026 15:08:46 -0700
Subject: [PATCH 1/3] Support explicitly configured solution-only dependencies

---
 LeanEvalGenerator/Contract.lean      |  7 ++++-
 LeanEvalGenerator/Core/Generate.lean | 38 +++++++++++++++++++++++++---
 README.md                            | 13 ++++++++++
 Tests/Dependencies.lean              | 22 ++++++++++++++++
 schemas/request-v1.schema.json       | 15 +++++++++++
 tests/scripts/contract.py            | 16 ++++++++++++
 6 files changed, 107 insertions(+), 4 deletions(-)

diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index 34d8e57..db2c09d 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -63,6 +63,7 @@ structure GenerateRequest where
   `LeanEvalGenerator.Core.workspaceRequires`). Omitting the field means no
   extra requires, which is how every earlier version 1 request behaves. -/
   dependencies : Option (Array DependencyPin) := none
+  solutionDependencies : Option (Array Core.SolutionDependency) := none
   templates : TemplateInputs
   problems : Array ProblemInput
   deriving FromJson
@@ -213,6 +214,7 @@ def render (request : GenerateRequest) : IO String := do
   let spec (pin : DependencyPin) : LeanEvalGenerator.Core.DependencySpec :=
     { name := pin.name, git := pin.git, rev := pin.rev }
   let deps : LeanEvalGenerator.Core.RootDependencies := {
+    solutions := request.solutionDependencies.getD #[]
     mathlib := spec request.mathlib
     extras := (request.dependencies.getD #[]).map
       (LeanEvalGenerator.Core.RootRequire.ofSpec ∘ spec)
@@ -239,7 +241,7 @@ private def ensureKnownFields (label : String) (allowed : Array String)
 
 private def validateJsonShape (value : Json) : Except String Unit := do
   ensureKnownFields "request" #[
-    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies", "templates",
+    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies", "solutionDependencies", "templates",
     "problems"
   ] value
   let mathlib ← value.getObjVal? "mathlib"
@@ -247,6 +249,9 @@ private def validateJsonShape (value : Json) : Except String Unit := do
   if let .ok deps := value.getObjVal? "dependencies" then
     for dep in ← deps.getArr? do
       ensureKnownFields "dependency" #["name", "git", "rev"] dep
+  if let .ok deps := value.getObjVal? "solutionDependencies" then
+    for dep in ← deps.getArr? do
+      ensureKnownFields "solution dependency" #["name", "moduleRoots"] dep
   let templates ← value.getObjVal? "templates"
   ensureKnownFields "templates" #["workspaceTest"] templates
   let problems ← (← value.getObjVal? "problems").getArr?
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index 9013df1..0e23816 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -99,13 +99,37 @@ private def rootRequireOfTable (t : Table) : Except String RootRequire := do
     | other, _ => unsupported := unsupported.push s!"`{other}`"
   return { name, git, rev, unsupportedFields := unsupported }
 
+/-- A package available to solutions, with library roots forbidden in statements. -/
+structure SolutionDependency where
+  name : String
+  moduleRoots : Array String
+  deriving FromJson, Inhabited
+
+/-- Optional consumer policy. Pins remain in the root lakefile. -/
+def loadSolutionDependencies (root : System.FilePath) : IO (Array SolutionDependency) := do
+  let path := root / "solution-dependencies.json"
+  if !(← path.pathExists) then return #[]
+  IO.ofExcept <| (Json.parse (← IO.FS.readFile path)).bind fromJson?
+
+/-- Check external imports after following repository-local helpers. -/
+def checkSolutionImports (solutions : Array SolutionDependency) (imports : Array String) :
+    Except String Unit := do
+  for dep in solutions do
+    if dep.name.isEmpty || dep.moduleRoots.isEmpty || dep.moduleRoots.any String.isEmpty then
+      throw "Solution dependencies require a name and non-empty moduleRoots"
+    for imported in imports do
+      if dep.moduleRoots.any (fun root =>
+          (parseModuleName root).isPrefixOf (parseModuleName imported)) then
+        throw s!"Problem statements may not import solution-only module '{imported}' (package '{dep.name}')"
+
 /-- The dependencies a generated workspace may require, read from the root
 lakefile: the mandatory `mathlib` pin, plus every other root `[[require]]` in
 root lakefile order. An extra require is only emitted into a workspace whose
-problem imports one of its modules; see `workspaceRequires`. -/
+problem imports one of its modules, or is explicitly enabled for solutions; see `workspaceRequires`. -/
 structure RootDependencies where
   mathlib : DependencySpec
   extras : Array RootRequire := #[]
+  solutions : Array SolutionDependency := #[]
   deriving Inhabited
 
 /-- A bare `mathlib` pin is a complete dependency set with no extras, so
@@ -161,6 +185,7 @@ private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : B
   return {
     mathlib := { name := "mathlib", git := git, rev := rev }
     extras := rootRequires.filter (·.name != "mathlib")
+    solutions := ← loadSolutionDependencies root
   }
 
 /-- Read the root `lakefile.toml` for workspace generation: the single
@@ -1358,7 +1383,9 @@ been followed): each extra root require whose `name` equals the first
 component of some imported module, in root lakefile order, followed by
 `mathlib`. For example `import TauCeti.Foo.Bar` selects the require named
 `TauCeti`. Tooling requires in the root lakefile are never selected, because
-no problem imports them. Fails if a selected require cannot be reproduced.
+no problem imports them. Explicit solution dependencies are also emitted, but
+their module roots are rejected in problem imports. Fails if a selected require
+cannot be reproduced.
 
 Known limitation: a package whose library root differs from its package name
 (say package `foo-bar` providing modules `FooBar.*`) is not matched. Its
@@ -1371,11 +1398,16 @@ putting an extra package after Mathlib would make `lake update` pick up that
 package's (typically older) pins instead of Mathlib's. -/
 def workspaceRequires (deps : RootDependencies) (imports : Array String) :
     Except String (Array DependencySpec) := do
+  checkSolutionImports deps.solutions imports
+  for dep in deps.solutions do
+    unless (deps.extras.filter (·.name == dep.name)).size == 1 do
+      throw s!"Solution dependency '{dep.name}' must name exactly one non-mathlib root require"
   let roots : Std.HashSet String := imports.foldl (init := {}) fun acc m =>
     match (splitNameComponents m)[0]? with
     | some r => acc.insert r
     | none => acc
-  let selected ← (deps.extras.filter fun r => roots.contains r.name).mapM (·.toSpec)
+  let selected ← (deps.extras.filter fun r =>
+    roots.contains r.name || deps.solutions.any (·.name == r.name)).mapM (·.toSpec)
   return selected.push deps.mathlib
 
 /-- `workspaceRequires` for the workspace generated from `moduleName`. -/
diff --git a/README.md b/README.md
index e098f44..5113387 100644
--- a/README.md
+++ b/README.md
@@ -55,3 +55,16 @@ transitive dependencies are not pinned in the workspace lakefile. A consumer
 that builds a generated workspace should install the root `lake-manifest.json`
 into it (as lean-eval's CI does) rather than running `lake update`, so that
 every package resolves to the same revision as in the root workspace.
+
+Solution-only packages can be enabled in the consumer's optional
+`solution-dependencies.json`, using names pinned in its root lakefile:
+
+```json
+[{"name": "proof-library", "moduleRoots": ["ProofLibrary"]}]
+```
+
+These packages are included in every workspace without adding statement imports.
+Generation rejects their module roots in statements, including imports through
+local helpers. Library consumers can use `checkSolutionImports` for earlier
+validation. JSON CLI requests use the same array in `solutionDependencies`, with
+the pins supplied in `dependencies`. Omitting the policy preserves existing output.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
index c820e26..afb47c3 100644
--- a/Tests/Dependencies.lean
+++ b/Tests/Dependencies.lean
@@ -119,6 +119,28 @@ def main : IO Unit := do
         (withChallengeDeps := false))
       (mathlibOnlyLakefile "plain")
 
+    -- Enable an unimported package for solutions, retaining root dependency order.
+    IO.FS.writeFile (root / "solution-dependencies.json")
+      "[{\"name\":\"TauCeti\",\"moduleRoots\":[\"TauCeti\"]}]"
+    let solutionDeps ← loadRootDependencies root
+    expectEq "solution dependency included without a statement import"
+      (names (← requiresFor root solutionDeps "LeanEval.Plain")) "#[TauCeti, mathlib]"
+    expectSelectionError solutionDeps "TauCeti" "solution-only"
+    expectSelectionError solutionDeps "«TauCeti»" "solution-only"
+    match ← (requiresFor root solutionDeps "LeanEval.Cfsg").toBaseIO with
+    | .ok _ => throw <| IO.userError "transitive solution import was accepted"
+    | .error e =>
+        unless ((toString e).splitOn "solution-only").length > 1 do throw e
+    expectEq "module root prefix boundary"
+      (names (← IO.ofExcept (workspaceRequires solutionDeps #["TauCetiOther.Foo"])))
+      "#[TauCeti, mathlib]"
+    let missing := { deps with solutions := #[{ name := "missing", moduleRoots := #["Missing"] }] }
+    expectSelectionError missing "Mathlib" "must name exactly one"
+    let unpinned := { deps with solutions := #[{ name := "Cli", moduleRoots := #["Cli"] }] }
+    expectSelectionError unpinned "Mathlib" "does not pin"
+    let invalid := { deps with solutions := #[{ name := "TauCeti", moduleRoots := #[] }] }
+    expectSelectionError invalid "Mathlib" "non-empty moduleRoots"
+
     -- Values are TOML-escaped; ordinary values are emitted verbatim.
     expectEq "plain TOML string" (tomlBasicString "https://x.org/a-b_c.git")
       "\"https://x.org/a-b_c.git\""
diff --git a/schemas/request-v1.schema.json b/schemas/request-v1.schema.json
index 3c80161..bc19af7 100644
--- a/schemas/request-v1.schema.json
+++ b/schemas/request-v1.schema.json
@@ -21,6 +21,21 @@
       "type": "array",
       "items": { "$ref": "#/$defs/extraDependency" }
     },
+    "solutionDependencies": {
+      "type": "array",
+      "items": {
+        "type": "object",
+        "additionalProperties": false,
+        "required": ["name", "moduleRoots"],
+        "properties": {
+          "name": { "type": "string", "minLength": 1 },
+          "moduleRoots": {
+            "type": "array", "minItems": 1,
+            "items": { "type": "string", "minLength": 1 }
+          }
+        }
+      }
+    },
     "templates": {
       "type": "object",
       "additionalProperties": false,
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index bd003d7..4f01244 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -115,6 +115,22 @@ def check_extra_dependencies() -> None:
                 assert lakefile.count("[[require]]") == 2, lakefile
             else:
                 assert lakefile == baseline, lakefile
+                original_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
+                payload["solutionDependencies"] = [
+                    {"name": "TauCeti", "moduleRoots": ["TauCeti"]}
+                ]
+                assert tauceti + mathlib in lakefile_for(payload)
+                updated_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
+                assert [f for f in updated_files if f["path"] != "lakefile.toml"] == [
+                    f for f in original_files if f["path"] != "lakefile.toml"
+                ]
+                payload["solutionDependencies"][0]["unexpected"] = True
+                assert_rejected(payload, "solution dependency contains an unknown field")
+            if module == "WithTauCeti":
+                payload["solutionDependencies"] = [
+                    {"name": "TauCeti", "moduleRoots": ["TauCeti"]}
+                ]
+                assert_rejected(payload, "solution-only")
 
 
 def main() -> int:

From bd54907811ed256e67e0f67f785d8d1a2b8981df Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sun, 27 Sep 2026 18:24:00 -0500
Subject: [PATCH 2/3] Clarify solution dependency policy and isolate its tests

---
 LeanEvalGenerator/Contract.lean      |  6 ++-
 LeanEvalGenerator/Core/Generate.lean | 20 +++++----
 README.md                            | 22 +++++-----
 Tests/Dependencies.lean              | 63 ++++++++++++++++++----------
 tests/scripts/contract.py            | 55 +++++++++++++++++-------
 5 files changed, 107 insertions(+), 59 deletions(-)

diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index db2c09d..315625f 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -63,6 +63,8 @@ structure GenerateRequest where
   `LeanEvalGenerator.Core.workspaceRequires`). Omitting the field means no
   extra requires, which is how every earlier version 1 request behaves. -/
   dependencies : Option (Array DependencyPin) := none
+  /-- Packages included without statement imports; their module roots are
+  forbidden in statements. Names refer to pins in `dependencies`. -/
   solutionDependencies : Option (Array Core.SolutionDependency) := none
   templates : TemplateInputs
   problems : Array ProblemInput
@@ -241,8 +243,8 @@ private def ensureKnownFields (label : String) (allowed : Array String)
 
 private def validateJsonShape (value : Json) : Except String Unit := do
   ensureKnownFields "request" #[
-    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies", "solutionDependencies", "templates",
-    "problems"
+    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies",
+    "solutionDependencies", "templates", "problems"
   ] value
   let mathlib ← value.getObjVal? "mathlib"
   ensureKnownFields "mathlib" #["name", "git", "rev"] mathlib
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index 0e23816..23e1bff 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -109,7 +109,8 @@ structure SolutionDependency where
 def loadSolutionDependencies (root : System.FilePath) : IO (Array SolutionDependency) := do
   let path := root / "solution-dependencies.json"
   if !(← path.pathExists) then return #[]
-  IO.ofExcept <| (Json.parse (← IO.FS.readFile path)).bind fromJson?
+  let parsed := (Json.parse (← IO.FS.readFile path)).bind fromJson?
+  IO.ofExcept <| parsed.mapError (fun err => s!"{path}: {err}")
 
 /-- Check external imports after following repository-local helpers. -/
 def checkSolutionImports (solutions : Array SolutionDependency) (imports : Array String) :
@@ -120,12 +121,14 @@ def checkSolutionImports (solutions : Array SolutionDependency) (imports : Array
     for imported in imports do
       if dep.moduleRoots.any (fun root =>
           (parseModuleName root).isPrefixOf (parseModuleName imported)) then
-        throw s!"Problem statements may not import solution-only module '{imported}' (package '{dep.name}')"
+        throw s!"Problem statements may not import solution-only module '{imported}' \
+          (package '{dep.name}')"
 
 /-- The dependencies a generated workspace may require, read from the root
 lakefile: the mandatory `mathlib` pin, plus every other root `[[require]]` in
 root lakefile order. An extra require is only emitted into a workspace whose
-problem imports one of its modules, or is explicitly enabled for solutions; see `workspaceRequires`. -/
+problem imports one of its modules, or is explicitly enabled for solutions;
+see `workspaceRequires`. -/
 structure RootDependencies where
   mathlib : DependencySpec
   extras : Array RootRequire := #[]
@@ -185,16 +188,17 @@ private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : B
   return {
     mathlib := { name := "mathlib", git := git, rev := rev }
     extras := rootRequires.filter (·.name != "mathlib")
-    solutions := ← loadSolutionDependencies root
   }
 
 /-- Read the root `lakefile.toml` for workspace generation: the single
 `mathlib` require, which must be a plain git require with non-empty `git` and
 `rev` and no other fields, and every other require as written. Other requires
 are not validated here; a problem that selects one fails if it cannot be
-reproduced (see `RootRequire.toSpec`). -/
-def loadRootDependencies (root : System.FilePath) : IO RootDependencies :=
-  loadRootDependenciesCore root (strictMathlib := true)
+reproduced (see `RootRequire.toSpec`). Also read the optional solution-only
+policy; the legacy Mathlib-only loader does not depend on that file. -/
+def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
+  return { (← loadRootDependenciesCore root (strictMathlib := true)) with
+    solutions := ← loadSolutionDependencies root }
 
 /-- The root `mathlib` pin. Unlike `loadRootDependencies`, this ignores
 fields beyond `name`, `git` and `rev`, as it always has. -/
@@ -1387,7 +1391,7 @@ no problem imports them. Explicit solution dependencies are also emitted, but
 their module roots are rejected in problem imports. Fails if a selected require
 cannot be reproduced.
 
-Known limitation: a package whose library root differs from its package name
+Known limitation for statement imports: a library root differing from its package name
 (say package `foo-bar` providing modules `FooBar.*`) is not matched. Its
 workspace then lacks the require, and the workspace build fails loudly on the
 missing import rather than silently changing the statement.
diff --git a/README.md b/README.md
index 5113387..d020288 100644
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@ problem may also import modules from another package. The library API reads
 the candidate packages from the consumer's root `lakefile.toml`
 (`loadRootDependencies`); a CLI request lists them in the optional
 `dependencies` array of `{name, git, rev}` pins, and omitting that array means
-Mathlib only. A candidate is required by a workspace exactly when its `name`
+Mathlib only. By default, a candidate is required by a workspace when its `name`
 equals the first component of a module the problem imports, after following
 repo-local imports: `import TauCeti.Foo.Bar` selects the package named
 `TauCeti`. Tooling packages are therefore never required, because no problem
@@ -46,25 +46,25 @@ Mathlib's pins.
 A selected root require must be a plain git require with a non-empty `git` and
 `rev`; `subDir`, `scope`, `options`, a table-valued `git` or any other field is
 an error, since the workspace would not reproduce it. Unselected requires are
-not checked. A package whose library root differs from its package name is not
-matched; the generated workspace then fails to build on the missing import
+not checked. For statement imports, a package whose library root differs from
+its package name is not matched; the workspace then fails on the missing import
 rather than silently changing the statement.
 
-The emitted requires are pruned to what the problem imports, but their
-transitive dependencies are not pinned in the workspace lakefile. A consumer
+Transitive dependencies are not pinned in the workspace lakefile. A consumer
 that builds a generated workspace should install the root `lake-manifest.json`
 into it (as lean-eval's CI does) rather than running `lake update`, so that
 every package resolves to the same revision as in the root workspace.
 
-Solution-only packages can be enabled in the consumer's optional
-`solution-dependencies.json`, using names pinned in its root lakefile:
+Solution-only packages use the same resolver, but are included even when the
+problem does not import them. Enable them in the consumer's optional
+`solution-dependencies.json`, using package names pinned in its root lakefile:
 
 ```json
 [{"name": "proof-library", "moduleRoots": ["ProofLibrary"]}]
 ```
 
-These packages are included in every workspace without adding statement imports.
-Generation rejects their module roots in statements, including imports through
-local helpers. Library consumers can use `checkSolutionImports` for earlier
-validation. JSON CLI requests use the same array in `solutionDependencies`, with
+The package name and module roots may differ, as with `lean-pool` and `LeanPool`.
+Generation rejects the listed module roots in statements, including imports
+through local helpers. TauCeti's existing statement-import behavior is unchanged.
+JSON CLI requests use the same array in `solutionDependencies`, with
 the pins supplied in `dependencies`. Omitting the policy preserves existing output.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
index afb47c3..cacff8c 100644
--- a/Tests/Dependencies.lean
+++ b/Tests/Dependencies.lean
@@ -72,6 +72,46 @@ private def expectSelectionError (deps : RootDependencies) (package expected : S
 private def names (specs : Array DependencySpec) : String :=
   toString (specs.map (·.name))
 
+/-- ProofLibrary models a solution-only package whose Lake name differs from
+its module root, as lean-pool/LeanPool do. TauCeti keeps its existing policy. -/
+private def checkSolutionDependencies (root : System.FilePath) : IO Unit := do
+  IO.FS.createDirAll root
+  IO.FS.writeFile (root / "lakefile.toml") <|
+    rootLakefile ++ requireBlock "proof-library" "https://proof.example/library" "proof-pin"
+  writeModule root "Plain" "import Mathlib.Data.Nat.Basic\n"
+  writeModule root "WithTauCeti" "import TauCeti.GroupTheory.Classification\n"
+  writeModule root "WithHelper" "import Helper\n"
+  writeModule root "Helper" "import ProofLibrary.Basic\n"
+  IO.FS.writeFile (root / "solution-dependencies.json")
+    "[{\"name\":\"proof-library\",\"moduleRoots\":[\"ProofLibrary\"]}]"
+  let deps ← loadRootDependencies root
+  expectEq "solution dependency included without a statement import"
+    (names (← requiresFor root deps "Plain")) "#[proof-library, mathlib]"
+  expectEq "TauCeti remains available to statements; Mathlib stays last"
+    (names (← requiresFor root deps "WithTauCeti")) "#[TauCeti, proof-library, mathlib]"
+  expectSelectionError deps "ProofLibrary" "solution-only"
+  expectSelectionError deps "«ProofLibrary»" "solution-only"
+  match ← (requiresFor root deps "WithHelper").toBaseIO with
+  | .ok _ => throw <| IO.userError "transitive solution import was accepted"
+  | .error e =>
+      unless ((toString e).splitOn "solution-only").length > 1 do throw e
+  expectEq "module root prefix boundary"
+    (names (← IO.ofExcept (workspaceRequires deps #["ProofLibraryOther.Foo"])))
+    "#[proof-library, mathlib]"
+  let missing := { deps with solutions := #[{ name := "missing", moduleRoots := #["Missing"] }] }
+  expectSelectionError missing "Mathlib" "must name exactly one"
+  let unpinned := { deps with solutions := #[{ name := "Cli", moduleRoots := #["Cli"] }] }
+  expectSelectionError unpinned "Mathlib" "does not pin"
+  let invalid := { deps with solutions := #[{ name := "proof-library", moduleRoots := #[] }] }
+  expectSelectionError invalid "Mathlib" "non-empty moduleRoots"
+  IO.FS.writeFile (root / "solution-dependencies.json") "invalid JSON"
+  expectEq "legacy Mathlib loader is independent of solution policy"
+    (← loadRootMathlibDependency root).rev mathlibRev
+  match ← (loadRootDependencies root).toBaseIO with
+  | .ok _ => throw <| IO.userError "malformed solution policy was accepted"
+  | .error e =>
+      unless ((toString e).splitOn "solution-dependencies.json").length > 1 do throw e
+
 def main : IO Unit := do
   let root ← IO.FS.createTempDir
   try
@@ -119,28 +159,6 @@ def main : IO Unit := do
         (withChallengeDeps := false))
       (mathlibOnlyLakefile "plain")
 
-    -- Enable an unimported package for solutions, retaining root dependency order.
-    IO.FS.writeFile (root / "solution-dependencies.json")
-      "[{\"name\":\"TauCeti\",\"moduleRoots\":[\"TauCeti\"]}]"
-    let solutionDeps ← loadRootDependencies root
-    expectEq "solution dependency included without a statement import"
-      (names (← requiresFor root solutionDeps "LeanEval.Plain")) "#[TauCeti, mathlib]"
-    expectSelectionError solutionDeps "TauCeti" "solution-only"
-    expectSelectionError solutionDeps "«TauCeti»" "solution-only"
-    match ← (requiresFor root solutionDeps "LeanEval.Cfsg").toBaseIO with
-    | .ok _ => throw <| IO.userError "transitive solution import was accepted"
-    | .error e =>
-        unless ((toString e).splitOn "solution-only").length > 1 do throw e
-    expectEq "module root prefix boundary"
-      (names (← IO.ofExcept (workspaceRequires solutionDeps #["TauCetiOther.Foo"])))
-      "#[TauCeti, mathlib]"
-    let missing := { deps with solutions := #[{ name := "missing", moduleRoots := #["Missing"] }] }
-    expectSelectionError missing "Mathlib" "must name exactly one"
-    let unpinned := { deps with solutions := #[{ name := "Cli", moduleRoots := #["Cli"] }] }
-    expectSelectionError unpinned "Mathlib" "does not pin"
-    let invalid := { deps with solutions := #[{ name := "TauCeti", moduleRoots := #[] }] }
-    expectSelectionError invalid "Mathlib" "non-empty moduleRoots"
-
     -- Values are TOML-escaped; ordinary values are emitted verbatim.
     expectEq "plain TOML string" (tomlBasicString "https://x.org/a-b_c.git")
       "\"https://x.org/a-b_c.git\""
@@ -169,6 +187,7 @@ def main : IO Unit := do
     unless ((lakefileToml "a\"b" #[] (withChallengeDeps := false)).startsWith
         "name = \"a\\\"b\"\n") do
       throw <| IO.userError "workspace name is not TOML-escaped"
+    checkSolutionDependencies (root / "solution-only")
   finally
     IO.FS.removeDirAll root
   IO.println "dependency tests passed"
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index 4f01244..c92f150 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -115,22 +115,44 @@ def check_extra_dependencies() -> None:
                 assert lakefile.count("[[require]]") == 2, lakefile
             else:
                 assert lakefile == baseline, lakefile
-                original_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
-                payload["solutionDependencies"] = [
-                    {"name": "TauCeti", "moduleRoots": ["TauCeti"]}
-                ]
-                assert tauceti + mathlib in lakefile_for(payload)
-                updated_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
-                assert [f for f in updated_files if f["path"] != "lakefile.toml"] == [
-                    f for f in original_files if f["path"] != "lakefile.toml"
-                ]
-                payload["solutionDependencies"][0]["unexpected"] = True
-                assert_rejected(payload, "solution dependency contains an unknown field")
-            if module == "WithTauCeti":
-                payload["solutionDependencies"] = [
-                    {"name": "TauCeti", "moduleRoots": ["TauCeti"]}
-                ]
-                assert_rejected(payload, "solution-only")
+
+
+def check_solution_dependencies() -> None:
+    """ProofLibrary is available to proofs; it must not change the statement environment."""
+    with tempfile.TemporaryDirectory() as directory:
+        context = Path(directory)
+        fixture = problem()
+        content = fixture["moduleContent"]
+        hole = fixture["resolvedHoles"][0]
+        hole["declarationName"] = "fixture"
+        hole["endColumn"] = len(content.rstrip())
+        (context / "Fixture.lean").write_text(content, encoding="utf-8")
+        ilean = context / ".lake/build/lib/lean"
+        ilean.mkdir(parents=True)
+        (ilean / "Fixture.ilean").write_text('{"decls": {}}', encoding="utf-8")
+        payload = request_with(fixture)
+        payload["contextRoot"] = str(context)
+        payload["dependencies"] = [
+            {"name": "proof-library", "git": "https://proof.example/library", "rev": "proof-pin"}
+        ]
+        assert 'name = "proof-library"' not in lakefile_for(payload)
+        original_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
+        payload["solutionDependencies"] = [
+            {"name": "proof-library", "moduleRoots": ["ProofLibrary"]}
+        ]
+        lakefile = lakefile_for(payload)
+        assert lakefile.index('name = "proof-library"') < lakefile.index('name = "mathlib"')
+        updated_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
+        assert [f for f in updated_files if f["path"] != "lakefile.toml"] == [
+            f for f in original_files if f["path"] != "lakefile.toml"
+        ]
+        payload["solutionDependencies"][0]["unexpected"] = True
+        assert_rejected(payload, "solution dependency contains an unknown field")
+        del payload["solutionDependencies"][0]["unexpected"]
+        fixture["moduleContent"] = "import ProofLibrary.Basic\n" + content
+        (context / "Fixture.lean").write_text(fixture["moduleContent"], encoding="utf-8")
+        hole["startLine"] = hole["endLine"] = 2
+        assert_rejected(payload, "solution-only")
 
 
 def main() -> int:
@@ -232,6 +254,7 @@ def main() -> int:
         assert_rejected(request_with(invalid_id), "is invalid")
 
     check_extra_dependencies()
+    check_solution_dependencies()
 
     print("PASS schema errors stay off stdout and quoted source/ilean paths resolve")
     return 0

From 0c9c5ce33933c5d19e817abfd918f552e6db60fe Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Sun, 27 Sep 2026 18:42:22 -0500
Subject: [PATCH 3/3] Reduce solution dependencies to shared policy and
 resolver

---
 LeanEvalGenerator/Contract.lean      | 12 ++----
 LeanEvalGenerator/Core/Generate.lean | 39 +++++++-----------
 README.md                            | 27 +++++--------
 Tests/Dependencies.lean              | 59 +++++++++-------------------
 schemas/request-v1.schema.json       | 15 -------
 tests/scripts/contract.py            | 39 ------------------
 6 files changed, 45 insertions(+), 146 deletions(-)

diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index 315625f..7b0a216 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -63,9 +63,6 @@ structure GenerateRequest where
   `LeanEvalGenerator.Core.workspaceRequires`). Omitting the field means no
   extra requires, which is how every earlier version 1 request behaves. -/
   dependencies : Option (Array DependencyPin) := none
-  /-- Packages included without statement imports; their module roots are
-  forbidden in statements. Names refer to pins in `dependencies`. -/
-  solutionDependencies : Option (Array Core.SolutionDependency) := none
   templates : TemplateInputs
   problems : Array ProblemInput
   deriving FromJson
@@ -216,7 +213,7 @@ def render (request : GenerateRequest) : IO String := do
   let spec (pin : DependencyPin) : LeanEvalGenerator.Core.DependencySpec :=
     { name := pin.name, git := pin.git, rev := pin.rev }
   let deps : LeanEvalGenerator.Core.RootDependencies := {
-    solutions := request.solutionDependencies.getD #[]
+    solutions := ← Core.loadSolutionDependencies request.contextRoot
     mathlib := spec request.mathlib
     extras := (request.dependencies.getD #[]).map
       (LeanEvalGenerator.Core.RootRequire.ofSpec ∘ spec)
@@ -243,17 +240,14 @@ private def ensureKnownFields (label : String) (allowed : Array String)
 
 private def validateJsonShape (value : Json) : Except String Unit := do
   ensureKnownFields "request" #[
-    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies",
-    "solutionDependencies", "templates", "problems"
+    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "dependencies", "templates",
+    "problems"
   ] value
   let mathlib ← value.getObjVal? "mathlib"
   ensureKnownFields "mathlib" #["name", "git", "rev"] mathlib
   if let .ok deps := value.getObjVal? "dependencies" then
     for dep in ← deps.getArr? do
       ensureKnownFields "dependency" #["name", "git", "rev"] dep
-  if let .ok deps := value.getObjVal? "solutionDependencies" then
-    for dep in ← deps.getArr? do
-      ensureKnownFields "solution dependency" #["name", "moduleRoots"] dep
   let templates ← value.getObjVal? "templates"
   ensureKnownFields "templates" #["workspaceTest"] templates
   let problems ← (← value.getObjVal? "problems").getArr?
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index 23e1bff..486ffbd 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -99,36 +99,22 @@ private def rootRequireOfTable (t : Table) : Except String RootRequire := do
     | other, _ => unsupported := unsupported.push s!"`{other}`"
   return { name, git, rev, unsupportedFields := unsupported }
 
-/-- A package available to solutions, with library roots forbidden in statements. -/
+/-- A pinned package available to solutions but forbidden in statement imports. -/
 structure SolutionDependency where
   name : String
   moduleRoots : Array String
   deriving FromJson, Inhabited
 
-/-- Optional consumer policy. Pins remain in the root lakefile. -/
+/-- Optional consumer policy; dependency pins remain in the root lakefile. -/
 def loadSolutionDependencies (root : System.FilePath) : IO (Array SolutionDependency) := do
   let path := root / "solution-dependencies.json"
   if !(← path.pathExists) then return #[]
-  let parsed := (Json.parse (← IO.FS.readFile path)).bind fromJson?
-  IO.ofExcept <| parsed.mapError (fun err => s!"{path}: {err}")
-
-/-- Check external imports after following repository-local helpers. -/
-def checkSolutionImports (solutions : Array SolutionDependency) (imports : Array String) :
-    Except String Unit := do
-  for dep in solutions do
-    if dep.name.isEmpty || dep.moduleRoots.isEmpty || dep.moduleRoots.any String.isEmpty then
-      throw "Solution dependencies require a name and non-empty moduleRoots"
-    for imported in imports do
-      if dep.moduleRoots.any (fun root =>
-          (parseModuleName root).isPrefixOf (parseModuleName imported)) then
-        throw s!"Problem statements may not import solution-only module '{imported}' \
-          (package '{dep.name}')"
+  IO.ofExcept <| (Json.parse (← IO.FS.readFile path)).bind fromJson?
 
 /-- The dependencies a generated workspace may require, read from the root
 lakefile: the mandatory `mathlib` pin, plus every other root `[[require]]` in
 root lakefile order. An extra require is only emitted into a workspace whose
-problem imports one of its modules, or is explicitly enabled for solutions;
-see `workspaceRequires`. -/
+problem imports one of its modules, or it is enabled for solutions; see `workspaceRequires`. -/
 structure RootDependencies where
   mathlib : DependencySpec
   extras : Array RootRequire := #[]
@@ -194,8 +180,7 @@ private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : B
 `mathlib` require, which must be a plain git require with non-empty `git` and
 `rev` and no other fields, and every other require as written. Other requires
 are not validated here; a problem that selects one fails if it cannot be
-reproduced (see `RootRequire.toSpec`). Also read the optional solution-only
-policy; the legacy Mathlib-only loader does not depend on that file. -/
+reproduced (see `RootRequire.toSpec`). -/
 def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
   return { (← loadRootDependenciesCore root (strictMathlib := true)) with
     solutions := ← loadSolutionDependencies root }
@@ -1387,11 +1372,10 @@ been followed): each extra root require whose `name` equals the first
 component of some imported module, in root lakefile order, followed by
 `mathlib`. For example `import TauCeti.Foo.Bar` selects the require named
 `TauCeti`. Tooling requires in the root lakefile are never selected, because
-no problem imports them. Explicit solution dependencies are also emitted, but
-their module roots are rejected in problem imports. Fails if a selected require
-cannot be reproduced.
+no problem imports them. Solution dependencies are always included, but their
+module roots are forbidden in statements. Fails if a selected require cannot be reproduced.
 
-Known limitation for statement imports: a library root differing from its package name
+Known limitation: a package whose library root differs from its package name
 (say package `foo-bar` providing modules `FooBar.*`) is not matched. Its
 workspace then lacks the require, and the workspace build fails loudly on the
 missing import rather than silently changing the statement.
@@ -1402,10 +1386,15 @@ putting an extra package after Mathlib would make `lake update` pick up that
 package's (typically older) pins instead of Mathlib's. -/
 def workspaceRequires (deps : RootDependencies) (imports : Array String) :
     Except String (Array DependencySpec) := do
-  checkSolutionImports deps.solutions imports
   for dep in deps.solutions do
     unless (deps.extras.filter (·.name == dep.name)).size == 1 do
       throw s!"Solution dependency '{dep.name}' must name exactly one non-mathlib root require"
+    if dep.moduleRoots.isEmpty || dep.moduleRoots.any String.isEmpty then
+      throw s!"Solution dependency '{dep.name}' requires non-empty moduleRoots"
+    for imported in imports do
+      if dep.moduleRoots.any (fun root =>
+          (parseModuleName root).isPrefixOf (parseModuleName imported)) then
+        throw s!"Problem statements may not import solution-only module '{imported}'"
   let roots : Std.HashSet String := imports.foldl (init := {}) fun acc m =>
     match (splitNameComponents m)[0]? with
     | some r => acc.insert r
diff --git a/README.md b/README.md
index d020288..17a0963 100644
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@ problem may also import modules from another package. The library API reads
 the candidate packages from the consumer's root `lakefile.toml`
 (`loadRootDependencies`); a CLI request lists them in the optional
 `dependencies` array of `{name, git, rev}` pins, and omitting that array means
-Mathlib only. By default, a candidate is required by a workspace when its `name`
+Mathlib only. A candidate is required by a workspace exactly when its `name`
 equals the first component of a module the problem imports, after following
 repo-local imports: `import TauCeti.Foo.Bar` selects the package named
 `TauCeti`. Tooling packages are therefore never required, because no problem
@@ -46,25 +46,18 @@ Mathlib's pins.
 A selected root require must be a plain git require with a non-empty `git` and
 `rev`; `subDir`, `scope`, `options`, a table-valued `git` or any other field is
 an error, since the workspace would not reproduce it. Unselected requires are
-not checked. For statement imports, a package whose library root differs from
-its package name is not matched; the workspace then fails on the missing import
+not checked. A package whose library root differs from its package name is not
+matched; the generated workspace then fails to build on the missing import
 rather than silently changing the statement.
 
-Transitive dependencies are not pinned in the workspace lakefile. A consumer
+The emitted requires are pruned to what the problem imports, but their
+transitive dependencies are not pinned in the workspace lakefile. A consumer
 that builds a generated workspace should install the root `lake-manifest.json`
 into it (as lean-eval's CI does) rather than running `lake update`, so that
 every package resolves to the same revision as in the root workspace.
 
-Solution-only packages use the same resolver, but are included even when the
-problem does not import them. Enable them in the consumer's optional
-`solution-dependencies.json`, using package names pinned in its root lakefile:
-
-```json
-[{"name": "proof-library", "moduleRoots": ["ProofLibrary"]}]
-```
-
-The package name and module roots may differ, as with `lean-pool` and `LeanPool`.
-Generation rejects the listed module roots in statements, including imports
-through local helpers. TauCeti's existing statement-import behavior is unchanged.
-JSON CLI requests use the same array in `solutionDependencies`, with
-the pins supplied in `dependencies`. Omitting the policy preserves existing output.
+To enable a package for solutions only, add `solution-dependencies.json` to the
+consumer root (`contextRoot` for JSON requests), for example:
+`[{"name": "lean-pool", "moduleRoots": ["LeanPool", "Challenge", "Solution"]}]`.
+The package must be pinned in the existing dependencies. It is included in every
+workspace; imports of its listed module roots in statements or local helpers are rejected.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
index cacff8c..508ef15 100644
--- a/Tests/Dependencies.lean
+++ b/Tests/Dependencies.lean
@@ -72,46 +72,6 @@ private def expectSelectionError (deps : RootDependencies) (package expected : S
 private def names (specs : Array DependencySpec) : String :=
   toString (specs.map (·.name))
 
-/-- ProofLibrary models a solution-only package whose Lake name differs from
-its module root, as lean-pool/LeanPool do. TauCeti keeps its existing policy. -/
-private def checkSolutionDependencies (root : System.FilePath) : IO Unit := do
-  IO.FS.createDirAll root
-  IO.FS.writeFile (root / "lakefile.toml") <|
-    rootLakefile ++ requireBlock "proof-library" "https://proof.example/library" "proof-pin"
-  writeModule root "Plain" "import Mathlib.Data.Nat.Basic\n"
-  writeModule root "WithTauCeti" "import TauCeti.GroupTheory.Classification\n"
-  writeModule root "WithHelper" "import Helper\n"
-  writeModule root "Helper" "import ProofLibrary.Basic\n"
-  IO.FS.writeFile (root / "solution-dependencies.json")
-    "[{\"name\":\"proof-library\",\"moduleRoots\":[\"ProofLibrary\"]}]"
-  let deps ← loadRootDependencies root
-  expectEq "solution dependency included without a statement import"
-    (names (← requiresFor root deps "Plain")) "#[proof-library, mathlib]"
-  expectEq "TauCeti remains available to statements; Mathlib stays last"
-    (names (← requiresFor root deps "WithTauCeti")) "#[TauCeti, proof-library, mathlib]"
-  expectSelectionError deps "ProofLibrary" "solution-only"
-  expectSelectionError deps "«ProofLibrary»" "solution-only"
-  match ← (requiresFor root deps "WithHelper").toBaseIO with
-  | .ok _ => throw <| IO.userError "transitive solution import was accepted"
-  | .error e =>
-      unless ((toString e).splitOn "solution-only").length > 1 do throw e
-  expectEq "module root prefix boundary"
-    (names (← IO.ofExcept (workspaceRequires deps #["ProofLibraryOther.Foo"])))
-    "#[proof-library, mathlib]"
-  let missing := { deps with solutions := #[{ name := "missing", moduleRoots := #["Missing"] }] }
-  expectSelectionError missing "Mathlib" "must name exactly one"
-  let unpinned := { deps with solutions := #[{ name := "Cli", moduleRoots := #["Cli"] }] }
-  expectSelectionError unpinned "Mathlib" "does not pin"
-  let invalid := { deps with solutions := #[{ name := "proof-library", moduleRoots := #[] }] }
-  expectSelectionError invalid "Mathlib" "non-empty moduleRoots"
-  IO.FS.writeFile (root / "solution-dependencies.json") "invalid JSON"
-  expectEq "legacy Mathlib loader is independent of solution policy"
-    (← loadRootMathlibDependency root).rev mathlibRev
-  match ← (loadRootDependencies root).toBaseIO with
-  | .ok _ => throw <| IO.userError "malformed solution policy was accepted"
-  | .error e =>
-      unless ((toString e).splitOn "solution-dependencies.json").length > 1 do throw e
-
 def main : IO Unit := do
   let root ← IO.FS.createTempDir
   try
@@ -187,7 +147,24 @@ def main : IO Unit := do
     unless ((lakefileToml "a\"b" #[] (withChallengeDeps := false)).startsWith
         "name = \"a\\\"b\"\n") do
       throw <| IO.userError "workspace name is not TOML-escaped"
-    checkSolutionDependencies (root / "solution-only")
+    -- Lean Pool is available without statement imports; TauCeti still works as before.
+    IO.FS.writeFile (root / "lakefile.toml") <|
+      rootLakefile ++ requireBlock "lean-pool" "https://example.com/lean-pool.git" "pool-pin"
+    IO.FS.writeFile (root / "solution-dependencies.json")
+      "[{\"name\":\"lean-pool\",\"moduleRoots\":[\"LeanPool\",\"Challenge\",\"Solution\"]}]"
+    let poolDeps ← loadRootDependencies root
+    expectEq "solution dependency without statement import"
+      (names (← requiresFor root poolDeps "LeanEval.Plain")) "#[lean-pool, mathlib]"
+    expectEq "solution dependency with TauCeti"
+      (names (← requiresFor root poolDeps "LeanEval.Cfsg")) "#[TauCeti, lean-pool, mathlib]"
+    expectSelectionError poolDeps "LeanPool" "solution-only"
+    expectSelectionError poolDeps "«LeanPool»" "solution-only"
+    writeModule root "LeanEval.Plain" "import LeanEval.PoolHelper\n"
+    writeModule root "LeanEval.PoolHelper" "import LeanPool.Basic\n"
+    match ← (requiresFor root poolDeps "LeanEval.Plain").toBaseIO with
+    | .ok _ => throw <| IO.userError "solution-only import through a helper was accepted"
+    | .error e =>
+        unless ((toString e).splitOn "solution-only").length > 1 do throw e
   finally
     IO.FS.removeDirAll root
   IO.println "dependency tests passed"
diff --git a/schemas/request-v1.schema.json b/schemas/request-v1.schema.json
index bc19af7..3c80161 100644
--- a/schemas/request-v1.schema.json
+++ b/schemas/request-v1.schema.json
@@ -21,21 +21,6 @@
       "type": "array",
       "items": { "$ref": "#/$defs/extraDependency" }
     },
-    "solutionDependencies": {
-      "type": "array",
-      "items": {
-        "type": "object",
-        "additionalProperties": false,
-        "required": ["name", "moduleRoots"],
-        "properties": {
-          "name": { "type": "string", "minLength": 1 },
-          "moduleRoots": {
-            "type": "array", "minItems": 1,
-            "items": { "type": "string", "minLength": 1 }
-          }
-        }
-      }
-    },
     "templates": {
       "type": "object",
       "additionalProperties": false,
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index c92f150..bd003d7 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -117,44 +117,6 @@ def check_extra_dependencies() -> None:
                 assert lakefile == baseline, lakefile
 
 
-def check_solution_dependencies() -> None:
-    """ProofLibrary is available to proofs; it must not change the statement environment."""
-    with tempfile.TemporaryDirectory() as directory:
-        context = Path(directory)
-        fixture = problem()
-        content = fixture["moduleContent"]
-        hole = fixture["resolvedHoles"][0]
-        hole["declarationName"] = "fixture"
-        hole["endColumn"] = len(content.rstrip())
-        (context / "Fixture.lean").write_text(content, encoding="utf-8")
-        ilean = context / ".lake/build/lib/lean"
-        ilean.mkdir(parents=True)
-        (ilean / "Fixture.ilean").write_text('{"decls": {}}', encoding="utf-8")
-        payload = request_with(fixture)
-        payload["contextRoot"] = str(context)
-        payload["dependencies"] = [
-            {"name": "proof-library", "git": "https://proof.example/library", "rev": "proof-pin"}
-        ]
-        assert 'name = "proof-library"' not in lakefile_for(payload)
-        original_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
-        payload["solutionDependencies"] = [
-            {"name": "proof-library", "moduleRoots": ["ProofLibrary"]}
-        ]
-        lakefile = lakefile_for(payload)
-        assert lakefile.index('name = "proof-library"') < lakefile.index('name = "mathlib"')
-        updated_files = json.loads(invoke(json.dumps(payload)).stdout)["files"]
-        assert [f for f in updated_files if f["path"] != "lakefile.toml"] == [
-            f for f in original_files if f["path"] != "lakefile.toml"
-        ]
-        payload["solutionDependencies"][0]["unexpected"] = True
-        assert_rejected(payload, "solution dependency contains an unknown field")
-        del payload["solutionDependencies"][0]["unexpected"]
-        fixture["moduleContent"] = "import ProofLibrary.Basic\n" + content
-        (context / "Fixture.lean").write_text(fixture["moduleContent"], encoding="utf-8")
-        hole["startLine"] = hole["endLine"] = 2
-        assert_rejected(payload, "solution-only")
-
-
 def main() -> int:
     subprocess.run(["lake", "build"], cwd=ROOT, check=True)
     subprocess.run(
@@ -254,7 +216,6 @@ def main() -> int:
         assert_rejected(request_with(invalid_id), "is invalid")
 
     check_extra_dependencies()
-    check_solution_dependencies()
 
     print("PASS schema errors stay off stdout and quoted source/ilean paths resolve")
     return 0