diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d088967..7704d8f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -37,5 +37,8 @@ jobs: - name: Check versioned JSON contract run: python3 tests/scripts/contract.py + - name: Check quoted module and declaration paths + run: lake build test_module_paths && lake env .lake/build/bin/test_module_paths + - name: Check Python test harnesses run: python3 -m py_compile tests/scripts/*.py diff --git a/LeanEvalGenerator/Core/Generate.lean b/LeanEvalGenerator/Core/Generate.lean index f374956..9f8c293 100644 --- a/LeanEvalGenerator/Core/Generate.lean +++ b/LeanEvalGenerator/Core/Generate.lean @@ -191,14 +191,14 @@ def extractOne (root : System.FilePath) (entry : EvalProblemMetadata) (hole : St /-! ## Source paths -/ def moduleSourcePath (root : System.FilePath) (moduleName : String) : System.FilePath := Id.run do - let parts := moduleName.splitOn "." + let parts := splitNameComponents moduleName let mut path := root for p in parts do path := path / p return path.addExtension "lean" def ileanPath (root : System.FilePath) (moduleName : String) : System.FilePath := Id.run do - let parts := moduleName.splitOn "." + let parts := splitNameComponents moduleName let mut path := root / ".lake" / "build" / "lib" / "lean" for p in parts do path := path / p @@ -864,8 +864,8 @@ def containsIdentifier (haystack needle : String) : Bool := Id.run do return false def lastComponentStr (name : String) : String := - match (name.splitOn ".").getLast? with - | some s => s + match (splitNameComponents name).back? with + | some s => renderNameComponents #[s] | none => name /-- Word boundary at codepoint index `i`: index is past-the-end, at position @@ -2006,10 +2006,10 @@ def derivedHelperOpens (helperNames : Std.HashSet String) : Array String := Id.r let mut opens : Array String := #[] let mut seen : Std.HashSet String := {} for name in helperNames.toList.mergeSort do - let parts := name.splitOn "." - if parts.length ≤ 1 then continue - for count in [1:parts.length] do - let prefix' := ".".intercalate (parts.take count) + let parts := splitNameComponents name + if parts.size ≤ 1 then continue + for count in [1:parts.size] do + let prefix' := renderNameComponents (parts.extract 0 count) if seen.contains prefix' then continue opens := opens.push s!"_root_.{prefix'}" seen := seen.insert prefix' @@ -2330,9 +2330,9 @@ private def renderWorkspaceMultiHole (root : System.FilePath) (entry : EvalProbl -- `Foo.bar.baz` from being silently accepted because some unrelated -- `Foo` happens to be declared in the same module. let hasKeptHelperParent : String → Bool := fun n => - let parts := n.splitOn "." - (List.range (parts.length - 1)).any fun i => - let p := ".".intercalate (parts.take (i + 1)) + let parts := splitNameComponents n + (List.range (parts.size - 1)).any fun i => + let p := renderNameComponents (parts.extract 0 (i + 1)) helperNames.contains p && declNameSet.contains p -- A helper with no `.ilean` span of its own was never written down: it is an -- auto-generated companion of a declaration that *was*. `deriving` emits its diff --git a/LeanEvalGenerator/Core/Markers.lean b/LeanEvalGenerator/Core/Markers.lean index 9feb8d9..57e2840 100644 --- a/LeanEvalGenerator/Core/Markers.lean +++ b/LeanEvalGenerator/Core/Markers.lean @@ -1,6 +1,7 @@ import Lake.Toml import Lake.Util.Message import Lean +import LeanEvalGenerator.Core.Names open Lean open Lean.Parser @@ -41,7 +42,7 @@ components, so `LeanEval.Foo.Bar` is `LeanEval/Foo/Bar.lean` and never `LeanEval/Foo.Bar.lean`. The inventory and extractor executables resolve the same field the same way; the two must agree or they address different files. -/ def parseModuleName (text : String) : Name := - text.splitOn "." |>.foldl Name.str .anonymous + parseHierarchicalName text /-- Walk up from `dir` searching for the manifest directory `manifests/problems/`. Returns the directory itself if found. -/ diff --git a/LeanEvalGenerator/Core/Names.lean b/LeanEvalGenerator/Core/Names.lean new file mode 100644 index 0000000..dedb1ab --- /dev/null +++ b/LeanEvalGenerator/Core/Names.lean @@ -0,0 +1,45 @@ +import Lean + +namespace LeanEvalGenerator.Core + +set_option autoImplicit false + +/-- Split a rendered Lean hierarchical name into its semantic components. + +Dots inside a guillemet-quoted identifier are data, not separators, and the +outer guillemets are not part of the resulting component. Lean permits any +character except `»` inside a quoted component, including another `«` and a +newline, so only the first closing `»` changes the scanner back to the ordinary +state. Callers use module and declaration names already accepted by Lean; this +helper is not a replacement identifier parser. -/ +def splitNameComponents (text : String) : Array String := Id.run do + let mut parts : Array String := #[] + let mut current := "" + let mut quoted := false + for character in text.toList do + if quoted then + if character == '»' then + quoted := false + else + current := current.push character + else if character == '«' then + quoted := true + else if character == '.' then + parts := parts.push current + current := "" + else + current := current.push character + parts.push current + +def nameFromComponents (parts : Array String) : Lean.Name := + parts.foldl Lean.Name.str .anonymous + +def parseHierarchicalName (text : String) : Lean.Name := + nameFromComponents (splitNameComponents text) + +/-- Render semantic components back to unambiguous Lean syntax. In particular, +a component containing `.` regains its required guillemets. -/ +def renderNameComponents (parts : Array String) : String := + (nameFromComponents parts).toString + +end LeanEvalGenerator.Core diff --git a/Tests/ModulePaths.lean b/Tests/ModulePaths.lean new file mode 100644 index 0000000..89c1197 --- /dev/null +++ b/Tests/ModulePaths.lean @@ -0,0 +1,29 @@ +import LeanEvalGenerator.Core.Generate + +open LeanEvalGenerator.Core + +private def assertEqual (label actual expected : String) : IO Unit := do + unless actual == expected do + throw <| IO.userError s!"{label}: got {actual.quote}, expected {expected.quote}" + +def main : IO Unit := do + let root : System.FilePath := "/tmp/lean-eval-generator-context" + let quoted := "FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture" + let components := splitNameComponents quoted + unless components == + #["FormalConjectures", "Arxiv", "0912.2382", "CurlingNumberConjecture"] do + throw <| IO.userError s!"quoted components were split incorrectly: {components}" + assertEqual "source path" (moduleSourcePath root quoted).toString + "/tmp/lean-eval-generator-context/FormalConjectures/Arxiv/0912.2382/CurlingNumberConjecture.lean" + assertEqual "ilean path" (ileanPath root quoted).toString + "/tmp/lean-eval-generator-context/.lake/build/lib/lean/FormalConjectures/Arxiv/0912.2382/CurlingNumberConjecture.ilean" + assertEqual "plain path" (moduleSourcePath root "LeanEval.Fixture").toString + "/tmp/lean-eval-generator-context/LeanEval/Fixture.lean" + assertEqual "quoted keyword" (moduleSourcePath root "Foo.«match».Bar").toString + "/tmp/lean-eval-generator-context/Foo/match/Bar.lean" + assertEqual "inner opening guillemet" + (moduleSourcePath root "Foo.«a«b.c».Bar").toString + "/tmp/lean-eval-generator-context/Foo/a«b.c/Bar.lean" + assertEqual "rendered prefix" + (renderNameComponents #["Foo", "a.b"]) "Foo.«a.b»" + assertEqual "last component" (lastComponentStr "Foo.«a.b»") "«a.b»" diff --git a/lakefile.toml b/lakefile.toml index 5fd3860..6fea374 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,3 +10,7 @@ name = "LeanEvalGenerator" [[lean_exe]] name = "lean-eval-generator" root = "LeanEvalGenerator.Main" + +[[lean_exe]] +name = "test_module_paths" +root = "Tests.ModulePaths" diff --git a/tests/scripts/contract.py b/tests/scripts/contract.py index 980819b..c278495 100644 --- a/tests/scripts/contract.py +++ b/tests/scripts/contract.py @@ -1,12 +1,13 @@ -#!/usr/bin/env python3 """Small dependency-free checks for the CLI transport contract.""" from __future__ import annotations import json import subprocess +import tempfile from pathlib import Path +from golden import module_path as golden_module_path ROOT = Path(__file__).resolve().parents[2] CLI = ROOT / ".lake/build/bin/lean-eval-generator" @@ -127,7 +128,29 @@ def main() -> int: hole_unknown["problems"][0]["resolvedHoles"][0]["unexpected"] = True assert_rejected(hole_unknown, "resolvedHole contains an unknown field") - print("PASS malformed, version, and schema-invariant errors stay off stdout") + with tempfile.TemporaryDirectory() as directory: + context = Path(directory) + module_name = "Arxiv.«0912.2382».Fixture" + module_content = "theorem fixture : True := by sorry\n" + module_path = context / "Arxiv" / "0912.2382" / "Fixture.lean" + assert golden_module_path(context, module_name) == module_path + module_path.parent.mkdir(parents=True) + module_path.write_text(module_content, encoding="utf-8") + quoted = problem() + quoted["moduleName"] = module_name + quoted["moduleContent"] = module_content + quoted["resolvedHoles"][0]["module"] = module_name + quoted["resolvedHoles"][0]["declarationName"] = f"{module_name}.fixture" + payload = request_with(quoted) + payload["contextRoot"] = str(context) + result = invoke(json.dumps(payload)) + assert result.returncode == 1 + assert result.stdout == "" + expected_ilean = context / ".lake/build/lib/lean/Arxiv/0912.2382/Fixture.ilean" + assert str(expected_ilean) in result.stderr, result.stderr + assert "Arxiv/«0912/2382»" not in result.stderr + + print("PASS schema errors stay off stdout and quoted source/ilean paths resolve") return 0 diff --git a/tests/scripts/golden.py b/tests/scripts/golden.py index ad254f9..0679f38 100644 --- a/tests/scripts/golden.py +++ b/tests/scripts/golden.py @@ -1,4 +1,3 @@ -#!/usr/bin/env python3 """Byte-for-byte parity tests against checked-in LeanEval workspaces.""" from __future__ import annotations @@ -7,9 +6,9 @@ import json import subprocess import sys -import tomllib from pathlib import Path +import tomllib PACKAGE_ROOT = Path(__file__).resolve().parents[2] FIXTURE_IDS = json.loads( @@ -23,8 +22,7 @@ def run(command: list[str], *, cwd: Path, stdin: str | None = None) -> str: cwd=cwd, input=stdin, text=True, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, + capture_output=True, check=False, ) if result.returncode != 0: @@ -35,8 +33,30 @@ def run(command: list[str], *, cwd: Path, stdin: str | None = None) -> str: return result.stdout +def module_components(module: str) -> list[str]: + """Mirror Lean quoted-component semantics for fixture source paths.""" + parts: list[str] = [] + current: list[str] = [] + quoted = False + for character in module: + if quoted: + if character == "»": + quoted = False + else: + current.append(character) + elif character == "«": + quoted = True + elif character == ".": + parts.append("".join(current)) + current = [] + else: + current.append(character) + parts.append("".join(current)) + return parts + + def module_path(root: Path, module: str) -> Path: - return root.joinpath(*module.split(".")).with_suffix(".lean") + return root.joinpath(*module_components(module)).with_suffix(".lean") def mathlib_pin(root: Path) -> dict[str, str]: