Support solution-only workspace dependencies

LeanEvalGenerator/Contract.lean

@@ -213,6 +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 := ← Core.loadSolutionDependencies request.contextRoot
     mathlib := spec request.mathlib
     extras := (request.dependencies.getD #[]).map
       (LeanEvalGenerator.Core.RootRequire.ofSpec ∘ spec)

LeanEvalGenerator/Core/Generate.lean

@@ -99,13 +99,26 @@ private def rootRequireOfTable (t : Table) : Except String RootRequire := do
     | other, _ => unsupported := unsupported.push s!"`{other}`"
   return { name, git, rev, unsupportedFields := unsupported }
 
+/-- 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; 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 #[]
+  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; see `workspaceRequires`. -/
+problem imports one of its modules, or it is 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
@@ -168,8 +181,9 @@ private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : B
 `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)
+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. -/
@@ -1358,7 +1372,8 @@ 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. Solution dependencies are always included, but their
+module roots are forbidden in statements. 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 +1386,21 @@ 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
+  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
     | 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`. -/

README.md

@@ -55,3 +55,9 @@ 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.
+
+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.

Tests/Dependencies.lean

@@ -147,6 +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"
+    -- 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"