From eabb0fce603d6b65e9409af83d13853c2b789c94 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 25 Sep 2026 12:21:53 +0000
Subject: [PATCH 1/3] feat: require imported root dependencies in generated
 workspaces

A problem statement may import a package other than Mathlib, for example
TauCeti for the classification of finite simple groups. Its generated
workspace then needs a `[[require]]` for that package, but the root
lakefile also requires tooling packages (Cli, lean-eval-generator) that
must never leak into a workspace.

`loadRootDependencies` now reads the mathlib pin together with every other
git-pinned root require, and each workspace lakefile requires those whose
name is the first component of a module the workspace imports. Extra
requires come first, in root lakefile order, and Mathlib last: Lake resolves
shared transitive dependencies from the later require, so Mathlib must win.
Workspaces that import only Mathlib render exactly as before, and a bare
`DependencySpec` still coerces to the new `RootDependencies`, so existing
callers of `renderWorkspace` keep compiling.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
---
 .github/workflows/ci.yml             |   3 +
 LeanEvalGenerator/Contract.lean      |   2 +-
 LeanEvalGenerator/Core/Generate.lean | 152 +++++++++++++++++++--------
 Tests/Dependencies.lean              |  97 +++++++++++++++++
 lakefile.toml                        |   4 +
 5 files changed, 211 insertions(+), 47 deletions(-)
 create mode 100644 Tests/Dependencies.lean

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 7704d8f..77f32a0 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -40,5 +40,8 @@ jobs:
       - name: Check quoted module and declaration paths
         run: lake build test_module_paths && lake env .lake/build/bin/test_module_paths
 
