fix: synchronize standalone generator with LeanEval

LeanEvalGenerator/Contract.lean

@@ -33,7 +33,7 @@ structure ResolvedHole where
   deriving FromJson, Inhabited
 
 /-- All problem-specific data supplied to the renderer. `contextRoot` remains
-necessary in v1 for trusted helper modules and `.ilean` declaration spans. -/
+necessary in schema version 1 for trusted helper modules and `.ilean` declaration spans. -/
 structure ProblemInput where
   id : String
   title : String

README.md

@@ -5,7 +5,7 @@ LeanEval. Its `lean-eval-generator` executable accepts one versioned JSON
 request on stdin (or from a single file argument), writes one JSON response to
 stdout, and writes diagnostics only to stderr.
 
-The v1 request supplies benchmark context, exact Lean/Mathlib pins, templates,
+The schema-version-1 request supplies benchmark context, exact Lean/Mathlib pins, templates,
 marked module content, and hole metadata resolved by the consumer's Lean
 environment. The response contains the complete generated file map and a
 SHA-256 digest for every file. The executable does not write generated files.
@@ -19,9 +19,9 @@ python3 tests/scripts/golden.py /path/to/lean-eval
 python3 tests/scripts/contract.py
 ```
 
-The benchmark context is still required in v1 to resolve trusted imported
+The benchmark context is still required in schema version 1 to resolve trusted imported
 modules and declaration spans from `.ilean` data. A future wire version can
-replace that context with an explicit dependency bundle without changing v1.
+replace that context with an explicit dependency bundle without changing schema version 1.
 
 The consumer owns hole resolution. This matches the interface needed by the
 Formal Conjectures importer: it can resolve declarations under LeanEval's

schemas/request-v1.schema.json

@@ -1,7 +1,7 @@
 {
   "$schema": "https://json-schema.org/draft/2020-12/schema",
   "$id": "https://leanprover.github.io/lean-eval-generator/request-v1.schema.json",
-  "title": "LeanEval generator request v1",
+  "title": "LeanEval generator request schema version 1",
   "type": "object",
   "additionalProperties": false,
   "required": [

schemas/response-v1.schema.json

@@ -1,7 +1,7 @@
 {
   "$schema": "https://json-schema.org/draft/2020-12/schema",
   "$id": "https://leanprover.github.io/lean-eval-generator/response-v1.schema.json",
-  "title": "LeanEval generator response v1",
+  "title": "LeanEval generator response schema version 1",
   "type": "object",
   "additionalProperties": false,
   "required": ["schemaVersion", "files"],
@@ -23,4 +23,3 @@
     }
   }
 }
-

tests/Context.lean

@@ -55,4 +55,16 @@ def main : IO Unit := do
       isLocalSyntaxContextDeclaration)
     "local notation \"A\" => Nat\n\n"
 
+  let markerFixtureRoot : System.FilePath := "/tmp/lean-eval-generator-marker-wrapper-test"
+  IO.FS.createDirAll (markerFixtureRoot / "EvalTools")
+  IO.FS.createDirAll (markerFixtureRoot / "LeanEval")
+  IO.FS.writeFile (markerFixtureRoot / "EvalTools" / "Markers.lean")
+    ("import Lake.Toml\nimport Lake.Util.Message\nimport Lean\n" ++
+      "import LeanEvalGenerator.Core.Markers\n")
+  IO.FS.writeFile (markerFixtureRoot / "LeanEval" / "Fixture.lean")
+    "import EvalTools.Markers\n"
+  expectEq "marker wrapper preserves only the trusted environment"
+    (← problemImportHeader markerFixtureRoot "LeanEval.Fixture")
+    "import Lake.Toml\nimport Lake.Util.Message\nimport Lean\n"
+
   IO.println "PASS active set_option context is preserved without scoped-option leakage"

tests/scripts/contract.py

@@ -1,3 +1,4 @@
+#!/usr/bin/env python3
 """Small dependency-free checks for the CLI transport contract."""
 
 from __future__ import annotations
@@ -9,6 +10,7 @@
 
 from golden import module_path as golden_module_path
 
+
 ROOT = Path(__file__).resolve().parents[2]
 CLI = ROOT / ".lake/build/bin/lean-eval-generator"