From 06527b06ea75b6b794bb6cc38ef516b0e81fd8d7 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+williamjblair@users.noreply.github.com> Date: Tue, 8 Sep 2026 11:42:36 +0100 Subject: [PATCH 1/5] Support pinned package dependencies in generator contract v2 --- .github/workflows/ci.yml | 3 + LeanEvalGenerator/Contract.lean | 36 +++- LeanEvalGenerator/Core/Generate.lean | 23 ++- README.md | 37 ++++ schemas/request-v2.schema.json | 272 +++++++++++++++++++++++++++ schemas/response-v2.schema.json | 46 +++++ tests/scripts/contract.py | 4 +- 7 files changed, 403 insertions(+), 18 deletions(-) create mode 100644 schemas/request-v2.schema.json create mode 100644 schemas/response-v2.schema.json diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7704d8f..cec6661 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -37,6 +37,9 @@ jobs: - name: Check versioned JSON contract run: python3 tests/scripts/contract.py + - name: Build a workspace with a pinned external package + run: python3 tests/scripts/packages.py + - name: Check quoted module and declaration paths run: lake build test_module_paths && lake env .lake/build/bin/test_module_paths diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean index 0f706dd..80fb8a9 100644 --- a/LeanEvalGenerator/Contract.lean +++ b/LeanEvalGenerator/Contract.lean @@ -57,14 +57,15 @@ structure GenerateRequest where contextRoot : String leanToolchain : String mathlib : DependencyPin + dependencies : Array DependencyPin := #[] templates : TemplateInputs problems : Array ProblemInput deriving FromJson private def validateRequest (request : GenerateRequest) : IO Unit := do - if request.schemaVersion != contractVersion then + if request.schemaVersion != 1 && request.schemaVersion != 2 then throw <| IO.userError - s!"Unsupported schemaVersion {request.schemaVersion}; expected {contractVersion}." + s!"Unsupported schemaVersion {request.schemaVersion}; expected 1 or 2." if request.problems.isEmpty then throw <| IO.userError "The request must contain at least one problem." if request.contextRoot.isEmpty then @@ -75,6 +76,20 @@ 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." + if request.schemaVersion == 1 && !request.dependencies.isEmpty then + throw <| IO.userError "Additional dependencies require schemaVersion 2." + let mut names := #["mathlib"] + for dep in request.dependencies do + if dep.name.isEmpty || !(dep.name.toList.all fun c => (c.toNat < 128 && c.isAlphanum) || c == '_' || c == '-') then + throw <| IO.userError "Dependency names must be non-empty package identifiers." + if names.contains dep.name then + throw <| IO.userError s!"Duplicate dependency `{dep.name}`." + names := names.push dep.name + if dep.git.isEmpty then + throw <| IO.userError s!"Dependency `{dep.name}` requires a git URL." + if dep.rev.length != 40 || !(dep.rev.toList.all fun c => + c.isDigit || ('a' ≤ c && c ≤ 'f')) then + throw <| IO.userError s!"Dependency `{dep.name}` requires a full lowercase commit SHA." let mut problemIds : Array String := #[] for problem in request.problems do if problemIds.contains problem.id then @@ -201,10 +216,11 @@ def render (request : GenerateRequest) : IO String := do let rendered ← LeanEvalGenerator.Core.renderWorkspace root (metadata problem) (problem.resolvedHoles.map extracted) request.leanToolchain mathlib request.templates.workspaceTest + (request.dependencies.map fun dep => { name := dep.name, git := dep.git, rev := dep.rev }) for (path, content) in rendered do files := files.push <| fileJson problem.id path content (← sha256 content) let response := LeanEvalGenerator.Core.ojObj #[ - ("schemaVersion", LeanEvalGenerator.Core.ojNat contractVersion), + ("schemaVersion", LeanEvalGenerator.Core.ojNat request.schemaVersion), ("files", LeanEvalGenerator.Core.ojArr files) ] return LeanEvalGenerator.Core.OJson.pretty response ++ "\n" @@ -216,9 +232,12 @@ private def ensureKnownFields (label : String) (allowed : Array String) throw s!"{label} contains an unknown field" private def validateJsonShape (value : Json) : Except String Unit := do - ensureKnownFields "request" #[ - "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "templates", "problems" - ] value + let version ← value.getObjValAs? Nat "schemaVersion" + let fields := #["schemaVersion", "contextRoot", "leanToolchain", "mathlib", "templates", "problems"] + ensureKnownFields "request" (if version == 2 then fields.push "dependencies" else fields) value + if version == 2 then + for dep in (← (← value.getObjVal? "dependencies").getArr?) do + ensureKnownFields "dependency" #["name", "git", "rev"] dep let mathlib ← value.getObjVal? "mathlib" ensureKnownFields "mathlib" #["name", "git", "rev"] mathlib let templates ← value.getObjVal? "templates" @@ -240,6 +259,9 @@ private def validateJsonShape (value : Json) : Except String Unit := do def parseRequest (payload : String) : Except String GenerateRequest := do let value ← Json.parse payload validateJsonShape value - fromJson? value + let version ← value.getObjValAs? Nat "schemaVersion" + if version != 1 && version != 2 then + throw s!"Unsupported schemaVersion {version}; expected 1 or 2." + fromJson? (if version == 1 then value.setObjVal! "dependencies" (toJson (#[] : Array Json)) else value) end LeanEvalGenerator diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean index 686e9a8..df4a69a 100644 --- a/LeanEvalGenerator/Core/Generate.lean +++ b/LeanEvalGenerator/Core/Generate.lean @@ -2893,7 +2893,10 @@ private def renderReadmeLines (entry : EvalProblemMetadata) return lines ++ body private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) - (withChallengeDeps : Bool) : String := + (withChallengeDeps : Bool) (dependencies : Array DependencySpec) : String := + let extraRequires := String.join <| dependencies.toList.map fun dep => + "[[require]]\n" ++ s!"name = {dep.name.quote}\n" ++ + s!"git = {dep.git.quote}\n" ++ s!"rev = {dep.rev.quote}\n\n" let challengeDepsLib := if withChallengeDeps then "[[lean_lib]]\nname = \"ChallengeDeps\"\n\n" @@ -2907,7 +2910,7 @@ private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) s!"name = \"{mathlibDep.name}\"\n" ++ s!"git = \"{mathlibDep.git}\"\n" ++ s!"rev = \"{mathlibDep.rev}\"\n\n" ++ - challengeDepsLib ++ + extraRequires ++ challengeDepsLib ++ "[[lean_lib]]\nname = \"Challenge\"\n\n" ++ "[[lean_lib]]\nname = \"Solution\"\n\n" ++ "[[lean_lib]]\nname = \"Submission\"\n\n" ++ @@ -2917,7 +2920,8 @@ private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProblemMetadata) (extracteds : Array ExtractedTheorem) (toolchain : String) - (mathlibDep : DependencySpec) (workspaceTest : String) : + (mathlibDep : DependencySpec) (workspaceTest : String) + (dependencies : Array DependencySpec := #[]) : IO (Array (String × String)) := do let sourcePath := moduleSourcePath root entry.moduleName if !(← sourcePath.pathExists) then @@ -3179,7 +3183,7 @@ 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 mathlibDep (withChallengeDeps := hasChallengeDeps) dependencies), ("Challenge.lean", challenge), ("Solution.lean", solutionBody), ("Submission.lean", submissionBody), @@ -3195,7 +3199,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProblemMetadata) (extracted : ExtractedTheorem) (toolchain : String) (mathlibDep : DependencySpec) - (workspaceTest : String) : IO (Array (String × String)) := do + (workspaceTest : String) (dependencies : Array DependencySpec := #[]) : IO (Array (String × String)) := do let sourcePath := moduleSourcePath root entry.moduleName let sourceText ← IO.FS.readFile sourcePath let src := Source.ofString sourceText @@ -3283,7 +3287,7 @@ 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 mathlibDep (withChallengeDeps := hasChallengeDeps) dependencies), ("Challenge.lean", challengeFile), ("Solution.lean", solutionFile), ("Submission.lean", submissionFile), @@ -3298,15 +3302,16 @@ 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) : + (mathlibDep : DependencySpec) (workspaceTest : String) + (dependencies : Array DependencySpec := #[]) : 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 mathlibDep workspaceTest dependencies else - renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest + renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest dependencies let holesJson ← buildHolesMetadata root entry extracteds return baseFiles.push ("holes.json", holesJson) diff --git a/README.md b/README.md index 70103ab..13cc7d2 100644 --- a/README.md +++ b/README.md @@ -27,3 +27,40 @@ 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. + +## Pinned package dependencies + +Schema version 2 adds a required `dependencies` array to the version 1 request. +Each entry contains `name`, `git`, and `rev`; `rev` must be a full lowercase Git +commit SHA. Names must be distinct and must not repeat `mathlib`. For example: + +```json +"dependencies": [ + {"name": "example_support", "git": "https://example.org/support.git", + "rev": "0123456789abcdef0123456789abcdef01234567"} +] +``` + +The renderer emits these dependencies in the workspace Lakefile. Imports of +package modules are preserved when their source files are outside `contextRoot`. +Keep package checkouts in Lake's package directory, not alongside the input +module in `contextRoot`: source modules found there retain the existing local +dependency-copying behavior. Dependencies are request-wide, so batch problems +that use the same environment together. + +The consumer approves the dependency source and resolves a compatible Lean and +Mathlib environment. The generator does not fetch packages or execute their code. +It still requires real declaration metadata under `contextRoot`. The response +uses the request's schema version and the same file-map shape. + +Version 1 remains unchanged and rejects the new field. A version 2 request with +an empty dependency array produces the same files as its version 1 equivalent. +The complete contracts are `schemas/request-v2.schema.json` and +`schemas/response-v2.schema.json`. Run the offline package integration test with: + +```sh +python3 tests/scripts/packages.py +``` + +The test creates local Git packages, compiles real Lean declaration metadata, +generates a workspace, fills its proof, and builds its fixed Solution adapter. diff --git a/schemas/request-v2.schema.json b/schemas/request-v2.schema.json new file mode 100644 index 0000000..9138c11 --- /dev/null +++ b/schemas/request-v2.schema.json @@ -0,0 +1,272 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://leanprover.github.io/lean-eval-generator/request-v2.schema.json", + "title": "LeanEval generator request schema version 2", + "type": "object", + "additionalProperties": false, + "required": [ + "schemaVersion", + "contextRoot", + "leanToolchain", + "mathlib", + "templates", + "problems", + "dependencies" + ], + "properties": { + "schemaVersion": { + "const": 2 + }, + "contextRoot": { + "type": "string", + "minLength": 1 + }, + "leanToolchain": { + "type": "string", + "minLength": 1 + }, + "mathlib": { + "$ref": "#/$defs/dependency" + }, + "templates": { + "type": "object", + "additionalProperties": false, + "required": [ + "workspaceTest" + ], + "properties": { + "workspaceTest": { + "type": "string" + } + } + }, + "problems": { + "type": "array", + "minItems": 1, + "items": { + "$ref": "#/$defs/problem" + } + }, + "dependencies": { + "type": "array", + "items": { + "$ref": "#/$defs/packageDependency" + } + } + }, + "$defs": { + "dependency": { + "type": "object", + "additionalProperties": false, + "required": [ + "name", + "git", + "rev" + ], + "properties": { + "name": { + "const": "mathlib" + }, + "git": { + "type": "string", + "minLength": 1 + }, + "rev": { + "type": "string", + "minLength": 1 + } + } + }, + "resolvedHole": { + "type": "object", + "additionalProperties": false, + "required": [ + "declarationName", + "module", + "startLine", + "startColumn", + "endLine", + "endColumn", + "kind" + ], + "properties": { + "declarationName": { + "type": "string", + "minLength": 1 + }, + "module": { + "type": "string", + "minLength": 1 + }, + "startLine": { + "type": "integer", + "minimum": 1 + }, + "startColumn": { + "type": "integer", + "minimum": 0 + }, + "endLine": { + "type": "integer", + "minimum": 1 + }, + "endColumn": { + "type": "integer", + "minimum": 0 + }, + "explicitParameters": { + "type": [ + "array", + "null" + ], + "items": { + "type": "string" + } + }, + "sameModuleDependencies": { + "type": "array", + "items": { + "type": "string" + } + }, + "holeDependentDependencies": { + "type": "array", + "items": { + "type": "string" + } + }, + "kind": { + "enum": [ + "theorem", + "def", + "instance" + ] + } + } + }, + "problem": { + "type": "object", + "additionalProperties": false, + "required": [ + "id", + "title", + "group", + "status", + "visible", + "statementRevision", + "tags", + "moduleName", + "holes", + "submitter", + "moduleContent", + "resolvedHoles" + ], + "properties": { + "id": { + "type": "string", + "minLength": 1 + }, + "title": { + "type": "string", + "minLength": 1 + }, + "group": { + "enum": [ + "formalization-evaluation", + "software-verification", + "open-conjectures" + ] + }, + "status": { + "enum": [ + "draft", + "active", + "archived" + ] + }, + "visible": { + "type": "boolean" + }, + "statementRevision": { + "type": "integer", + "minimum": 1 + }, + "tags": { + "type": "array", + "uniqueItems": true, + "items": { + "type": "string", + "minLength": 1 + } + }, + "moduleName": { + "type": "string", + "minLength": 1 + }, + "holes": { + "type": "array", + "minItems": 1, + "items": { + "type": "string", + "minLength": 1 + } + }, + "submitter": { + "type": "string", + "minLength": 1 + }, + "notes": { + "type": [ + "string", + "null" + ] + }, + "source": { + "type": [ + "string", + "null" + ] + }, + "informalSolution": { + "type": [ + "string", + "null" + ] + }, + "moduleContent": { + "type": "string" + }, + "resolvedHoles": { + "type": "array", + "minItems": 1, + "items": { + "$ref": "#/$defs/resolvedHole" + } + } + } + }, + "packageDependency": { + "type": "object", + "additionalProperties": false, + "required": [ + "name", + "git", + "rev" + ], + "properties": { + "name": { + "type": "string", + "pattern": "^[A-Za-z0-9_-]+$" + }, + "git": { + "type": "string", + "minLength": 1 + }, + "rev": { + "type": "string", + "pattern": "^[0-9a-f]{40}$" + } + } + } + } +} diff --git a/schemas/response-v2.schema.json b/schemas/response-v2.schema.json new file mode 100644 index 0000000..454fb75 --- /dev/null +++ b/schemas/response-v2.schema.json @@ -0,0 +1,46 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "https://leanprover.github.io/lean-eval-generator/response-v2.schema.json", + "title": "LeanEval generator response schema version 2", + "type": "object", + "additionalProperties": false, + "required": [ + "schemaVersion", + "files" + ], + "properties": { + "schemaVersion": { + "const": 2 + }, + "files": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": [ + "problemId", + "path", + "sha256", + "content" + ], + "properties": { + "problemId": { + "type": "string", + "minLength": 1 + }, + "path": { + "type": "string", + "minLength": 1 + }, + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "content": { + "type": "string" + } + } + } + } + } +} diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py index f10ee9e..be2f635 100644 --- a/tests/scripts/contract.py +++ b/tests/scripts/contract.py @@ -84,7 +84,7 @@ def main() -> int: wrong_version = invoke( json.dumps( { - "schemaVersion": 2, + "schemaVersion": 99, "contextRoot": ".", "leanToolchain": "leanprover/lean4:v0.0.0\n", "mathlib": {"name": "mathlib", "git": "x", "rev": "y"}, @@ -95,7 +95,7 @@ def main() -> int: ) assert wrong_version.returncode == 1 assert wrong_version.stdout == "" - assert "Unsupported schemaVersion 2; expected 1" in wrong_version.stderr + assert "Unsupported schemaVersion 99; expected 1 or 2" in wrong_version.stderr duplicate_tags = problem() duplicate_tags["tags"] = ["example", "example"] From 3d688f5e205086d539be6a867f07ed7818812189 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+williamjblair@users.noreply.github.com> Date: Tue, 8 Sep 2026 11:43:09 +0100 Subject: [PATCH 2/5] Exercise external package imports and legacy file parity --- tests/scripts/packages.py | 105 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 105 insertions(+) create mode 100644 tests/scripts/packages.py diff --git a/tests/scripts/packages.py b/tests/scripts/packages.py new file mode 100644 index 0000000..2d4bba3 --- /dev/null +++ b/tests/scripts/packages.py @@ -0,0 +1,105 @@ +"""Generate and build an external-package workspace using real Lean metadata.""" + +import hashlib +import json +import os +from pathlib import Path +import subprocess +import tempfile +import tomllib + +from contract import CLI, ROOT, assert_rejected, invoke, problem, request_with + + +def run(args, cwd, env=None): + result = subprocess.run(args, cwd=cwd, env=env, text=True, capture_output=True) + if result.returncode: + raise AssertionError(f"{args}:\n{result.stdout}\n{result.stderr}") + return result.stdout.strip() + + +def package(root, name, module, content): + root.mkdir() + (root / "lakefile.toml").write_text( + f'name = "{name}"\n[[lean_lib]]\nname = "{module}"\n' + ) + (root / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) + (root / f"{module}.lean").write_text(content) + run(["git", "init", "-q"], root) + run(["git", "add", "."], root) + run(["git", "-c", "user.name=Fixture", "-c", "user.email=fixture@example.invalid", + "commit", "-qm", "fixture"], root) + return {"name": name, "git": str(root), "rev": run(["git", "rev-parse", "HEAD"], root)} + + +def main(): + run(["lake", "--wfail", "build"], ROOT) + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + mathlib = package(root / "mathlib", "mathlib", "Mathlib", "-- Empty fixture library.\n") + dependency = package(root / "support", "fixture_support", "FixtureSupport", + "namespace FixtureSupport\ndef value : Nat := 7\nend FixtureSupport\n") + run(["lake", "build", "FixtureSupport"], root / "support") + context = root / "context" + context.mkdir() + source = "import FixtureSupport\n\ntheorem fixture : FixtureSupport.value = 7 := by sorry\n" + (context / "Fixture.lean").write_text(source) + metadata = context / ".lake/build/lib/lean/Fixture.ilean" + metadata.parent.mkdir(parents=True) + env = dict(os.environ, LEAN_PATH=str(root / "support/.lake/build/lib/lean")) + run(["lake", "env", "lean", "-i", str(metadata), str(context / "Fixture.lean")], ROOT, env) + p = problem() + p["moduleContent"] = source + p["resolvedHoles"][0].update(declarationName="fixture", startLine=3, + startColumn=0, endLine=3, endColumn=len(source.splitlines()[2]), explicitParameters=[]) + payload = request_with(p) + payload.update(schemaVersion=2, contextRoot=str(context), mathlib=mathlib, + leanToolchain=(ROOT / "lean-toolchain").read_text(), dependencies=[dependency]) + result = invoke(json.dumps(payload)) + assert result.returncode == 0, result.stderr + assert invoke(json.dumps(payload)).stdout == result.stdout + response = json.loads(result.stdout) + assert response["schemaVersion"] == 2 + files = {f["path"]: f["content"] for f in response["files"]} + for f in response["files"]: + assert hashlib.sha256(f["content"].encode()).hexdigest() == f["sha256"] + assert tomllib.loads(files["lakefile.toml"])["require"] == [mathlib, dependency] + assert "ChallengeDeps.lean" not in files + for path in ("Challenge.lean", "Submission.lean", "Solution.lean"): + assert "import FixtureSupport" in files[path] + assert "def value" not in files[path] + workspace = root / "workspace" + workspace.mkdir() + for path, content in files.items(): + target = workspace / path + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(content) + submission = workspace / "Submission.lean" + submission.write_text(submission.read_text().replace("sorry", "rfl")) + run(["lake", "update"], workspace) + run(["lake", "build", "Challenge", "Solution"], workspace) + + # v1 stays strict, including rejection of even an empty new field. + payload["schemaVersion"] = 1 + assert_rejected(payload, "request contains an unknown field") + payload["schemaVersion"] = 2 + for deps, message in [ + ([dependency, dependency], "Duplicate dependency"), + ([dict(dependency, name="mathlib")], "Duplicate dependency"), + ([dict(dependency, rev="main")], "full lowercase commit SHA"), + ([dict(dependency, name="../escape")], "package identifiers"), + ([dict(dependency, extra=True)], "dependency contains an unknown field"), + ]: + payload["dependencies"] = deps + assert_rejected(payload, message) + payload["dependencies"] = [] + v2 = json.loads(invoke(json.dumps(payload)).stdout) + del payload["dependencies"] + payload["schemaVersion"] = 1 + v1 = json.loads(invoke(json.dumps(payload)).stdout) + assert v1["files"] == v2["files"], "Empty v2 dependencies changed legacy rendering" + print("PASS package imports, real metadata, workspace build, pins, and v1 parity") + + +if __name__ == "__main__": + main() From 36db50fdb873d420c90c2f1ab457aea2c79a3e2a Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+williamjblair@users.noreply.github.com> Date: Tue, 8 Sep 2026 12:14:16 +0100 Subject: [PATCH 3/5] Render structured declarations without source ranges or compiler metadata --- .github/workflows/ci.yml | 3 + LeanEvalGenerator/Contract.lean | 2 +- LeanEvalGenerator/Main.lean | 14 ++-- LeanEvalGenerator/Structured.lean | 132 ++++++++++++++++++++++++++++++ README.md | 21 +++++ schemas/request-v3.schema.json | 120 +++++++++++++++++++++++++++ schemas/response-v3.schema.json | 46 +++++++++++ tests/scripts/structured.py | 69 ++++++++++++++++ 8 files changed, 401 insertions(+), 6 deletions(-) create mode 100644 LeanEvalGenerator/Structured.lean create mode 100644 schemas/request-v3.schema.json create mode 100644 schemas/response-v3.schema.json create mode 100644 tests/scripts/structured.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cec6661..7703a20 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -45,3 +45,6 @@ jobs: - name: Check Python test harnesses run: python3 -m py_compile tests/scripts/*.py + + - name: Test structured declaration contract + run: python3 tests/scripts/structured.py diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean index 80fb8a9..da9dfe5 100644 --- a/LeanEvalGenerator/Contract.lean +++ b/LeanEvalGenerator/Contract.lean @@ -96,7 +96,7 @@ private def validateRequest (request : GenerateRequest) : IO Unit := do throw <| IO.userError s!"Duplicate problem id `{problem.id}`." problemIds := problemIds.push problem.id -private def sha256 (content : String) : IO String := do +def sha256 (content : String) : IO String := do let out ← IO.Process.output { cmd := "sha256sum" args := #["-"] diff --git a/LeanEvalGenerator/Main.lean b/LeanEvalGenerator/Main.lean index a45b241..0642940 100644 --- a/LeanEvalGenerator/Main.lean +++ b/LeanEvalGenerator/Main.lean @@ -1,4 +1,4 @@ -import LeanEvalGenerator.Contract +import LeanEvalGenerator.Structured namespace LeanEvalGenerator @@ -14,10 +14,14 @@ private def readRequest : List String → IO String def run (args : List String) : IO UInt32 := do try let payload ← readRequest args - let request ← match parseRequest payload with - | .ok request => pure request - | .error error => throw <| IO.userError s!"Invalid generator request: {error}" - let response ← render request + let value ← IO.ofExcept <| (Lean.Json.parse payload).mapError ("Invalid generator request: " ++ ·) + let version ← IO.ofExcept <| (value.getObjValAs? Nat "schemaVersion").mapError ("Invalid generator request: " ++ ·) + let response ← if version == 3 then do + let request ← IO.ofExcept <| (Structured.parse value).mapError ("Invalid generator request: " ++ ·) + Structured.render request + else do + let request ← IO.ofExcept <| (parseRequest payload).mapError ("Invalid generator request: " ++ ·) + render request IO.print response return 0 catch error => diff --git a/LeanEvalGenerator/Structured.lean b/LeanEvalGenerator/Structured.lean new file mode 100644 index 0000000..bca6102 --- /dev/null +++ b/LeanEvalGenerator/Structured.lean @@ -0,0 +1,132 @@ +import LeanEvalGenerator.Contract + +/-! A source-free renderer for closed declaration signatures. No source slices, +`.ilean` files, dependency discovery, or namespace reconstruction are used. -/ +namespace LeanEvalGenerator.Structured +open Lean + +structure Declaration where + name : String + kind : String + type : String + levels : Array String + deriving FromJson, ToJson + +structure Problem where + id : String + title : String + imports : Array String + declarations : Array Declaration + deriving FromJson + +structure Request where + schemaVersion : Nat + leanToolchain : String + dependencies : Array DependencyPin + templates : TemplateInputs + problems : Array Problem + deriving FromJson + +private def exactFields (value : Json) (fields : List String) : Except String Unit := do + let object ← value.getObj? + unless object.size == fields.length && object.all (fun k _ => fields.contains k) do + throw "Unexpected or missing structured request fields" + +def parse (value : Json) : Except String Request := do + exactFields value ["schemaVersion", "leanToolchain", "dependencies", "templates", "problems"] + exactFields (← value.getObjVal? "templates") ["workspaceTest"] + for d in (← value.getObjValAs? (Array Json) "dependencies") do + exactFields d ["name", "git", "rev"] + for p in (← value.getObjValAs? (Array Json) "problems") do + exactFields p ["id", "title", "imports", "declarations"] + for d in (← p.getObjValAs? (Array Json) "declarations") do + exactFields d ["name", "kind", "type", "levels"] + fromJson? value + +private def identifier (s : String) : Bool := + !s.isEmpty && (s.toList.head!.isAlpha || s.startsWith "_") && + s.toList.all (fun c => c.toNat < 128 && (c.isAlphanum || c == '_')) + +private def require (condition : Bool) (message : String) : IO Unit := + unless condition do throw <| IO.userError message + +private def validate (r : Request) : IO Unit := do + require (r.schemaVersion == 3) "Expected schemaVersion 3" + require (!r.leanToolchain.trimAscii.isEmpty && !r.problems.isEmpty) "Empty toolchain or problems" + let mut packages := #[] + for d in r.dependencies do + require (identifier (d.name.replace "-" "_") && !packages.contains d.name) + "Invalid or duplicate package name" + require (!d.git.isEmpty && d.rev.length == 40 && d.rev.toList.all + (fun c => c.isDigit || ('a' ≤ c && c ≤ 'f'))) "Expected package URL and full lowercase commit SHA" + packages := packages.push d.name + let mut ids := #[] + for p in r.problems do + require (identifier p.id && !ids.contains p.id && !p.title.isEmpty) "Invalid or duplicate problem id" + ids := ids.push p.id + require (!p.imports.isEmpty && !p.declarations.isEmpty) "Empty imports or declarations" + -- Use Lean's parser to validate syntax boundaries, never an approximate lexer. + for name in p.imports do + let ctx := Parser.mkInputContext s!"import {name}\n" "" + let (header, state, messages) ← Parser.parseHeader ctx + let imports := Elab.HeaderSyntax.imports header (includeInit := false) + require (!messages.hasErrors && ctx.atEnd state.pos && imports.size == 1 && + imports[0]!.module.toString == name.toName.toString) "Invalid module import" + let mut names := #[] + for d in p.declarations do + require (identifier d.name && !names.contains d.name) "Invalid or duplicate declaration name" + names := names.push d.name + require (d.kind == "def" || d.kind == "theorem") "Expected def or theorem" + require (d.levels.all identifier && d.levels.toList.eraseDups.length == d.levels.size) + "Invalid universe parameters" + -- Type syntax belongs to the producer's Lean environment (which may + -- provide notation unknown to this renderer). It is trusted input, + -- just like v1 moduleContent, and must be validated by the consumer. + require (!d.type.trimAscii.isEmpty) "Empty declaration type" + +private def levelSuffix (d : Declaration) : String := + if d.levels.isEmpty then "" else ".{" ++ String.intercalate ", " d.levels.toList ++ "}" + +private def declaration (d : Declaration) (solution : Bool := false) : String := + let command := if d.kind == "def" then + (if solution then "@[reducible] " else "") ++ "noncomputable def" else "theorem" + let body := if solution then "@Submission." ++ d.name ++ levelSuffix d else "by\n sorry" + s!"{command} {d.name}{levelSuffix d} : {d.type} := {body}\n\n" + +private def workspace (r : Request) (p : Problem) : Array (String × String) := Id.run do + let imports := String.join (p.imports.toList.map (fun n => s!"import {n}\n")) ++ "\n" + let holes := String.join (p.declarations.toList.map (declaration ·)) + let challenge := imports ++ holes + let submission := imports ++ "import Submission.Helpers\n\nnamespace Submission\n\n" ++ + holes ++ "end Submission\n" + let solution := imports ++ "import Submission\n\n" ++ + String.join (p.declarations.toList.map (declaration · true)) + let deps := String.join <| r.dependencies.toList.map fun d => + s!"[[require]]\nname = {d.name.quote}\ngit = {d.git.quote}\nrev = {d.rev.quote}\n\n" + let lakefile := s!"name = {p.id.quote}\nversion = \"0.1.0\"\ndefaultTargets = [\"Challenge\", \"Solution\"]\ntestDriver = \"workspace_test\"\n\n" ++ + deps ++ "[[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" + let config := Json.mkObj [ + ("challenge_module", toJson "Challenge"), ("solution_module", toJson "Solution"), + ("theorem_names", toJson (p.declarations.filter (·.kind == "theorem") |>.map (·.name))), + ("definition_names", toJson (p.declarations.filter (·.kind == "def") |>.map (·.name))), + ("permitted_axioms", toJson #["propext", "Quot.sound", "Classical.choice"])] + return #[("Challenge.lean", challenge), ("Submission.lean", submission), + ("Submission/Helpers.lean", imports), ("Solution.lean", solution), + ("lakefile.toml", lakefile), ("lean-toolchain", r.leanToolchain.trimAscii.toString ++ "\n"), + ("WorkspaceTest.lean", r.templates.workspaceTest), ("config.json", config.pretty ++ "\n"), + ("holes.json", (Json.mkObj [("id", toJson p.id), + ("declarations", toJson p.declarations)]).pretty ++ "\n"), + ("README.md", s!"# {p.title}\n\nFill the holes in Submission.lean. Keep Challenge.lean and Solution.lean unchanged.\nRun `lake test` with the configured Comparator and sandbox.\n")] + +/-- Render only the supplied signatures; the consumer must compile the result +under its pinned imports before publishing it as a challenge. -/ +def render (r : Request) : IO String := do + validate r + let mut files := #[] + for p in r.problems do + for (path, content) in workspace r p do + files := files.push <| Json.mkObj [("problemId", toJson p.id), ("path", toJson path), + ("content", toJson content), ("sha256", toJson (← LeanEvalGenerator.sha256 content))] + return (Json.mkObj [("schemaVersion", toJson (3 : Nat)), ("files", toJson files)]).pretty ++ "\n" + +end LeanEvalGenerator.Structured diff --git a/README.md b/README.md index 13cc7d2..dc8f085 100644 --- a/README.md +++ b/README.md @@ -64,3 +64,24 @@ python3 tests/scripts/packages.py The test creates local Git packages, compiles real Lean declaration metadata, generates a workspace, fills its proof, and builds its fixed Solution adapter. + +## Structured declarations (version 3) + +Version 3 accepts package pins, imports, and ordered declarations with `name`, +`kind`, `type`, and explicit `levels`. It renders Challenge, Submission and Solution +without a context directory, source ranges, `.ilean`, helper discovery, or source +rewriting. Definitions in Solution are reducible aliases to the submitted values, +so later hole types can depend on earlier holes. Signatures contain all binders; +Solution forwards them with an explicit `@` reference and universe arguments. + +The schemas are `schemas/request-v3.schema.json` and `schemas/response-v3.schema.json`. +Types and the test-driver template are trusted source supplied by the consumer, +just as moduleContent is trusted in v1. The consumer must validate the signatures +with its own Lean environment and compile the generated Challenge before use. +The renderer does not interpret type syntax using its potentially different Lean +version. Import boundaries are validated with Lean's header parser. All versions +remain supported; no legacy source-processing path is used for v3 requests. + +Run `python3 tests/scripts/structured.py` to exercise real Git package resolution, +dependent definition holes, polymorphic theorems, deterministic output and invalid +request rejection, without any source context or compiler metadata. diff --git a/schemas/request-v3.schema.json b/schemas/request-v3.schema.json new file mode 100644 index 0000000..67bd0a3 --- /dev/null +++ b/schemas/request-v3.schema.json @@ -0,0 +1,120 @@ +{ + "type": "object", + "properties": { + "schemaVersion": { + "const": 3 + }, + "leanToolchain": { + "type": "string" + }, + "dependencies": { + "type": "array", + "items": { + "type": "object", + "properties": { + "name": { + "type": "string" + }, + "git": { + "type": "string" + }, + "rev": { + "type": "string", + "pattern": "^[0-9a-f]{40}$" + } + }, + "required": [ + "name", + "git", + "rev" + ], + "additionalProperties": false + } + }, + "templates": { + "type": "object", + "properties": { + "workspaceTest": { + "type": "string" + } + }, + "required": [ + "workspaceTest" + ], + "additionalProperties": false + }, + "problems": { + "type": "array", + "items": { + "type": "object", + "properties": { + "id": { + "type": "string" + }, + "title": { + "type": "string" + }, + "imports": { + "type": "array", + "items": { + "type": "string" + } + }, + "declarations": { + "type": "array", + "items": { + "type": "object", + "properties": { + "name": { + "type": "string", + "pattern": "^[A-Za-z_][A-Za-z0-9_]*$" + }, + "kind": { + "enum": [ + "def", + "theorem" + ] + }, + "type": { + "type": "string", + "minLength": 1 + }, + "levels": { + "type": "array", + "items": { + "type": "string" + } + } + }, + "required": [ + "name", + "kind", + "type", + "levels" + ], + "additionalProperties": false + } + } + }, + "required": [ + "id", + "title", + "imports", + "declarations" + ], + "additionalProperties": false + } + } + }, + "required": [ + "schemaVersion", + "leanToolchain", + "dependencies", + "templates", + "problems" + ], + "additionalProperties": false, + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "request-v3.schema.json", + "title": "Structured package-backed workspace request" +} diff --git a/schemas/response-v3.schema.json b/schemas/response-v3.schema.json new file mode 100644 index 0000000..c6ce455 --- /dev/null +++ b/schemas/response-v3.schema.json @@ -0,0 +1,46 @@ +{ + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "response-v3.schema.json", + "title": "Structured workspace response", + "type": "object", + "additionalProperties": false, + "required": [ + "schemaVersion", + "files" + ], + "properties": { + "schemaVersion": { + "const": 3 + }, + "files": { + "type": "array", + "items": { + "type": "object", + "additionalProperties": false, + "required": [ + "problemId", + "path", + "sha256", + "content" + ], + "properties": { + "problemId": { + "type": "string", + "minLength": 1 + }, + "path": { + "type": "string", + "minLength": 1 + }, + "sha256": { + "type": "string", + "pattern": "^[0-9a-f]{64}$" + }, + "content": { + "type": "string" + } + } + } + } + } +} diff --git a/tests/scripts/structured.py b/tests/scripts/structured.py new file mode 100644 index 0000000..a8acca5 --- /dev/null +++ b/tests/scripts/structured.py @@ -0,0 +1,69 @@ +"""Source-free contract: no context tree or .ilean, including dependent holes.""" +import copy +import hashlib +import json +from pathlib import Path +import tempfile +import tomllib + +from contract import ROOT, invoke +from packages import package, run + + +def main(): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + support = package(root / 'support', 'fixture_support', 'FixtureSupport', + 'def FixtureSupport.value : Nat := 7\n') + request = {'schemaVersion': 3, 'leanToolchain': (ROOT / 'lean-toolchain').read_text(), + 'dependencies': [support], 'templates': {'workspaceTest': 'def main : IO Unit := pure ()\n'}, + 'problems': [{'id': 'structured', 'title': 'Structured fixtures', + 'imports': ['FixtureSupport'], 'declarations': [ + {'name': 'answer', 'kind': 'def', 'type': 'Nat', 'levels': []}, + {'name': 'second', 'kind': 'def', 'type': 'Fin (answer + 1)', 'levels': []}, + {'name': 'problem', 'kind': 'theorem', + 'type': 'answer = FixtureSupport.value ∧ second.val ≤ answer', 'levels': []}, + {'name': 'poly', 'kind': 'theorem', + 'type': '∀ (α : Type u) (x : α), x = x', 'levels': ['u']}]}]} + result = invoke(json.dumps(request)) + assert result.returncode == 0, result.stderr + assert invoke(json.dumps(request)).stdout == result.stdout + response = json.loads(result.stdout) + assert response['schemaVersion'] == 3 + files = {f['path']: f['content'] for f in response['files']} + for f in response['files']: + assert hashlib.sha256(f['content'].encode()).hexdigest() == f['sha256'] + assert tomllib.loads(files['lakefile.toml'])['require'] == [support] + assert not any('Deps' in name or name.endswith('.ilean') for name in files) + workspace = root / 'workspace' + workspace.mkdir() + for name, content in files.items(): + p = workspace / name + p.parent.mkdir(parents=True, exist_ok=True) + p.write_text(content) + submission = workspace / 'Submission.lean' + text = submission.read_text() + for proof in ['exact 7', 'exact ⟨0, by decide⟩', 'constructor <;> decide', 'intro α x; rfl']: + text = text.replace('sorry', proof, 1) + submission.write_text(text) + run(['lake', 'update'], workspace) + run(['lake', 'build', 'Challenge', 'Solution'], workspace) + mutations = [ + lambda r: r.update(contextRoot='unused'), + lambda r: r['dependencies'][0].update(rev='master'), + lambda r: r['dependencies'].append(r['dependencies'][0]), + lambda r: r['problems'][0].update(imports=['FixtureSupport\naxiom bad : False']), + lambda r: r['problems'][0]['declarations'][0].update(name='../bad'), + lambda r: r['problems'][0]['declarations'][0].update(kind='axiom'), + lambda r: r['problems'][0]['declarations'][0].update(levels=['u\naxiom bad : False']), + lambda r: r['problems'][0]['declarations'].append(r['problems'][0]['declarations'][0]), + ] + for mutation in mutations: + bad = copy.deepcopy(request) + mutation(bad) + assert invoke(json.dumps(bad)).returncode != 0, bad + print('PASS structured rendering, real Git dependencies, dependent holes, universes, malformed requests') + + +if __name__ == '__main__': + main() From 166d574bb9eee2765149200f959222f2c6b4cdbc Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+williamjblair@users.noreply.github.com> Date: Tue, 8 Sep 2026 12:20:35 +0100 Subject: [PATCH 4/5] Make the unmerged v2 contract source-free and expose kernel policy --- .github/workflows/ci.yml | 3 - LeanEvalGenerator/Contract.lean | 36 +-- LeanEvalGenerator/Core/Generate.lean | 23 +- LeanEvalGenerator/Main.lean | 4 +- LeanEvalGenerator/Structured.lean | 8 +- README.md | 47 +--- schemas/request-v2.schema.json | 342 ++++++++------------------- schemas/request-v3.schema.json | 120 ---------- schemas/response-v2.schema.json | 4 +- schemas/response-v3.schema.json | 46 ---- tests/scripts/packages.py | 105 -------- tests/scripts/structured.py | 28 ++- 12 files changed, 153 insertions(+), 613 deletions(-) delete mode 100644 schemas/request-v3.schema.json delete mode 100644 schemas/response-v3.schema.json delete mode 100644 tests/scripts/packages.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7703a20..2758ca6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -37,9 +37,6 @@ jobs: - name: Check versioned JSON contract run: python3 tests/scripts/contract.py - - name: Build a workspace with a pinned external package - run: python3 tests/scripts/packages.py - - name: Check quoted module and declaration paths run: lake build test_module_paths && lake env .lake/build/bin/test_module_paths diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean index da9dfe5..491cd7e 100644 --- a/LeanEvalGenerator/Contract.lean +++ b/LeanEvalGenerator/Contract.lean @@ -57,15 +57,14 @@ structure GenerateRequest where contextRoot : String leanToolchain : String mathlib : DependencyPin - dependencies : Array DependencyPin := #[] templates : TemplateInputs problems : Array ProblemInput deriving FromJson private def validateRequest (request : GenerateRequest) : IO Unit := do - if request.schemaVersion != 1 && request.schemaVersion != 2 then + if request.schemaVersion != contractVersion then throw <| IO.userError - s!"Unsupported schemaVersion {request.schemaVersion}; expected 1 or 2." + s!"Unsupported schemaVersion {request.schemaVersion}; expected {contractVersion}." if request.problems.isEmpty then throw <| IO.userError "The request must contain at least one problem." if request.contextRoot.isEmpty then @@ -76,20 +75,6 @@ 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." - if request.schemaVersion == 1 && !request.dependencies.isEmpty then - throw <| IO.userError "Additional dependencies require schemaVersion 2." - let mut names := #["mathlib"] - for dep in request.dependencies do - if dep.name.isEmpty || !(dep.name.toList.all fun c => (c.toNat < 128 && c.isAlphanum) || c == '_' || c == '-') then - throw <| IO.userError "Dependency names must be non-empty package identifiers." - if names.contains dep.name then - throw <| IO.userError s!"Duplicate dependency `{dep.name}`." - names := names.push dep.name - if dep.git.isEmpty then - throw <| IO.userError s!"Dependency `{dep.name}` requires a git URL." - if dep.rev.length != 40 || !(dep.rev.toList.all fun c => - c.isDigit || ('a' ≤ c && c ≤ 'f')) then - throw <| IO.userError s!"Dependency `{dep.name}` requires a full lowercase commit SHA." let mut problemIds : Array String := #[] for problem in request.problems do if problemIds.contains problem.id then @@ -216,11 +201,10 @@ def render (request : GenerateRequest) : IO String := do let rendered ← LeanEvalGenerator.Core.renderWorkspace root (metadata problem) (problem.resolvedHoles.map extracted) request.leanToolchain mathlib request.templates.workspaceTest - (request.dependencies.map fun dep => { name := dep.name, git := dep.git, rev := dep.rev }) for (path, content) in rendered do files := files.push <| fileJson problem.id path content (← sha256 content) let response := LeanEvalGenerator.Core.ojObj #[ - ("schemaVersion", LeanEvalGenerator.Core.ojNat request.schemaVersion), + ("schemaVersion", LeanEvalGenerator.Core.ojNat contractVersion), ("files", LeanEvalGenerator.Core.ojArr files) ] return LeanEvalGenerator.Core.OJson.pretty response ++ "\n" @@ -232,12 +216,9 @@ private def ensureKnownFields (label : String) (allowed : Array String) throw s!"{label} contains an unknown field" private def validateJsonShape (value : Json) : Except String Unit := do - let version ← value.getObjValAs? Nat "schemaVersion" - let fields := #["schemaVersion", "contextRoot", "leanToolchain", "mathlib", "templates", "problems"] - ensureKnownFields "request" (if version == 2 then fields.push "dependencies" else fields) value - if version == 2 then - for dep in (← (← value.getObjVal? "dependencies").getArr?) do - ensureKnownFields "dependency" #["name", "git", "rev"] dep + ensureKnownFields "request" #[ + "schemaVersion", "contextRoot", "leanToolchain", "mathlib", "templates", "problems" + ] value let mathlib ← value.getObjVal? "mathlib" ensureKnownFields "mathlib" #["name", "git", "rev"] mathlib let templates ← value.getObjVal? "templates" @@ -259,9 +240,6 @@ private def validateJsonShape (value : Json) : Except String Unit := do def parseRequest (payload : String) : Except String GenerateRequest := do let value ← Json.parse payload validateJsonShape value - let version ← value.getObjValAs? Nat "schemaVersion" - if version != 1 && version != 2 then - throw s!"Unsupported schemaVersion {version}; expected 1 or 2." - fromJson? (if version == 1 then value.setObjVal! "dependencies" (toJson (#[] : Array Json)) else value) + fromJson? value end LeanEvalGenerator diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean index df4a69a..686e9a8 100644 --- a/LeanEvalGenerator/Core/Generate.lean +++ b/LeanEvalGenerator/Core/Generate.lean @@ -2893,10 +2893,7 @@ private def renderReadmeLines (entry : EvalProblemMetadata) return lines ++ body private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) - (withChallengeDeps : Bool) (dependencies : Array DependencySpec) : String := - let extraRequires := String.join <| dependencies.toList.map fun dep => - "[[require]]\n" ++ s!"name = {dep.name.quote}\n" ++ - s!"git = {dep.git.quote}\n" ++ s!"rev = {dep.rev.quote}\n\n" + (withChallengeDeps : Bool) : String := let challengeDepsLib := if withChallengeDeps then "[[lean_lib]]\nname = \"ChallengeDeps\"\n\n" @@ -2910,7 +2907,7 @@ private def lakefileToml (problemId : String) (mathlibDep : DependencySpec) s!"name = \"{mathlibDep.name}\"\n" ++ s!"git = \"{mathlibDep.git}\"\n" ++ s!"rev = \"{mathlibDep.rev}\"\n\n" ++ - extraRequires ++ challengeDepsLib ++ + challengeDepsLib ++ "[[lean_lib]]\nname = \"Challenge\"\n\n" ++ "[[lean_lib]]\nname = \"Solution\"\n\n" ++ "[[lean_lib]]\nname = \"Submission\"\n\n" ++ @@ -2920,8 +2917,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) - (dependencies : Array DependencySpec := #[]) : + (mathlibDep : DependencySpec) (workspaceTest : String) : IO (Array (String × String)) := do let sourcePath := moduleSourcePath root entry.moduleName if !(← sourcePath.pathExists) then @@ -3183,7 +3179,7 @@ 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) dependencies), + ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)), ("Challenge.lean", challenge), ("Solution.lean", solutionBody), ("Submission.lean", submissionBody), @@ -3199,7 +3195,7 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl private def renderWorkspaceSingleHole (root : System.FilePath) (entry : EvalProblemMetadata) (extracted : ExtractedTheorem) (toolchain : String) (mathlibDep : DependencySpec) - (workspaceTest : String) (dependencies : Array DependencySpec := #[]) : IO (Array (String × String)) := do + (workspaceTest : String) : IO (Array (String × String)) := do let sourcePath := moduleSourcePath root entry.moduleName let sourceText ← IO.FS.readFile sourcePath let src := Source.ofString sourceText @@ -3287,7 +3283,7 @@ 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) dependencies), + ("lakefile.toml", lakefileToml entry.id mathlibDep (withChallengeDeps := hasChallengeDeps)), ("Challenge.lean", challengeFile), ("Solution.lean", solutionFile), ("Submission.lean", submissionFile), @@ -3302,16 +3298,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) - (dependencies : Array DependencySpec := #[]) : + (mathlibDep : DependencySpec) (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 dependencies + renderWorkspaceMultiHole root entry extracteds toolchain mathlibDep workspaceTest else - renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest dependencies + renderWorkspaceSingleHole root entry extracteds[0]! toolchain mathlibDep workspaceTest let holesJson ← buildHolesMetadata root entry extracteds return baseFiles.push ("holes.json", holesJson) diff --git a/LeanEvalGenerator/Main.lean b/LeanEvalGenerator/Main.lean index 0642940..1f280f7 100644 --- a/LeanEvalGenerator/Main.lean +++ b/LeanEvalGenerator/Main.lean @@ -16,7 +16,9 @@ def run (args : List String) : IO UInt32 := do let payload ← readRequest args let value ← IO.ofExcept <| (Lean.Json.parse payload).mapError ("Invalid generator request: " ++ ·) let version ← IO.ofExcept <| (value.getObjValAs? Nat "schemaVersion").mapError ("Invalid generator request: " ++ ·) - let response ← if version == 3 then do + unless version == 1 || version == 2 do + throw <| IO.userError s!"Unsupported schemaVersion {version}; expected 1 or 2." + let response ← if version == 2 then do let request ← IO.ofExcept <| (Structured.parse value).mapError ("Invalid generator request: " ++ ·) Structured.render request else do diff --git a/LeanEvalGenerator/Structured.lean b/LeanEvalGenerator/Structured.lean index bca6102..76d398d 100644 --- a/LeanEvalGenerator/Structured.lean +++ b/LeanEvalGenerator/Structured.lean @@ -22,6 +22,7 @@ structure Problem where structure Request where schemaVersion : Nat leanToolchain : String + enableNanoda : Bool dependencies : Array DependencyPin templates : TemplateInputs problems : Array Problem @@ -33,7 +34,7 @@ private def exactFields (value : Json) (fields : List String) : Except String Un throw "Unexpected or missing structured request fields" def parse (value : Json) : Except String Request := do - exactFields value ["schemaVersion", "leanToolchain", "dependencies", "templates", "problems"] + exactFields value ["schemaVersion", "leanToolchain", "enableNanoda", "dependencies", "templates", "problems"] exactFields (← value.getObjVal? "templates") ["workspaceTest"] for d in (← value.getObjValAs? (Array Json) "dependencies") do exactFields d ["name", "git", "rev"] @@ -51,7 +52,7 @@ private def require (condition : Bool) (message : String) : IO Unit := unless condition do throw <| IO.userError message private def validate (r : Request) : IO Unit := do - require (r.schemaVersion == 3) "Expected schemaVersion 3" + require (r.schemaVersion == 2) "Expected schemaVersion 2" require (!r.leanToolchain.trimAscii.isEmpty && !r.problems.isEmpty) "Empty toolchain or problems" let mut packages := #[] for d in r.dependencies do @@ -109,6 +110,7 @@ private def workspace (r : Request) (p : Problem) : Array (String × String) := ("challenge_module", toJson "Challenge"), ("solution_module", toJson "Solution"), ("theorem_names", toJson (p.declarations.filter (·.kind == "theorem") |>.map (·.name))), ("definition_names", toJson (p.declarations.filter (·.kind == "def") |>.map (·.name))), + ("enable_nanoda", toJson r.enableNanoda), ("permitted_axioms", toJson #["propext", "Quot.sound", "Classical.choice"])] return #[("Challenge.lean", challenge), ("Submission.lean", submission), ("Submission/Helpers.lean", imports), ("Solution.lean", solution), @@ -127,6 +129,6 @@ def render (r : Request) : IO String := do for (path, content) in workspace r p do files := files.push <| Json.mkObj [("problemId", toJson p.id), ("path", toJson path), ("content", toJson content), ("sha256", toJson (← LeanEvalGenerator.sha256 content))] - return (Json.mkObj [("schemaVersion", toJson (3 : Nat)), ("files", toJson files)]).pretty ++ "\n" + return (Json.mkObj [("schemaVersion", toJson (2 : Nat)), ("files", toJson files)]).pretty ++ "\n" end LeanEvalGenerator.Structured diff --git a/README.md b/README.md index dc8f085..9f8b489 100644 --- a/README.md +++ b/README.md @@ -28,59 +28,22 @@ 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. -## Pinned package dependencies +## Structured declarations (version 2) -Schema version 2 adds a required `dependencies` array to the version 1 request. -Each entry contains `name`, `git`, and `rev`; `rev` must be a full lowercase Git -commit SHA. Names must be distinct and must not repeat `mathlib`. For example: - -```json -"dependencies": [ - {"name": "example_support", "git": "https://example.org/support.git", - "rev": "0123456789abcdef0123456789abcdef01234567"} -] -``` - -The renderer emits these dependencies in the workspace Lakefile. Imports of -package modules are preserved when their source files are outside `contextRoot`. -Keep package checkouts in Lake's package directory, not alongside the input -module in `contextRoot`: source modules found there retain the existing local -dependency-copying behavior. Dependencies are request-wide, so batch problems -that use the same environment together. - -The consumer approves the dependency source and resolves a compatible Lean and -Mathlib environment. The generator does not fetch packages or execute their code. -It still requires real declaration metadata under `contextRoot`. The response -uses the request's schema version and the same file-map shape. - -Version 1 remains unchanged and rejects the new field. A version 2 request with -an empty dependency array produces the same files as its version 1 equivalent. -The complete contracts are `schemas/request-v2.schema.json` and -`schemas/response-v2.schema.json`. Run the offline package integration test with: - -```sh -python3 tests/scripts/packages.py -``` - -The test creates local Git packages, compiles real Lean declaration metadata, -generates a workspace, fills its proof, and builds its fixed Solution adapter. - -## Structured declarations (version 3) - -Version 3 accepts package pins, imports, and ordered declarations with `name`, +Version 2 accepts package pins, imports, and ordered declarations with `name`, `kind`, `type`, and explicit `levels`. It renders Challenge, Submission and Solution without a context directory, source ranges, `.ilean`, helper discovery, or source rewriting. Definitions in Solution are reducible aliases to the submitted values, so later hole types can depend on earlier holes. Signatures contain all binders; Solution forwards them with an explicit `@` reference and universe arguments. -The schemas are `schemas/request-v3.schema.json` and `schemas/response-v3.schema.json`. +The schemas are `schemas/request-v2.schema.json` and `schemas/response-v2.schema.json`. Types and the test-driver template are trusted source supplied by the consumer, just as moduleContent is trusted in v1. The consumer must validate the signatures with its own Lean environment and compile the generated Challenge before use. The renderer does not interpret type syntax using its potentially different Lean -version. Import boundaries are validated with Lean's header parser. All versions -remain supported; no legacy source-processing path is used for v3 requests. +version. Import boundaries are validated with Lean's header parser. Version 1 +remains unchanged; no legacy source-processing path is used for v2 requests. Run `python3 tests/scripts/structured.py` to exercise real Git package resolution, dependent definition holes, polymorphic theorems, deterministic output and invalid diff --git a/schemas/request-v2.schema.json b/schemas/request-v2.schema.json index 9138c11..6d0cfb7 100644 --- a/schemas/request-v2.schema.json +++ b/schemas/request-v2.schema.json @@ -1,272 +1,124 @@ { - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://leanprover.github.io/lean-eval-generator/request-v2.schema.json", - "title": "LeanEval generator request schema version 2", "type": "object", - "additionalProperties": false, - "required": [ - "schemaVersion", - "contextRoot", - "leanToolchain", - "mathlib", - "templates", - "problems", - "dependencies" - ], "properties": { "schemaVersion": { "const": 2 }, - "contextRoot": { - "type": "string", - "minLength": 1 - }, "leanToolchain": { - "type": "string", - "minLength": 1 - }, - "mathlib": { - "$ref": "#/$defs/dependency" - }, - "templates": { - "type": "object", - "additionalProperties": false, - "required": [ - "workspaceTest" - ], - "properties": { - "workspaceTest": { - "type": "string" - } - } - }, - "problems": { - "type": "array", - "minItems": 1, - "items": { - "$ref": "#/$defs/problem" - } + "type": "string" }, "dependencies": { "type": "array", "items": { - "$ref": "#/$defs/packageDependency" - } - } - }, - "$defs": { - "dependency": { - "type": "object", - "additionalProperties": false, - "required": [ - "name", - "git", - "rev" - ], - "properties": { - "name": { - "const": "mathlib" - }, - "git": { - "type": "string", - "minLength": 1 - }, - "rev": { - "type": "string", - "minLength": 1 - } - } - }, - "resolvedHole": { - "type": "object", - "additionalProperties": false, - "required": [ - "declarationName", - "module", - "startLine", - "startColumn", - "endLine", - "endColumn", - "kind" - ], - "properties": { - "declarationName": { - "type": "string", - "minLength": 1 - }, - "module": { - "type": "string", - "minLength": 1 - }, - "startLine": { - "type": "integer", - "minimum": 1 - }, - "startColumn": { - "type": "integer", - "minimum": 0 - }, - "endLine": { - "type": "integer", - "minimum": 1 - }, - "endColumn": { - "type": "integer", - "minimum": 0 - }, - "explicitParameters": { - "type": [ - "array", - "null" - ], - "items": { - "type": "string" - } - }, - "sameModuleDependencies": { - "type": "array", - "items": { + "type": "object", + "properties": { + "name": { "type": "string" - } - }, - "holeDependentDependencies": { - "type": "array", - "items": { + }, + "git": { "type": "string" + }, + "rev": { + "type": "string", + "pattern": "^[0-9a-f]{40}$" } }, - "kind": { - "enum": [ - "theorem", - "def", - "instance" - ] - } + "required": [ + "name", + "git", + "rev" + ], + "additionalProperties": false } }, - "problem": { + "templates": { "type": "object", - "additionalProperties": false, - "required": [ - "id", - "title", - "group", - "status", - "visible", - "statementRevision", - "tags", - "moduleName", - "holes", - "submitter", - "moduleContent", - "resolvedHoles" - ], "properties": { - "id": { - "type": "string", - "minLength": 1 - }, - "title": { - "type": "string", - "minLength": 1 - }, - "group": { - "enum": [ - "formalization-evaluation", - "software-verification", - "open-conjectures" - ] - }, - "status": { - "enum": [ - "draft", - "active", - "archived" - ] - }, - "visible": { - "type": "boolean" - }, - "statementRevision": { - "type": "integer", - "minimum": 1 - }, - "tags": { - "type": "array", - "uniqueItems": true, - "items": { - "type": "string", - "minLength": 1 - } - }, - "moduleName": { - "type": "string", - "minLength": 1 - }, - "holes": { - "type": "array", - "minItems": 1, - "items": { - "type": "string", - "minLength": 1 - } - }, - "submitter": { - "type": "string", - "minLength": 1 - }, - "notes": { - "type": [ - "string", - "null" - ] - }, - "source": { - "type": [ - "string", - "null" - ] - }, - "informalSolution": { - "type": [ - "string", - "null" - ] - }, - "moduleContent": { + "workspaceTest": { "type": "string" - }, - "resolvedHoles": { - "type": "array", - "minItems": 1, - "items": { - "$ref": "#/$defs/resolvedHole" - } } - } - }, - "packageDependency": { - "type": "object", - "additionalProperties": false, + }, "required": [ - "name", - "git", - "rev" + "workspaceTest" ], - "properties": { - "name": { - "type": "string", - "pattern": "^[A-Za-z0-9_-]+$" - }, - "git": { - "type": "string", - "minLength": 1 + "additionalProperties": false + }, + "problems": { + "type": "array", + "items": { + "type": "object", + "properties": { + "id": { + "type": "string" + }, + "title": { + "type": "string" + }, + "imports": { + "type": "array", + "items": { + "type": "string" + } + }, + "declarations": { + "type": "array", + "items": { + "type": "object", + "properties": { + "name": { + "type": "string", + "pattern": "^[A-Za-z_][A-Za-z0-9_]*$" + }, + "kind": { + "enum": [ + "def", + "theorem" + ] + }, + "type": { + "type": "string", + "minLength": 1 + }, + "levels": { + "type": "array", + "items": { + "type": "string" + } + } + }, + "required": [ + "name", + "kind", + "type", + "levels" + ], + "additionalProperties": false + } + } }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - } + "required": [ + "id", + "title", + "imports", + "declarations" + ], + "additionalProperties": false } + }, + "enableNanoda": { + "type": "boolean" } - } + }, + "required": [ + "schemaVersion", + "leanToolchain", + "dependencies", + "templates", + "problems", + "enableNanoda" + ], + "additionalProperties": false, + "$schema": "https://json-schema.org/draft/2020-12/schema", + "$id": "request-v2.schema.json", + "title": "Structured package-backed workspace request" } diff --git a/schemas/request-v3.schema.json b/schemas/request-v3.schema.json deleted file mode 100644 index 67bd0a3..0000000 --- a/schemas/request-v3.schema.json +++ /dev/null @@ -1,120 +0,0 @@ -{ - "type": "object", - "properties": { - "schemaVersion": { - "const": 3 - }, - "leanToolchain": { - "type": "string" - }, - "dependencies": { - "type": "array", - "items": { - "type": "object", - "properties": { - "name": { - "type": "string" - }, - "git": { - "type": "string" - }, - "rev": { - "type": "string", - "pattern": "^[0-9a-f]{40}$" - } - }, - "required": [ - "name", - "git", - "rev" - ], - "additionalProperties": false - } - }, - "templates": { - "type": "object", - "properties": { - "workspaceTest": { - "type": "string" - } - }, - "required": [ - "workspaceTest" - ], - "additionalProperties": false - }, - "problems": { - "type": "array", - "items": { - "type": "object", - "properties": { - "id": { - "type": "string" - }, - "title": { - "type": "string" - }, - "imports": { - "type": "array", - "items": { - "type": "string" - } - }, - "declarations": { - "type": "array", - "items": { - "type": "object", - "properties": { - "name": { - "type": "string", - "pattern": "^[A-Za-z_][A-Za-z0-9_]*$" - }, - "kind": { - "enum": [ - "def", - "theorem" - ] - }, - "type": { - "type": "string", - "minLength": 1 - }, - "levels": { - "type": "array", - "items": { - "type": "string" - } - } - }, - "required": [ - "name", - "kind", - "type", - "levels" - ], - "additionalProperties": false - } - } - }, - "required": [ - "id", - "title", - "imports", - "declarations" - ], - "additionalProperties": false - } - } - }, - "required": [ - "schemaVersion", - "leanToolchain", - "dependencies", - "templates", - "problems" - ], - "additionalProperties": false, - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "request-v3.schema.json", - "title": "Structured package-backed workspace request" -} diff --git a/schemas/response-v2.schema.json b/schemas/response-v2.schema.json index 454fb75..3746c7e 100644 --- a/schemas/response-v2.schema.json +++ b/schemas/response-v2.schema.json @@ -1,7 +1,7 @@ { "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "https://leanprover.github.io/lean-eval-generator/response-v2.schema.json", - "title": "LeanEval generator response schema version 2", + "$id": "response-v2.schema.json", + "title": "Structured workspace response", "type": "object", "additionalProperties": false, "required": [ diff --git a/schemas/response-v3.schema.json b/schemas/response-v3.schema.json deleted file mode 100644 index c6ce455..0000000 --- a/schemas/response-v3.schema.json +++ /dev/null @@ -1,46 +0,0 @@ -{ - "$schema": "https://json-schema.org/draft/2020-12/schema", - "$id": "response-v3.schema.json", - "title": "Structured workspace response", - "type": "object", - "additionalProperties": false, - "required": [ - "schemaVersion", - "files" - ], - "properties": { - "schemaVersion": { - "const": 3 - }, - "files": { - "type": "array", - "items": { - "type": "object", - "additionalProperties": false, - "required": [ - "problemId", - "path", - "sha256", - "content" - ], - "properties": { - "problemId": { - "type": "string", - "minLength": 1 - }, - "path": { - "type": "string", - "minLength": 1 - }, - "sha256": { - "type": "string", - "pattern": "^[0-9a-f]{64}$" - }, - "content": { - "type": "string" - } - } - } - } - } -} diff --git a/tests/scripts/packages.py b/tests/scripts/packages.py deleted file mode 100644 index 2d4bba3..0000000 --- a/tests/scripts/packages.py +++ /dev/null @@ -1,105 +0,0 @@ -"""Generate and build an external-package workspace using real Lean metadata.""" - -import hashlib -import json -import os -from pathlib import Path -import subprocess -import tempfile -import tomllib - -from contract import CLI, ROOT, assert_rejected, invoke, problem, request_with - - -def run(args, cwd, env=None): - result = subprocess.run(args, cwd=cwd, env=env, text=True, capture_output=True) - if result.returncode: - raise AssertionError(f"{args}:\n{result.stdout}\n{result.stderr}") - return result.stdout.strip() - - -def package(root, name, module, content): - root.mkdir() - (root / "lakefile.toml").write_text( - f'name = "{name}"\n[[lean_lib]]\nname = "{module}"\n' - ) - (root / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) - (root / f"{module}.lean").write_text(content) - run(["git", "init", "-q"], root) - run(["git", "add", "."], root) - run(["git", "-c", "user.name=Fixture", "-c", "user.email=fixture@example.invalid", - "commit", "-qm", "fixture"], root) - return {"name": name, "git": str(root), "rev": run(["git", "rev-parse", "HEAD"], root)} - - -def main(): - run(["lake", "--wfail", "build"], ROOT) - with tempfile.TemporaryDirectory() as directory: - root = Path(directory) - mathlib = package(root / "mathlib", "mathlib", "Mathlib", "-- Empty fixture library.\n") - dependency = package(root / "support", "fixture_support", "FixtureSupport", - "namespace FixtureSupport\ndef value : Nat := 7\nend FixtureSupport\n") - run(["lake", "build", "FixtureSupport"], root / "support") - context = root / "context" - context.mkdir() - source = "import FixtureSupport\n\ntheorem fixture : FixtureSupport.value = 7 := by sorry\n" - (context / "Fixture.lean").write_text(source) - metadata = context / ".lake/build/lib/lean/Fixture.ilean" - metadata.parent.mkdir(parents=True) - env = dict(os.environ, LEAN_PATH=str(root / "support/.lake/build/lib/lean")) - run(["lake", "env", "lean", "-i", str(metadata), str(context / "Fixture.lean")], ROOT, env) - p = problem() - p["moduleContent"] = source - p["resolvedHoles"][0].update(declarationName="fixture", startLine=3, - startColumn=0, endLine=3, endColumn=len(source.splitlines()[2]), explicitParameters=[]) - payload = request_with(p) - payload.update(schemaVersion=2, contextRoot=str(context), mathlib=mathlib, - leanToolchain=(ROOT / "lean-toolchain").read_text(), dependencies=[dependency]) - result = invoke(json.dumps(payload)) - assert result.returncode == 0, result.stderr - assert invoke(json.dumps(payload)).stdout == result.stdout - response = json.loads(result.stdout) - assert response["schemaVersion"] == 2 - files = {f["path"]: f["content"] for f in response["files"]} - for f in response["files"]: - assert hashlib.sha256(f["content"].encode()).hexdigest() == f["sha256"] - assert tomllib.loads(files["lakefile.toml"])["require"] == [mathlib, dependency] - assert "ChallengeDeps.lean" not in files - for path in ("Challenge.lean", "Submission.lean", "Solution.lean"): - assert "import FixtureSupport" in files[path] - assert "def value" not in files[path] - workspace = root / "workspace" - workspace.mkdir() - for path, content in files.items(): - target = workspace / path - target.parent.mkdir(parents=True, exist_ok=True) - target.write_text(content) - submission = workspace / "Submission.lean" - submission.write_text(submission.read_text().replace("sorry", "rfl")) - run(["lake", "update"], workspace) - run(["lake", "build", "Challenge", "Solution"], workspace) - - # v1 stays strict, including rejection of even an empty new field. - payload["schemaVersion"] = 1 - assert_rejected(payload, "request contains an unknown field") - payload["schemaVersion"] = 2 - for deps, message in [ - ([dependency, dependency], "Duplicate dependency"), - ([dict(dependency, name="mathlib")], "Duplicate dependency"), - ([dict(dependency, rev="main")], "full lowercase commit SHA"), - ([dict(dependency, name="../escape")], "package identifiers"), - ([dict(dependency, extra=True)], "dependency contains an unknown field"), - ]: - payload["dependencies"] = deps - assert_rejected(payload, message) - payload["dependencies"] = [] - v2 = json.loads(invoke(json.dumps(payload)).stdout) - del payload["dependencies"] - payload["schemaVersion"] = 1 - v1 = json.loads(invoke(json.dumps(payload)).stdout) - assert v1["files"] == v2["files"], "Empty v2 dependencies changed legacy rendering" - print("PASS package imports, real metadata, workspace build, pins, and v1 parity") - - -if __name__ == "__main__": - main() diff --git a/tests/scripts/structured.py b/tests/scripts/structured.py index a8acca5..c260288 100644 --- a/tests/scripts/structured.py +++ b/tests/scripts/structured.py @@ -7,7 +7,29 @@ import tomllib from contract import ROOT, invoke -from packages import package, run +import subprocess + +def run(args, cwd, env=None): + result = subprocess.run(args, cwd=cwd, env=env, text=True, capture_output=True) + if result.returncode: + raise AssertionError(f"{args}:\n{result.stdout}\n{result.stderr}") + return result.stdout.strip() + + +def package(root, name, module, content): + root.mkdir() + (root / "lakefile.toml").write_text( + f'name = "{name}"\n[[lean_lib]]\nname = "{module}"\n' + ) + (root / "lean-toolchain").write_text((ROOT / "lean-toolchain").read_text()) + (root / f"{module}.lean").write_text(content) + run(["git", "init", "-q"], root) + run(["git", "add", "."], root) + run(["git", "-c", "user.name=Fixture", "-c", "user.email=fixture@example.invalid", + "commit", "-qm", "fixture"], root) + return {"name": name, "git": str(root), "rev": run(["git", "rev-parse", "HEAD"], root)} + + def main(): @@ -15,7 +37,7 @@ def main(): root = Path(directory) support = package(root / 'support', 'fixture_support', 'FixtureSupport', 'def FixtureSupport.value : Nat := 7\n') - request = {'schemaVersion': 3, 'leanToolchain': (ROOT / 'lean-toolchain').read_text(), + request = {'schemaVersion': 2, 'enableNanoda': True, 'leanToolchain': (ROOT / 'lean-toolchain').read_text(), 'dependencies': [support], 'templates': {'workspaceTest': 'def main : IO Unit := pure ()\n'}, 'problems': [{'id': 'structured', 'title': 'Structured fixtures', 'imports': ['FixtureSupport'], 'declarations': [ @@ -29,7 +51,7 @@ def main(): assert result.returncode == 0, result.stderr assert invoke(json.dumps(request)).stdout == result.stdout response = json.loads(result.stdout) - assert response['schemaVersion'] == 3 + assert response['schemaVersion'] == 2 files = {f['path']: f['content'] for f in response['files']} for f in response['files']: assert hashlib.sha256(f['content'].encode()).hexdigest() == f['sha256'] From e611b55d7097b9de973cbe0cef0f0cfad66dbe92 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+williamjblair@users.noreply.github.com> Date: Tue, 8 Sep 2026 22:35:16 +0100 Subject: [PATCH 5/5] Use portable OpenSSL file digests --- LeanEvalGenerator/Contract.lean | 10 +++++----- README.md | 5 +++++ tests/Context.lean | 6 +++++- 3 files changed, 15 insertions(+), 6 deletions(-) diff --git a/LeanEvalGenerator/Contract.lean b/LeanEvalGenerator/Contract.lean index 491cd7e..9b0a672 100644 --- a/LeanEvalGenerator/Contract.lean +++ b/LeanEvalGenerator/Contract.lean @@ -83,14 +83,14 @@ private def validateRequest (request : GenerateRequest) : IO Unit := do def sha256 (content : String) : IO String := do let out ← IO.Process.output { - cmd := "sha256sum" - args := #["-"] + cmd := "openssl" + args := #["dgst", "-sha256", "-r"] } (some content) if out.exitCode != 0 then - throw <| IO.userError s!"sha256sum failed: {out.stderr.trimAscii.toString}" + throw <| IO.userError s!"openssl SHA-256 failed: {out.stderr.trimAscii.toString}" let digest := (out.stdout.splitOn " ").head!.trimAscii.toString - if digest.length != 64 then - throw <| IO.userError "sha256sum returned an invalid digest." + if digest.length != 64 || !digest.toList.all (fun c => c.isDigit || (c >= 'a' && c <= 'f')) then + throw <| IO.userError "openssl returned an invalid SHA-256 digest." return digest private def metadata (problem : ProblemInput) : LeanEvalGenerator.Core.EvalProblemMetadata := { diff --git a/README.md b/README.md index 9f8b489..15b594a 100644 --- a/README.md +++ b/README.md @@ -48,3 +48,8 @@ remains unchanged; no legacy source-processing path is used for v2 requests. Run `python3 tests/scripts/structured.py` to exercise real Git package resolution, dependent definition holes, polymorphic theorems, deterministic output and invalid request rejection, without any source context or compiler metadata. + +The renderer requires `openssl` on `PATH` for SHA-256 file digests (macOS and Linux); +GNU `sha256sum` is not required. Deploy a reviewed generator revision built with its +pinned Lean toolchain, and record the executable digest alongside the source revision. +The wire schema version identifies the contract, not the executable provenance. diff --git a/tests/Context.lean b/tests/Context.lean index a45ee7f..e4c6d22 100644 --- a/tests/Context.lean +++ b/tests/Context.lean @@ -1,4 +1,4 @@ -import LeanEvalGenerator.Core.Generate +import LeanEvalGenerator.Contract open LeanEvalGenerator.Core @@ -19,6 +19,10 @@ private def expectEq (label actual expected : String) : IO Unit := do s!"{label} mismatch\nexpected:\n{repr expected}\nactual:\n{repr actual}" def main : IO Unit := do + expectEq "empty SHA-256" (← LeanEvalGenerator.sha256 "") + "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" + expectEq "UTF-8 SHA-256" (← LeanEvalGenerator.sha256 "∀ n : ℕ, n = n\n") + "dc24fa7cb94558b9cdf90e20ca6372130a63a26c9c05640a00aab7e75b8d000a" let erdosStyle := "namespace Fixture\nset_option quotPrecheck false\n\n" ++ "local notation \"A\" => { x : Nat | x = 0 }\nvariable (n : Nat)\n" ++