+      - name: Check workspace dependency selection
+        run: lake build test_dependencies && lake env .lake/build/bin/test_dependencies
+
       - name: Check Python test harnesses
         run: python3 -m py_compile tests/scripts/*.py
diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index 0f706dd..288b200 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -199,7 +199,7 @@ def render (request : GenerateRequest) : IO String := do
   for problem in request.problems do
     validateProblem root problem
     let rendered ← LeanEvalGenerator.Core.renderWorkspace root (metadata problem)
-      (problem.resolvedHoles.map extracted) request.leanToolchain mathlib
+      (problem.resolvedHoles.map extracted) request.leanToolchain { mathlib }
       request.templates.workspaceTest
     for (path, content) in rendered do
       files := files.push <| fileJson problem.id path content (← sha256 content)
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index 686e9a8..29892f0 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -42,7 +42,7 @@ def ignoredPathNames : Array String := #[".lake", "build", ".cache", "lake-manif
 def loadWorkspaceTestTemplate (root : System.FilePath) : IO String :=
   IO.FS.readFile (root / "templates" / "WorkspaceTest.lean")
 
-/-! ## Mathlib dependency -/
+/-! ## Root dependencies -/
 
 structure DependencySpec where
   name : String
@@ -64,8 +64,21 @@ private instance : DecodeToml RawRequire where
     let rev? : Option String ← t.decode? `rev
     return { name := name, git := git?, rev := rev? }
 
-def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec := do
-  let path := root / "lakefile.toml"
+/-- The dependencies a generated workspace may require, read from the root
+lakefile: the mandatory `mathlib` pin, plus every other git-pinned `[[require]]`
+in root lakefile order. An extra require is only emitted into a workspace whose
+problem imports one of its modules; see `workspaceRequires`. -/
+structure RootDependencies where
+  mathlib : DependencySpec
+  extras : Array DependencySpec := #[]
+  deriving Inhabited
+
+/-- A bare `mathlib` pin is a complete dependency set with no extras, so
+callers holding only a `DependencySpec` keep working unchanged. -/
+instance : Coe DependencySpec RootDependencies where
+  coe mathlib := { mathlib }
+
+private def loadRootRequires (path : System.FilePath) : IO (Array RawRequire) := do
   let contents ← IO.FS.readFile path
   let inputCtx := mkInputContext contents path.toString
   let table ←
@@ -75,36 +88,52 @@ def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec := do
   let decoded :
       EStateM.Result Unit (Array DecodeError) (Array RawRequire) :=
     (Lake.Toml.Table.decode (α := Array RawRequire) table `require).run #[]
-  let requires ←
-    match decoded with
-    | .ok arr errors =>
-        if errors.isEmpty then pure arr
-        else throw <| IO.userError (decodeErrorsToString errors)
-    | .error _ errors =>
-        throw <| IO.userError (decodeErrorsToString errors)
-  let mathlib := requires.filter fun r => r.name == "mathlib"
+  match decoded with
+  | .ok arr errors =>
+      if errors.isEmpty then pure arr
+      else throw <| IO.userError (decodeErrorsToString errors)
+  | .error _ errors =>
+      throw <| IO.userError (decodeErrorsToString errors)
+
+private def requiredField (path : System.FilePath) (depName field : String)
+    (value? : Option String) : IO String := do
+  match value?.map (·.trim) with
+  | some v =>
+      if v.isEmpty then
+        throw <| IO.userError
+          s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
+      else pure v
+  | none =>
+      throw <| IO.userError
+        s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
+
+/-- Read the root `lakefile.toml`: the single `mathlib` require (which must
+have non-empty `git` and `rev`), and every other require that has a `git`
+field, which must then also pin a non-empty `rev`. Requires without `git`
+(path or Reservoir dependencies) cannot be reproduced in a standalone
+workspace and are ignored. -/
+def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
+  let path := root / "lakefile.toml"
+  let rootRequires ← loadRootRequires path
+  let mathlib := rootRequires.filter fun r => r.name == "mathlib"
   if mathlib.isEmpty then
     throw <| IO.userError s!"Could not find a mathlib dependency in {path}"
   if mathlib.size > 1 then
     throw <| IO.userError s!"Found multiple mathlib dependencies in {path}"
   let entry := mathlib[0]!
-  let git ← match entry.git with
-    | some g =>
-        let g := g.trim
-        if g.isEmpty then
-          throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field"
-        else pure g
-    | none =>
-        throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'git' field"
-  let rev ← match entry.rev with
-    | some r =>
-        let r := r.trim
-        if r.isEmpty then
-          throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field"
-        else pure r
-    | none =>
-        throw <| IO.userError s!"mathlib dependency in {path} is missing a non-empty 'rev' field"
-  return { name := "mathlib", git := git, rev := rev }
+  let git ← requiredField path "mathlib" "git" entry.git
+  let rev ← requiredField path "mathlib" "rev" entry.rev
+  let mut extras : Array DependencySpec := #[]
+  for r in rootRequires do
+    if r.name == "mathlib" then continue
+    let some git := r.git | continue
+    let git ← requiredField path r.name "git" (some git)
+    let rev ← requiredField path r.name "rev" r.rev
+    extras := extras.push { name := r.name, git, rev }
+  return { mathlib := { name := "mathlib", git := git, rev := rev }, extras }
+
+def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec :=
+  return (← loadRootDependencies root).mathlib
 
 /-! ## ExtractedTheorem (subprocess result) -/
 
@@ -1251,6 +1280,15 @@ private partial def collectWorkspaceImports (root : System.FilePath) (moduleName
       unless (← out.get).contains imported do
         out.modify (·.push imported)
 
+/-- The external modules a generated workspace imports, in the order
+`problemImportHeader` emits them. -/
+def problemWorkspaceImports (root : System.FilePath) (moduleName : String) :
+    IO (Array String) := do
+  let visited ← IO.mkRef ({} : Std.HashSet String)
+  let out ← IO.mkRef (#[] : Array String)
+  collectWorkspaceImports root moduleName visited out
+  out.get
+
 /-- The `import` header a generated workspace needs to reproduce the trusted
 module's elaboration context.
 
@@ -1270,12 +1308,26 @@ Known limitation: flattening several repo-local modules into one
 so an inlined module can see a name that only a later one introduced. Avoiding
 that would mean emitting one workspace module per source module. -/
 def problemImportHeader (root : System.FilePath) (moduleName : String) : IO String := do
-  let visited ← IO.mkRef ({} : Std.HashSet String)
-  let out ← IO.mkRef (#[] : Array String)
-  collectWorkspaceImports root moduleName visited out
-  let imports ← out.get
+  let imports ← problemWorkspaceImports root moduleName
   return String.join (imports.toList.map fun m => s!"import {m}\n")
 
+/-- The `[[require]]` entries for a workspace whose modules import `imports`:
+each extra root require whose name is the first component of some import, in
+root lakefile order, followed by `mathlib`. Tooling packages in the root
+lakefile are never selected, because no problem imports them.
+
+Mathlib must come last. When two requires share a transitive dependency
+(batteries, aesop, Qq, ...), Lake resolves it from the later require, so
+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) :
+    Array DependencySpec :=
+  let roots : Std.HashSet String := imports.foldl (init := {}) fun acc m =>
+    match (splitNameComponents m)[0]? with
+    | some r => acc.insert r
+    | none => acc
+  (deps.extras.filter fun d => roots.contains d.name).push deps.mathlib
+
 /-! ## ILean metadata -/
 
 /-- A declaration's source range from the `.ilean`, as
@@ -2892,21 +2944,25 @@ private def renderReadmeLines (entry : EvalProblemMetadata)
       ]
   return lines ++ body
 
-private def lakefileToml (problemId : String) (mathlibDep : DependencySpec)
+/-- Render a workspace `lakefile.toml`. `workspaceDeps` is emitted in the given
+order; see `workspaceRequires` for why Mathlib must be last. -/
+def lakefileToml (problemId : String) (workspaceDeps : Array DependencySpec)
     (withChallengeDeps : Bool) : String :=
   let challengeDepsLib :=
     if withChallengeDeps then
       "[[lean_lib]]\nname = \"ChallengeDeps\"\n\n"
     else ""
+  let requireBlocks := String.join <| workspaceDeps.toList.map fun dep =>
+    "[[require]]\n" ++
+    s!"name = \"{dep.name}\"\n" ++
+    s!"git = \"{dep.git}\"\n" ++
+    s!"rev = \"{dep.rev}\"\n\n"
   s!"name = \"{problemId}\"\n" ++
   "testDriver = \"workspace_test\"\n" ++
   "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
   "[leanOptions]\n" ++
   "autoImplicit = false\n\n" ++
-  "[[require]]\n" ++
-  s!"name = \"{mathlibDep.name}\"\n" ++
-  s!"git = \"{mathlibDep.git}\"\n" ++
-  s!"rev = \"{mathlibDep.rev}\"\n\n" ++
+  requireBlocks ++
   challengeDepsLib ++
   "[[lean_lib]]\nname = \"Challenge\"\n\n" ++
   "[[lean_lib]]\nname = \"Solution\"\n\n" ++
@@ -2917,7 +2973,7 @@ private def lakefileToml (problemId : String) (mathlibDep : DependencySpec)
 
 private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProblemMetadata)
     (extracteds : Array ExtractedTheorem) (toolchain : String)
-    (mathlibDep : DependencySpec) (workspaceTest : String) :
+    (deps : RootDependencies) (workspaceTest : String) :
     IO (Array (String × String)) := do
   let sourcePath := moduleSourcePath root entry.moduleName
   if !(← sourcePath.pathExists) then
@@ -3132,6 +3188,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
     if hasChallengeDeps then removeDuplicatedReducibilityAttributes helperStripped depsHelpers
     else helperStripped
   let moduleImports ← problemImportHeader root entry.moduleName
+  let workspaceDeps := workspaceRequires deps (← problemWorkspaceImports root entry.moduleName)
   let baseImport := if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let challengeBodyStripped := stripProblemMarkers helperStripped localImports
   let challengeBody :=
@@ -3179,7 +3236,8 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
   let mut files : Array (String × String) := #[
     ("README.md", readme),
     ("lean-toolchain", toolchain'),
-    ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)),
+    ("lakefile.toml",
+      lakefileToml entry.id workspaceDeps (withChallengeDeps := hasChallengeDeps)),
     ("Challenge.lean", challenge),
     ("Solution.lean", solutionBody),
     ("Submission.lean", submissionBody),
@@ -3194,7 +3252,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
 /-! ## Single-hole rendering -/
 
 private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProblemMetadata)
-    (extracted : ExtractedTheorem) (toolchain : String) (mathlibDep : DependencySpec)
+    (extracted : ExtractedTheorem) (toolchain : String) (deps : RootDependencies)
     (workspaceTest : String) : IO (Array (String × String)) := do
   let sourcePath := moduleSourcePath root entry.moduleName
   let sourceText ← IO.FS.readFile sourcePath
@@ -3208,6 +3266,7 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
   let challengeDeps? ← renderChallengeDeps root entry extracted localImports
   let hasChallengeDeps := challengeDeps?.isSome
   let moduleImports ← problemImportHeader root entry.moduleName
+  let workspaceDeps := workspaceRequires deps (← problemWorkspaceImports root entry.moduleName)
   let challengeImport :=
     if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let solutionImports :=
@@ -3283,7 +3342,8 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
   let mut files : Array (String × String) := #[
     ("README.md", readme),
     ("lean-toolchain", toolchain'),
-    ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)),
+    ("lakefile.toml",
+      lakefileToml entry.id workspaceDeps (withChallengeDeps := hasChallengeDeps)),
     ("Challenge.lean", challengeFile),
     ("Solution.lean", solutionFile),
     ("Submission.lean", submissionFile),
@@ -3298,15 +3358,15 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
 /-- Render every file in a generated workspace. Mirrors `render_workspace`. -/
 def renderWorkspace (root : System.FilePath) (entry : EvalProblemMetadata)
     (extracteds : Array ExtractedTheorem) (toolchain : String)
-    (mathlibDep : DependencySpec) (workspaceTest : String) :
+    (deps : RootDependencies) (workspaceTest : String) :
     IO (Array (String × String)) := do
   let isMultiHole :=
     extracteds.size != 1 || extracteds[0]!.kind != "theorem"
   let baseFiles ←
     if isMultiHole then
-      renderWorkspaceMultiHole root entry extracteds toolchain mathlibDep workspaceTest
+      renderWorkspaceMultiHole root entry extracteds toolchain deps workspaceTest
     else
-      renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest
+      renderWorkspaceSingleHole root entry extracteds[0]! toolchain deps workspaceTest
   let holesJson ← buildHolesMetadata root entry extracteds
   return baseFiles.push ("holes.json", holesJson)
 
@@ -3512,7 +3572,7 @@ def generate (root : System.FilePath) (selectedProblemId : Option String) (check
         pure problems
   validateHoleShape root selectedProblems
   let toolchain ← IO.FS.readFile (root / "lean-toolchain")
-  let mathlibDep ← loadRootMathlibDependency root
+  let deps ← loadRootDependencies root
   buildExtractor root selectedProblems
   let workspaceTest ← loadWorkspaceTestTemplate root
   let mut mismatches : Array String := #[]
@@ -3521,7 +3581,7 @@ def generate (root : System.FilePath) (selectedProblemId : Option String) (check
     for hole in entry.holes do
       let e ← extractOne root entry hole
       extracteds := extracteds.push e
-    let files ← renderWorkspace root entry extracteds toolchain mathlibDep workspaceTest
+    let files ← renderWorkspace root entry extracteds toolchain deps workspaceTest
     let problemDir := root / "generated" / entry.id
     let relDisplay := s!"generated/{entry.id}"
     if check then
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
new file mode 100644
index 0000000..b074e85
--- /dev/null
+++ b/Tests/Dependencies.lean
@@ -0,0 +1,97 @@
+import LeanEvalGenerator.Core.Generate
+
+open LeanEvalGenerator.Core
+
+private def expectEq (label actual expected : String) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError
+      s!"{label} mismatch\nexpected:\n{repr expected}\nactual:\n{repr actual}"
+
+private def mathlibRev := "d13f23b723b8a846827a245b89c10fc7d3f11612"
+private def tauCetiRev := "7cfdfef3ac31cce91302b926ac2f49525eed6fbc"
+
+private def rootLakefile : String :=
+  "name = \"fixture\"\n\n" ++
+  "[[require]]\nname = \"mathlib\"\n" ++
+  "git = \"https://github.com/leanprover-community/mathlib4.git\"\n" ++
+  s!"rev = \"{mathlibRev}\"\n\n" ++
+  "[[require]]\nname = \"TauCeti\"\n" ++
+  "git = \"https://github.com/TauCetiProject/TauCeti\"\n" ++
+  s!"rev = \"{tauCetiRev}\"\n\n" ++
+  "[[require]]\nname = \"Cli\"\n" ++
+  "git = \"https://github.com/leanprover/lean4-cli\"\n" ++
+  "rev = \"e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204\"\n\n" ++
+  "[[require]]\nname = \"LocalTool\"\npath = \"tools/local\"\n"
+
+private def requireBlock (name git rev : String) : String :=
+  s!"[[require]]\nname = \"{name}\"\ngit = \"{git}\"\nrev = \"{rev}\"\n\n"
+
+private def mathlibBlock : String :=
+  requireBlock "mathlib" "https://github.com/leanprover-community/mathlib4.git" mathlibRev
+
+/-- The lakefile every Mathlib-only workspace had before extra requires
+existed, spelled out literally so any drift in its bytes is caught. -/
+private def mathlibOnlyLakefile (problemId : String) : String :=
+  s!"name = \"{problemId}\"\n" ++
+  "testDriver = \"workspace_test\"\n" ++
+  "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
+  "[leanOptions]\nautoImplicit = false\n\n" ++
+  mathlibBlock ++
+  "[[lean_lib]]\nname = \"Challenge\"\n\n" ++
+  "[[lean_lib]]\nname = \"Solution\"\n\n" ++
+  "[[lean_lib]]\nname = \"Submission\"\n\n" ++
+  "[[lean_exe]]\nname = \"workspace_test\"\nroot = \"WorkspaceTest\"\n"
+
+private def writeModule (root : System.FilePath) (moduleName source : String) : IO Unit := do
+  let path := moduleSourcePath root moduleName
+  if let some dir := path.parent then IO.FS.createDirAll dir
+  IO.FS.writeFile path source
+
+private def requiresFor (root : System.FilePath) (deps : RootDependencies)
+    (moduleName : String) : IO (Array DependencySpec) :=
+  return workspaceRequires deps (← problemWorkspaceImports root moduleName)
+
+private def names (specs : Array DependencySpec) : String :=
+  toString (specs.map (·.name))
+
+def main : IO Unit := do
+  let root ← IO.FS.createTempDir
+  try
+    IO.FS.writeFile (root / "lakefile.toml") rootLakefile
+    -- The TauCeti import is reached only through a repo-local helper module.
+    writeModule root "LeanEval.Cfsg"
+      "import Mathlib.GroupTheory.Perm.Basic\nimport LeanEval.CfsgHelper\n"
+    writeModule root "LeanEval.CfsgHelper"
+      "import TauCeti.GroupTheory.SpecificGroups.CFSG.Classification\n"
+    writeModule root "LeanEval.Plain" "import Mathlib.Data.Nat.Basic\n"
+
+    let deps ← loadRootDependencies root
+    expectEq "mathlib pin" deps.mathlib.rev mathlibRev
+    expectEq "extra requires" (names deps.extras) "#[TauCeti, Cli]"
+    expectEq "legacy loader" (← loadRootMathlibDependency root).rev mathlibRev
+
+    let cfsg ← requiresFor root deps "LeanEval.Cfsg"
+    expectEq "imported extra require precedes mathlib; Cli is not required"
+      (names cfsg) "#[TauCeti, mathlib]"
+    let cfsgLakefile := lakefileToml "cfsg" cfsg (withChallengeDeps := false)
+    unless (cfsgLakefile.splitOn
+        (requireBlock "TauCeti" "https://github.com/TauCetiProject/TauCeti" tauCetiRev ++
+          mathlibBlock)).length == 2 do
+      throw <| IO.userError
+        s!"TauCeti require is not immediately before mathlib:\n{cfsgLakefile}"
+    if (cfsgLakefile.splitOn "Cli").length > 1 then
+      throw <| IO.userError s!"unimported Cli require was emitted:\n{cfsgLakefile}"
+
+    let plain ← requiresFor root deps "LeanEval.Plain"
+    expectEq "mathlib-only requires" (names plain) "#[mathlib]"
+    expectEq "mathlib-only lakefile"
+      (lakefileToml "plain" plain (withChallengeDeps := false))
+      (mathlibOnlyLakefile "plain")
+    -- A bare mathlib pin (the pre-existing API) coerces to the same result.
+    expectEq "coerced mathlib pin"
+      (lakefileToml "plain" (workspaceRequires deps.mathlib #["TauCeti.X"])
+        (withChallengeDeps := false))
+      (mathlibOnlyLakefile "plain")
+  finally
+    IO.FS.removeDirAll root
+  IO.println "dependency tests passed"
diff --git a/lakefile.toml b/lakefile.toml
index 6fea374..ce074cb 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,3 +14,7 @@ root = "LeanEvalGenerator.Main"
 [[lean_exe]]
 name = "test_module_paths"
 root = "Tests.ModulePaths"
+
+[[lean_exe]]
+name = "test_dependencies"
+root = "Tests.Dependencies"

From d37dc44c0489a8dbc589add581a9f36f9dd5a5b0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 25 Sep 2026 14:04:15 +0000
Subject: [PATCH 2/3] feat: validate selected requires lazily and accept extras
 over the CLI

The JSON request gains an optional `dependencies` array of extra git pins,
so the CLI path can render workspaces for problems that import packages
other than Mathlib; omitting it keeps every existing version 1 request's
meaning and output. Root requires other than mathlib are now only checked
when a problem selects them, so tooling requires may use any Lake syntax,
and a selected require using fields a workspace would not reproduce
(`subDir`, `scope`, table-valued `git`, ...) is a clear error rather than
being silently dropped. Require values are TOML-escaped, which leaves
ordinary names, URLs and revisions unchanged. The README documents the
selection rule and its limitation for packages whose library root differs
from their package name.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
---
 LeanEvalGenerator/Contract.lean      |  36 +++++-
 LeanEvalGenerator/Core/Generate.lean | 164 +++++++++++++++++++--------
 README.md                            |  22 ++++
 Tests/Dependencies.lean              |  48 +++++++-
 schemas/request-v1.schema.json       |  14 +++
 tests/scripts/contract.py            |  60 ++++++++++
 6 files changed, 282 insertions(+), 62 deletions(-)

diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index 288b200..d0ddd21 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -57,6 +57,12 @@ structure GenerateRequest where
   contextRoot : String
   leanToolchain : String
   mathlib : DependencyPin
+  /-- Optional non-mathlib git requires, in the order a workspace should
+  require them. Each is emitted, before Mathlib, into the workspace of every
+  problem that imports one of its modules (the rule is
+  `LeanEvalGenerator.Core.workspaceRequires`). Omitting the field means no
+  extra requires, which is how every earlier version 1 request behaves. -/
+  dependencies : Option (Array DependencyPin) := none
   templates : TemplateInputs
   problems : Array ProblemInput
   deriving FromJson
@@ -75,6 +81,18 @@ private def validateRequest (request : GenerateRequest) : IO Unit := do
     throw <| IO.userError "The dependency pin must be named `mathlib`."
   if request.mathlib.git.isEmpty || request.mathlib.rev.isEmpty then
     throw <| IO.userError "The mathlib git and rev pins must be non-empty."
+  let mut dependencyNames : Array String := #[]
+  for dep in request.dependencies.getD #[] do
+    if dep.name.isEmpty then
+      throw <| IO.userError "Dependency names must be non-empty."
+    if dep.name == "mathlib" then
+      throw <| IO.userError
+        "`dependencies` must not contain `mathlib`; it is pinned by the `mathlib` field."
+    if dependencyNames.contains dep.name then
+      throw <| IO.userError s!"Duplicate dependency `{dep.name}`."
+    if dep.git.isEmpty || dep.rev.isEmpty then
+      throw <| IO.userError s!"Dependency `{dep.name}` git and rev pins must be non-empty."
+    dependencyNames := dependencyNames.push dep.name
   let mut problemIds : Array String := #[]
   for problem in request.problems do
     if problemIds.contains problem.id then
@@ -190,16 +208,18 @@ ordered and byte-stable, including complete file contents and SHA-256 digests. -
 def render (request : GenerateRequest) : IO String := do
   validateRequest request
   let root : System.FilePath := request.contextRoot
-  let mathlib : LeanEvalGenerator.Core.DependencySpec := {
-    name := request.mathlib.name
-    git := request.mathlib.git
-    rev := request.mathlib.rev
+  let spec (pin : DependencyPin) : LeanEvalGenerator.Core.DependencySpec :=
+    { name := pin.name, git := pin.git, rev := pin.rev }
+  let deps : LeanEvalGenerator.Core.RootDependencies := {
+    mathlib := spec request.mathlib
+    extras := (request.dependencies.getD #[]).map
+      (LeanEvalGenerator.Core.RootRequire.ofSpec ∘ spec)
   }
   let mut files : Array LeanEvalGenerator.Core.OJson := #[]
   for problem in request.problems do
     validateProblem root problem
     let rendered ← LeanEvalGenerator.Core.renderWorkspace root (metadata problem)
-      (problem.resolvedHoles.map extracted) request.leanToolchain { mathlib }
+      (problem.resolvedHoles.map extracted) request.leanToolchain deps
       request.templates.workspaceTest
     for (path, content) in rendered do
       files := files.push <| fileJson problem.id path content (← sha256 content)
@@ -217,10 +237,14 @@ private def ensureKnownFields (label : String) (allowed : Array String)
 
 private def validateJsonShape (value : Json) : Except String Unit := do
   ensureKnownFields "request" #[
-    "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "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
   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 29892f0..d7dee0a 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -50,27 +50,62 @@ structure DependencySpec where
   rev : String
   deriving Inhabited
 
-private structure RawRequire where
+/-- A `[[require]]` from the root lakefile, kept as read. Non-mathlib requires
+are only validated when some problem selects them (see `workspaceRequires`), so
+tooling requires the generator never emits may use any Lake require syntax. -/
+structure RootRequire where
   name : String
   git : Option String := none
   rev : Option String := none
+  /-- Fields present in the root require that a generated `[[require]]` would
+  not reproduce, such as `subDir`, `scope`, `version`, `path`, `options`, or a
+  table-valued `git`. -/
+  unsupportedFields : Array String := #[]
   deriving Inhabited
 
-private instance : DecodeToml RawRequire where
-  decode v := do
-    let t ← v.decodeTable
-    let name : String ← t.decode `name
-    let git? : Option String ← t.decode? `git
-    let rev? : Option String ← t.decode? `rev
-    return { name := name, git := git?, rev := rev? }
+def RootRequire.ofSpec (spec : DependencySpec) : RootRequire :=
+  { name := spec.name, git := some spec.git, rev := some spec.rev }
+
+private def nonEmptyTrimmed? (value? : Option String) : Option String :=
+  value?.bind fun v => let v := v.trim; if v.isEmpty then none else some v
+
+/-- The `[[require]]` to emit for a selected root require, or an explanation of
+why a standalone workspace cannot reproduce it. -/
+def RootRequire.toSpec (r : RootRequire) : Except String DependencySpec := do
+  unless r.unsupportedFields.isEmpty do
+    throw s!"root require '{r.name}' uses fields a generated workspace does not \
+      reproduce: {", ".intercalate r.unsupportedFields.toList}. Only `name`, `git` \
+      and `rev` are supported."
+  let some git := nonEmptyTrimmed? r.git
+    | throw s!"root require '{r.name}' is not a git require with a non-empty `git` URL"
+  let some rev := nonEmptyTrimmed? r.rev
+    | throw s!"root require '{r.name}' does not pin a non-empty `rev`"
+  return { name := r.name, git, rev }
+
+private def rootRequireOfTable (t : Table) : Except String RootRequire := do
+  let name ← match t.find? `name with
+    | some (.string _ n) => pure n
+    | _ => throw "a [[require]] entry is missing a string `name` field"
+  let mut git : Option String := none
+  let mut rev : Option String := none
+  let mut unsupported : Array String := #[]
+  for (key, value) in t.items do
+    match key.toString, value with
+    | "name", _ => pure ()
+    | "git", .string _ g => git := some g
+    | "git", _ => unsupported := unsupported.push "table-valued `git`"
+    | "rev", .string _ r => rev := some r
+    | "rev", _ => unsupported := unsupported.push "non-string `rev`"
+    | other, _ => unsupported := unsupported.push s!"`{other}`"
+  return { name, git, rev, unsupportedFields := unsupported }
 
 /-- The dependencies a generated workspace may require, read from the root
-lakefile: the mandatory `mathlib` pin, plus every other git-pinned `[[require]]`
-in root lakefile order. An extra require is only emitted into a workspace whose
+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`. -/
 structure RootDependencies where
   mathlib : DependencySpec
-  extras : Array DependencySpec := #[]
+  extras : Array RootRequire := #[]
   deriving Inhabited
 
 /-- A bare `mathlib` pin is a complete dependency set with no extras, so
@@ -78,7 +113,7 @@ callers holding only a `DependencySpec` keep working unchanged. -/
 instance : Coe DependencySpec RootDependencies where
   coe mathlib := { mathlib }
 
-private def loadRootRequires (path : System.FilePath) : IO (Array RawRequire) := do
+private def loadRootRequires (path : System.FilePath) : IO (Array RootRequire) := do
   let contents ← IO.FS.readFile path
   let inputCtx := mkInputContext contents path.toString
   let table ←
@@ -86,32 +121,30 @@ private def loadRootRequires (path : System.FilePath) : IO (Array RawRequire) :=
     | .ok table => pure table
     | .error err => throw <| IO.userError (← Lake.mkMessageLogString err)
   let decoded :
-      EStateM.Result Unit (Array DecodeError) (Array RawRequire) :=
-    (Lake.Toml.Table.decode (α := Array RawRequire) table `require).run #[]
-  match decoded with
-  | .ok arr errors =>
-      if errors.isEmpty then pure arr
-      else throw <| IO.userError (decodeErrorsToString errors)
-  | .error _ errors =>
-      throw <| IO.userError (decodeErrorsToString errors)
+      EStateM.Result Unit (Array DecodeError) (Array Table) :=
+    (Lake.Toml.Table.decode (α := Array Table) table `require).run #[]
+  let tables ← match decoded with
+    | .ok arr errors =>
+        if errors.isEmpty then pure arr
+        else throw <| IO.userError (decodeErrorsToString errors)
+    | .error _ errors =>
+        throw <| IO.userError (decodeErrorsToString errors)
+  tables.mapM fun t => match rootRequireOfTable t with
+    | .ok r => pure r
+    | .error e => throw <| IO.userError s!"{path}: {e}"
 
 private def requiredField (path : System.FilePath) (depName field : String)
     (value? : Option String) : IO String := do
-  match value?.map (·.trim) with
-  | some v =>
-      if v.isEmpty then
-        throw <| IO.userError
-          s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
-      else pure v
+  match nonEmptyTrimmed? value? with
+  | some v => pure v
   | none =>
       throw <| IO.userError
         s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
 
-/-- Read the root `lakefile.toml`: the single `mathlib` require (which must
-have non-empty `git` and `rev`), and every other require that has a `git`
-field, which must then also pin a non-empty `rev`. Requires without `git`
-(path or Reservoir dependencies) cannot be reproduced in a standalone
-workspace and are ignored. -/
+/-- Read the root `lakefile.toml`: the single `mathlib` require, which must
+have non-empty `git` and `rev`, 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 := do
   let path := root / "lakefile.toml"
   let rootRequires ← loadRootRequires path
@@ -123,14 +156,10 @@ def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
   let entry := mathlib[0]!
   let git ← requiredField path "mathlib" "git" entry.git
   let rev ← requiredField path "mathlib" "rev" entry.rev
-  let mut extras : Array DependencySpec := #[]
-  for r in rootRequires do
-    if r.name == "mathlib" then continue
-    let some git := r.git | continue
-    let git ← requiredField path r.name "git" (some git)
-    let rev ← requiredField path r.name "rev" r.rev
-    extras := extras.push { name := r.name, git, rev }
-  return { mathlib := { name := "mathlib", git := git, rev := rev }, extras }
+  return {
+    mathlib := { name := "mathlib", git := git, rev := rev }
+    extras := rootRequires.filter (·.name != "mathlib")
+  }
 
 def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec :=
   return (← loadRootDependencies root).mathlib
@@ -1311,22 +1340,38 @@ def problemImportHeader (root : System.FilePath) (moduleName : String) : IO Stri
   let imports ← problemWorkspaceImports root moduleName
   return String.join (imports.toList.map fun m => s!"import {m}\n")
 
-/-- The `[[require]]` entries for a workspace whose modules import `imports`:
-each extra root require whose name is the first component of some import, in
-root lakefile order, followed by `mathlib`. Tooling packages in the root
-lakefile are never selected, because no problem imports them.
+/-- The `[[require]]` entries for a workspace whose modules import `imports`
+(as returned by `problemWorkspaceImports`, so repo-local imports have already
+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.
+
+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.
 
 Mathlib must come last. When two requires share a transitive dependency
 (batteries, aesop, Qq, ...), Lake resolves it from the later require, so
 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) :
-    Array DependencySpec :=
+    Except String (Array DependencySpec) := do
   let roots : Std.HashSet String := imports.foldl (init := {}) fun acc m =>
     match (splitNameComponents m)[0]? with
     | some r => acc.insert r
     | none => acc
-  (deps.extras.filter fun d => roots.contains d.name).push deps.mathlib
+  let selected ← (deps.extras.filter fun r => roots.contains r.name).mapM (·.toSpec)
+  return selected.push deps.mathlib
+
+/-- `workspaceRequires` for the workspace generated from `moduleName`. -/
+def problemWorkspaceRequires (root : System.FilePath) (deps : RootDependencies)
+    (problemId moduleName : String) : IO (Array DependencySpec) := do
+  match workspaceRequires deps (← problemWorkspaceImports root moduleName) with
+  | .ok specs => pure specs
+  | .error e => throw <| IO.userError s!"Problem '{problemId}': {e}"
 
 /-! ## ILean metadata -/
 
@@ -2944,6 +2989,25 @@ private def renderReadmeLines (entry : EvalProblemMetadata)
       ]
   return lines ++ body
 
+/-- A TOML basic string literal for `s`: backslash, double quote and control
+characters are escaped; anything else (in particular every ordinary package
+name, URL and revision) is emitted verbatim between double quotes. -/
+def tomlBasicString (s : String) : String := Id.run do
+  let mut out := "\""
+  for c in s.toList do
+    out := match c with
+      | '\\' => out ++ "\\\\"
+      | '"' => out ++ "\\\""
+      | '\n' => out ++ "\\n"
+      | '\t' => out ++ "\\t"
+      | '\r' => out ++ "\\r"
+      | c =>
+          if c.toNat < 0x20 || c.toNat == 0x7f then
+            let hex := String.mk (Nat.toDigits 16 c.toNat)
+            out ++ "\\u" ++ String.mk (List.replicate (4 - hex.length) '0') ++ hex
+          else out.push c
+  return out.push '"'
+
 /-- Render a workspace `lakefile.toml`. `workspaceDeps` is emitted in the given
 order; see `workspaceRequires` for why Mathlib must be last. -/
 def lakefileToml (problemId : String) (workspaceDeps : Array DependencySpec)
@@ -2954,9 +3018,9 @@ def lakefileToml (problemId : String) (workspaceDeps : Array DependencySpec)
     else ""
   let requireBlocks := String.join <| workspaceDeps.toList.map fun dep =>
     "[[require]]\n" ++
-    s!"name = \"{dep.name}\"\n" ++
-    s!"git = \"{dep.git}\"\n" ++
-    s!"rev = \"{dep.rev}\"\n\n"
+    s!"name = {tomlBasicString dep.name}\n" ++
+    s!"git = {tomlBasicString dep.git}\n" ++
+    s!"rev = {tomlBasicString dep.rev}\n\n"
   s!"name = \"{problemId}\"\n" ++
   "testDriver = \"workspace_test\"\n" ++
   "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
@@ -3188,7 +3252,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl
     if hasChallengeDeps then removeDuplicatedReducibilityAttributes helperStripped depsHelpers
     else helperStripped
   let moduleImports ← problemImportHeader root entry.moduleName
-  let workspaceDeps := workspaceRequires deps (← problemWorkspaceImports root entry.moduleName)
+  let workspaceDeps ← problemWorkspaceRequires root deps entry.id entry.moduleName
   let baseImport := if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let challengeBodyStripped := stripProblemMarkers helperStripped localImports
   let challengeBody :=
@@ -3266,7 +3330,7 @@ private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProb
   let challengeDeps? ← renderChallengeDeps root entry extracted localImports
   let hasChallengeDeps := challengeDeps?.isSome
   let moduleImports ← problemImportHeader root entry.moduleName
-  let workspaceDeps := workspaceRequires deps (← problemWorkspaceImports root entry.moduleName)
+  let workspaceDeps ← problemWorkspaceRequires root deps entry.id entry.moduleName
   let challengeImport :=
     if hasChallengeDeps then "import ChallengeDeps\n\n" else moduleImports ++ "\n"
   let solutionImports :=
diff --git a/README.md b/README.md
index 70103ab..3a00922 100644
--- a/README.md
+++ b/README.md
@@ -27,3 +27,25 @@ The consumer owns hole resolution. A consumer resolves declarations under its
 pinned target environment, then passes the resulting ranges and dependency
 data to this renderer. Consumer-specific fixtures and source trees do not
 belong in this foundation package.
+
+## Workspace dependencies
+
+Every generated `lakefile.toml` requires Mathlib at the pinned revision. A
+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`
+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
+imports them. Selected packages are emitted in root order before Mathlib,
+which stays last so that Lake resolves shared transitive dependencies from
+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
+rather than silently changing the statement.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
index b074e85..8b9bcf6 100644
--- a/Tests/Dependencies.lean
+++ b/Tests/Dependencies.lean
@@ -18,10 +18,16 @@ private def rootLakefile : String :=
   "[[require]]\nname = \"TauCeti\"\n" ++
   "git = \"https://github.com/TauCetiProject/TauCeti\"\n" ++
   s!"rev = \"{tauCetiRev}\"\n\n" ++
+  -- Tooling requires that no problem imports may use any Lake syntax: none of
+  -- these is validated unless a problem selects it.
   "[[require]]\nname = \"Cli\"\n" ++
-  "git = \"https://github.com/leanprover/lean4-cli\"\n" ++
-  "rev = \"e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204\"\n\n" ++
-  "[[require]]\nname = \"LocalTool\"\npath = \"tools/local\"\n"
+  "git = \"https://github.com/leanprover/lean4-cli\"\n\n" ++
+  "[[require]]\nname = \"LocalTool\"\npath = \"tools/local\"\n\n" ++
+  "[[require]]\nname = \"Reservoir\"\nscope = \"someone\"\nversion = \"1.0\"\n\n" ++
+  "[[require]]\nname = \"SubDirPkg\"\ngit = \"https://example.com/x\"\n" ++
+  "rev = \"abc\"\nsubDir = \"pkg\"\n\n" ++
+  "[[require]]\nname = \"TableGit\"\ngit = { url = \"https://example.com/y\" }\n" ++
+  "rev = \"abc\"\n"
 
 private def requireBlock (name git rev : String) : String :=
   s!"[[require]]\nname = \"{name}\"\ngit = \"{git}\"\nrev = \"{rev}\"\n\n"
@@ -49,7 +55,19 @@ private def writeModule (root : System.FilePath) (moduleName source : String) :
 
 private def requiresFor (root : System.FilePath) (deps : RootDependencies)
     (moduleName : String) : IO (Array DependencySpec) :=
-  return workspaceRequires deps (← problemWorkspaceImports root moduleName)
+  problemWorkspaceRequires root deps moduleName moduleName
+
+/-- Selecting the require that `import {package}.X` pulls in must fail with a
+message containing `expected`. -/
+private def expectSelectionError (deps : RootDependencies) (package expected : String) :
+    IO Unit := do
+  match workspaceRequires deps #[s!"{package}.X", "Mathlib.Logic.Basic"] with
+  | .ok specs =>
+      throw <| IO.userError
+        s!"selecting {package} should fail, but gave {specs.map (·.name)}"
+  | .error e =>
+      unless (e.splitOn expected).length > 1 do
+        throw <| IO.userError s!"selecting {package}: error {e.quote} lacks {expected.quote}"
 
 private def names (specs : Array DependencySpec) : String :=
   toString (specs.map (·.name))
@@ -67,9 +85,17 @@ def main : IO Unit := do
 
     let deps ← loadRootDependencies root
     expectEq "mathlib pin" deps.mathlib.rev mathlibRev
-    expectEq "extra requires" (names deps.extras) "#[TauCeti, Cli]"
+    expectEq "extra requires" (toString (deps.extras.map (·.name)))
+      "#[TauCeti, Cli, LocalTool, Reservoir, SubDirPkg, TableGit]"
     expectEq "legacy loader" (← loadRootMathlibDependency root).rev mathlibRev
 
+    -- Unreproducible requires only fail once a problem selects them.
+    expectSelectionError deps "Cli" "does not pin a non-empty `rev`"
+    expectSelectionError deps "LocalTool" "`path`"
+    expectSelectionError deps "Reservoir" "`scope`, `version`"
+    expectSelectionError deps "SubDirPkg" "`subDir`"
+    expectSelectionError deps "TableGit" "table-valued `git`"
+
     let cfsg ← requiresFor root deps "LeanEval.Cfsg"
     expectEq "imported extra require precedes mathlib; Cli is not required"
       (names cfsg) "#[TauCeti, mathlib]"
@@ -89,9 +115,19 @@ def main : IO Unit := do
       (mathlibOnlyLakefile "plain")
     -- A bare mathlib pin (the pre-existing API) coerces to the same result.
     expectEq "coerced mathlib pin"
-      (lakefileToml "plain" (workspaceRequires deps.mathlib #["TauCeti.X"])
+      (lakefileToml "plain" (← IO.ofExcept (workspaceRequires deps.mathlib #["TauCeti.X"]))
         (withChallengeDeps := false))
       (mathlibOnlyLakefile "plain")
+
+    -- 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\""
+    expectEq "escaped TOML string" (tomlBasicString "a\"b\\c\nd\x01")
+      "\"a\\\"b\\\\c\\nd\\u0001\""
+    let odd : DependencySpec := { name := "Odd", git := "https://x.org/\"q\"", rev := "r\\1" }
+    unless ((lakefileToml "odd" #[odd] (withChallengeDeps := false)).splitOn
+        "git = \"https://x.org/\\\"q\\\"\"\nrev = \"r\\\\1\"\n").length == 2 do
+      throw <| IO.userError "lakefile require values are not TOML-escaped"
   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 10fee8b..3cfe7aa 100644
--- a/schemas/request-v1.schema.json
+++ b/schemas/request-v1.schema.json
@@ -17,6 +17,10 @@
     "contextRoot": { "type": "string", "minLength": 1 },
     "leanToolchain": { "type": "string", "minLength": 1 },
     "mathlib": { "$ref": "#/$defs/dependency" },
+    "dependencies": {
+      "type": "array",
+      "items": { "$ref": "#/$defs/extraDependency" }
+    },
     "templates": {
       "type": "object",
       "additionalProperties": false,
@@ -40,6 +44,16 @@
         "rev": { "type": "string", "minLength": 1 }
       }
     },
+    "extraDependency": {
+      "type": "object",
+      "additionalProperties": false,
+      "required": ["name", "git", "rev"],
+      "properties": {
+        "name": { "type": "string", "minLength": 1, "not": { "const": "mathlib" } },
+        "git": { "type": "string", "minLength": 1 },
+        "rev": { "type": "string", "minLength": 1 }
+      }
+    },
     "resolvedHole": {
       "type": "object",
       "additionalProperties": false,
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index f10ee9e..6c9b860 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -69,6 +69,54 @@ def assert_rejected(payload: dict[str, object], message: str) -> None:
     assert message in result.stderr, result.stderr
 
 
+def lakefile_for(payload: dict[str, object]) -> str:
+    result = invoke(json.dumps(payload))
+    assert result.returncode == 0, result.stderr
+    files = json.loads(result.stdout)["files"]
+    [lakefile] = [item["content"] for item in files if item["path"] == "lakefile.toml"]
+    return lakefile
+
+
+def check_extra_dependencies() -> None:
+    """Render a problem importing a non-Mathlib package through the CLI."""
+    mathlib = '[[require]]\nname = "mathlib"\ngit = "x"\nrev = "y"\n\n'
+    tauceti = '[[require]]\nname = "TauCeti"\ngit = "https://t.example"\nrev = "abc"\n\n'
+    dependencies = [
+        {"name": "TauCeti", "git": "https://t.example", "rev": "abc"},
+        {"name": "Cli", "git": "https://c.example", "rev": "def"},
+    ]
+    with tempfile.TemporaryDirectory() as directory:
+        context = Path(directory)
+        ilean = context / ".lake/build/lib/lean"
+        ilean.mkdir(parents=True)
+        for module, header in [
+            ("WithTauCeti", "import TauCeti.GroupTheory.Classification\n\n"),
+            ("MathlibOnly", "import Mathlib.Logic.Basic\n\n"),
+        ]:
+            content = header + "theorem fixture : True := by sorry\n"
+            (context / f"{module}.lean").write_text(content, encoding="utf-8")
+            (ilean / f"{module}.ilean").write_text('{"decls": {}}', encoding="utf-8")
+            fixture = problem()
+            fixture["moduleName"] = module
+            fixture["moduleContent"] = content
+            hole = fixture["resolvedHoles"][0]
+            hole["module"] = module
+            hole["declarationName"] = "fixture"
+            hole["startLine"] = hole["endLine"] = 3
+            payload = request_with(fixture)
+            payload["contextRoot"] = str(context)
+            baseline = lakefile_for(payload)
+            payload["dependencies"] = dependencies
+            lakefile = lakefile_for(payload)
+            assert "Cli" not in lakefile, lakefile
+            if module == "WithTauCeti":
+                assert baseline.count("[[require]]") == 1, baseline
+                assert tauceti + mathlib in lakefile, lakefile
+                assert lakefile.count("[[require]]") == 2, lakefile
+            else:
+                assert lakefile == baseline, lakefile
+
+
 def main() -> int:
     subprocess.run(["lake", "build"], cwd=ROOT, check=True)
     subprocess.run(
@@ -152,6 +200,18 @@ def main() -> int:
         assert str(expected_ilean) in result.stderr, result.stderr
         assert "Arxiv/«0912/2382»" not in result.stderr
 
+    extra_named_mathlib = request_with(problem())
+    extra_named_mathlib["dependencies"] = [{"name": "mathlib", "git": "x", "rev": "y"}]
+    assert_rejected(extra_named_mathlib, "must not contain `mathlib`")
+
+    dependency_unknown = request_with(problem())
+    dependency_unknown["dependencies"] = [
+        {"name": "TauCeti", "git": "x", "rev": "y", "subDir": "z"}
+    ]
+    assert_rejected(dependency_unknown, "dependency contains an unknown field")
+
+    check_extra_dependencies()
+
     print("PASS schema errors stay off stdout and quoted source/ilean paths resolve")
     return 0
 

From bd4a83795655a1056a42f1647c783328dd6a8c3c Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 25 Sep 2026 14:41:36 +0000
Subject: [PATCH 3/3] fix: reject unreproducible mathlib requires and invalid
 problem ids

Generation now refuses a root mathlib require carrying fields such as
`subDir` or `scope`, which the emitted `[[require]]` would silently drop,
just as it does for a selected extra require; `loadRootMathlibDependency`
keeps ignoring them as before. CLI requests must use the same problem id
rule as manifests, and the workspace name is emitted as an escaped TOML
string. The README tells consumers to install the root lake-manifest.json
into a generated workspace, so the pruned requires resolve to the same
package revisions as the root workspace.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
---
 LeanEvalGenerator/Contract.lean      |  6 ++++--
 LeanEvalGenerator/Core/Generate.lean | 26 +++++++++++++++++++-------
 LeanEvalGenerator/Core/Manifest.lean |  2 +-
 README.md                            |  6 ++++++
 Tests/Dependencies.lean              | 19 +++++++++++++++++++
 schemas/request-v1.schema.json       |  2 +-
 tests/scripts/contract.py            |  5 +++++
 7 files changed, 55 insertions(+), 11 deletions(-)

diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean
index d0ddd21..34d8e57 100644
--- a/LeanEvalGenerator/Contract.lean
+++ b/LeanEvalGenerator/Contract.lean
@@ -141,8 +141,10 @@ private def extracted (hole : ResolvedHole) : LeanEvalGenerator.Core.ExtractedTh
 }
 
 private def validateProblem (root : System.FilePath) (problem : ProblemInput) : IO Unit := do
-  if problem.id.isEmpty then
-    throw <| IO.userError "Problem id must be non-empty."
+  unless LeanEvalGenerator.Core.isValidProblemId problem.id do
+    throw <| IO.userError
+      s!"Problem id {problem.id.quote} is invalid. Use only letters, digits, '_' or '-', \
+        starting with a letter or digit."
   if problem.title.isEmpty then
     throw <| IO.userError s!"Problem `{problem.id}` title must be non-empty."
   if problem.moduleName.isEmpty then
diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean
index d7dee0a..9013df1 100644
--- a/LeanEvalGenerator/Core/Generate.lean
+++ b/LeanEvalGenerator/Core/Generate.lean
@@ -141,11 +141,8 @@ private def requiredField (path : System.FilePath) (depName field : String)
       throw <| IO.userError
         s!"{depName} dependency in {path} is missing a non-empty '{field}' field"
 
-/-- Read the root `lakefile.toml`: the single `mathlib` require, which must
-have non-empty `git` and `rev`, 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 := do
+private def loadRootDependenciesCore (root : System.FilePath) (strictMathlib : Bool) :
+    IO RootDependencies := do
   let path := root / "lakefile.toml"
   let rootRequires ← loadRootRequires path
   let mathlib := rootRequires.filter fun r => r.name == "mathlib"
@@ -154,6 +151,11 @@ def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
   if mathlib.size > 1 then
     throw <| IO.userError s!"Found multiple mathlib dependencies in {path}"
   let entry := mathlib[0]!
+  if strictMathlib && !entry.unsupportedFields.isEmpty then
+    throw <| IO.userError
+      s!"mathlib dependency in {path} uses fields a generated workspace does not \
+        reproduce: {", ".intercalate entry.unsupportedFields.toList}. Only `name`, \
+        `git` and `rev` are supported."
   let git ← requiredField path "mathlib" "git" entry.git
   let rev ← requiredField path "mathlib" "rev" entry.rev
   return {
@@ -161,8 +163,18 @@ def loadRootDependencies (root : System.FilePath) : IO RootDependencies := do
     extras := rootRequires.filter (·.name != "mathlib")
   }
 
+/-- 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)
+
+/-- The root `mathlib` pin. Unlike `loadRootDependencies`, this ignores
+fields beyond `name`, `git` and `rev`, as it always has. -/
 def loadRootMathlibDependency (root : System.FilePath) : IO DependencySpec :=
-  return (← loadRootDependencies root).mathlib
+  return (← loadRootDependenciesCore root (strictMathlib := false)).mathlib
 
 /-! ## ExtractedTheorem (subprocess result) -/
 
@@ -3021,7 +3033,7 @@ def lakefileToml (problemId : String) (workspaceDeps : Array DependencySpec)
     s!"name = {tomlBasicString dep.name}\n" ++
     s!"git = {tomlBasicString dep.git}\n" ++
     s!"rev = {tomlBasicString dep.rev}\n\n"
-  s!"name = \"{problemId}\"\n" ++
+  s!"name = {tomlBasicString problemId}\n" ++
   "testDriver = \"workspace_test\"\n" ++
   "defaultTargets = [\"Challenge\", \"Solution\", \"Submission\"]\n\n" ++
   "[leanOptions]\n" ++
diff --git a/LeanEvalGenerator/Core/Manifest.lean b/LeanEvalGenerator/Core/Manifest.lean
index 3690afc..9e412b8 100644
--- a/LeanEvalGenerator/Core/Manifest.lean
+++ b/LeanEvalGenerator/Core/Manifest.lean
@@ -17,7 +17,7 @@ private def isAsciiAlnum (c : Char) : Bool :=
   c.isAlpha || c.isDigit
 
 /-- Mirrors the Python `ID_PATTERN = re.compile(r"^[A-Za-z0-9][A-Za-z0-9_-]*$")`. -/
-private def isValidProblemId (s : String) : Bool :=
+def isValidProblemId (s : String) : Bool :=
   !s.isEmpty
     && isAsciiAlnum s.front
     && s.all (fun c => isAsciiAlnum c || c == '_' || c == '-')
diff --git a/README.md b/README.md
index 3a00922..e098f44 100644
--- a/README.md
+++ b/README.md
@@ -49,3 +49,9 @@ 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
 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
+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.
diff --git a/Tests/Dependencies.lean b/Tests/Dependencies.lean
index 8b9bcf6..c820e26 100644
--- a/Tests/Dependencies.lean
+++ b/Tests/Dependencies.lean
@@ -128,6 +128,25 @@ def main : IO Unit := do
     unless ((lakefileToml "odd" #[odd] (withChallengeDeps := false)).splitOn
         "git = \"https://x.org/\\\"q\\\"\"\nrev = \"r\\\\1\"\n").length == 2 do
       throw <| IO.userError "lakefile require values are not TOML-escaped"
+
+    -- Generation rejects a mathlib require that a workspace would not
+    -- reproduce faithfully; the legacy mathlib loader still ignores the field.
+    let subDirRoot := root / "subdir-mathlib"
+    IO.FS.createDirAll subDirRoot
+    IO.FS.writeFile (subDirRoot / "lakefile.toml") <|
+      "name = \"fixture\"\n\n" ++ mathlibBlock.dropEnd 1 ++ "subDir = \"x\"\n"
+    match ← (loadRootDependencies subDirRoot).toBaseIO with
+    | .ok _ => throw <| IO.userError "mathlib require with `subDir` was accepted"
+    | .error e =>
+        unless ((toString e).splitOn "`subDir`").length > 1 do
+          throw <| IO.userError s!"unexpected mathlib `subDir` error: {e}"
+    expectEq "legacy loader ignores mathlib subDir"
+      (← loadRootMathlibDependency subDirRoot).rev mathlibRev
+
+    -- The workspace name is emitted as a TOML string too.
+    unless ((lakefileToml "a\"b" #[] (withChallengeDeps := false)).startsWith
+        "name = \"a\\\"b\"\n") do
+      throw <| IO.userError "workspace name is not TOML-escaped"
   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 3cfe7aa..3c80161 100644
--- a/schemas/request-v1.schema.json
+++ b/schemas/request-v1.schema.json
@@ -106,7 +106,7 @@
         "resolvedHoles"
       ],
       "properties": {
-        "id": { "type": "string", "minLength": 1 },
+        "id": { "type": "string", "pattern": "^[A-Za-z0-9][A-Za-z0-9_-]*$" },
         "title": { "type": "string", "minLength": 1 },
         "group": {
           "enum": ["formalization-evaluation", "software-verification", "open-conjectures"]
diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py
index 6c9b860..bd003d7 100644
--- a/tests/scripts/contract.py
+++ b/tests/scripts/contract.py
@@ -210,6 +210,11 @@ def main() -> int:
     ]
     assert_rejected(dependency_unknown, "dependency contains an unknown field")
 
+    for bad_id in ["", "-leading", 'a"b', "a b", "a\\b", "a.b", "é"]:
+        invalid_id = problem()
+        invalid_id["id"] = bad_id
+        assert_rejected(request_with(invalid_id), "is invalid")
+
     check_extra_dependencies()
 
     print("PASS schema errors stay off stdout and quoted source/ilean paths resolve")