Fix quoted Lean module path resolution

.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

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

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. -/

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

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»"

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"

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
 
 

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]: