Keep work impact working beside Lean files whose names are not identifiers

autoform_cli/audit.py

@@ -367,8 +367,12 @@ def _coverage_findings(
 
 
 def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]:
-    root = Path(lean_root).expanduser().resolve()
-    if not root.is_dir():
+    try:
+        root = Path(lean_root).expanduser().resolve()
+        valid = root.is_dir()
+    except (OSError, RuntimeError, ValueError):
+        valid = False
+    if not valid:
         return [
             AuditFinding(
                 ".",

autoform_cli/impact.py

@@ -208,21 +208,24 @@ def project_modules(
     modules: set[str] = set()
     local_modules: set[str] = set()
     for library in libraries:
-        sources = _source_modules(library, snapshot)
+        sources, unimportable = _source_modules(library, snapshot)
         local_modules.update(sources)
+        # A glob also selects modules nothing can import; they are refused
+        # below like any other non-plain name, not dropped.
+        selected = {**unimportable, **sources}
         for glob in library.globs or library.roots:
             base, mode = _glob(glob, library)
             if mode != "+":
                 if base not in sources:
                     raise SkeletonError([f"lean_lib {library.name}: module {base} has no source file"])
                 modules.add(base)
             if mode:
-                descendants = sorted(module for module in sources if module.startswith(f"{base}."))
+                descendants = sorted(module for module in selected if module.startswith(f"{base}."))
                 for module in descendants:
                     if not all(_MODULE_COMPONENT.fullmatch(part) for part in module.split(".")):
                         raise SkeletonError(
                             [
-                                f"lean_lib {library.name}: cannot import {sources[module].as_posix()}; "
+                                f"lean_lib {library.name}: cannot import {selected[module].as_posix()}; "
                                 "the impact probe supports plain module names only"
                             ]
                         )
@@ -232,14 +235,21 @@ def project_modules(
     return tuple(sorted(modules)), tuple(sorted(local_modules))
 
 
-def _source_modules(library: LeanLibrary, snapshot: IndexedSourceSnapshot) -> dict[str, Path]:
-    """Map source modules to captured repository-relative paths for one library."""
+def _source_modules(
+    library: LeanLibrary, snapshot: IndexedSourceSnapshot
+) -> tuple[dict[str, Path], dict[str, Path]]:
+    """Map source modules to captured repository-relative paths for one library.
+
+    The second map holds sources whose module name would contain ``»``. Lake
+    may build them, but no import can name them, so they are never local.
+    """
 
     try:
         prefix = library.src_dir.relative_to(snapshot.index.root)
     except ValueError as exc:
         raise SkeletonError([f"lean_lib {library.name}: srcDir is outside the captured Lean root"]) from exc
     found: dict[str, Path] = {}
+    unimportable: dict[str, Path] = {}
     for path, _data in snapshot.source_files:
         try:
             relative = path.relative_to(prefix) if prefix.parts else path
@@ -249,15 +259,25 @@ def _source_modules(library: LeanLibrary, snapshot: IndexedSourceSnapshot) -> di
             raise SkeletonError(
                 [f"lean_lib {library.name}: source tree exceeds {_MAX_SOURCE_DEPTH} directory levels"]
             )
-        module = ".".join(relative.with_suffix("").parts)
+        # Not with_suffix(""), which rejects the stem `.` of `..lean` on 3.13.
+        parts = (*relative.parts[:-1], relative.stem)
+        # Quote components that are not plain identifiers, so `Basic copy.lean`
+        # is the module `«Basic copy»` that Lean reports.
+        module = ".".join(part if _MODULE_COMPONENT.fullmatch(part) else f"«{part}»" for part in parts)
+        # A component containing `»` has no quoted spelling, so nothing can
+        # import that module. Quoting it anyway keeps a dotted stem one
+        # component, so a glob selects it exactly when Lake does.
+        if any("»" in part for part in parts):
+            unimportable.setdefault(module, path)
+            continue
         if not module:
             continue
         found.setdefault(module, path)
         if len(found) > _MAX_PROJECT_MODULES:
             raise SkeletonError(
                 [f"lean_lib {library.name}: source tree exceeds {_MAX_PROJECT_MODULES} Lean modules"]
             )
-    return found
+    return found, unimportable
 
 
 def _module_source_paths(
@@ -267,7 +287,7 @@ def _module_source_paths(
 
     paths: dict[str, str] = {}
     for library in libraries:
-        for module, path in _source_modules(library, snapshot).items():
+        for module, path in _source_modules(library, snapshot)[0].items():
             paths.setdefault(module, path.as_posix())
     return paths
 
@@ -885,13 +905,13 @@ def _locator(
     """Locate a constant through one captured index, else by its captured module path."""
 
     def locate(record: ConstantRecord) -> tuple[str | None, int | None]:
-        module_path = module_paths.get(record.module)
+        module_path = module_paths.get(_name_key(record.module))
         declaration = snapshot.index.find(record.user_name or record.name)
         if declaration is not None and module_path in (None, declaration.path.as_posix()):
             return declaration.path.as_posix(), declaration.line
         return module_path, None
 
-    module_paths = _module_source_paths(libraries, snapshot)
+    module_paths = {_name_key(module): path for module, path in _module_source_paths(libraries, snapshot).items()}
     return locate
 
 

autoform_cli/lean.py

@@ -895,8 +895,12 @@ def build_linker(
     A supplied source snapshot never inherits a live Git ref; callers must bind
     that ref explicitly if they want permalinks.
     """
-    requested_root = directory_binding.lexical_absolute_path(lean_root)
-    resolved_root = requested_root.resolve()
+    try:
+        requested_root = directory_binding.lexical_absolute_path(lean_root)
+        resolved_root = requested_root.resolve()
+    except RuntimeError as error:
+        # An unknown ~user, or before Python 3.13 a symbolic link loop.
+        raise LeanSourceError("Lean root cannot be resolved") from error
     remapped_exclusions = tuple(
         _remap_resolved_root_exclusion(requested_root, resolved_root, value)
         for value in exclude_roots

autoform_cli/skeleton.py

@@ -1453,7 +1453,7 @@ def run_probe(
 
     lake = shutil.which("lake")
     if lake is None:
-        raise SkeletonError(["lake is not on PATH; a built Lean project is required to extract skeletons"])
+        raise SkeletonError([f"lake is not on PATH; {_probe_purpose(label)} requires a built Lean project"])
     if not (lean_root / "lake-manifest.json").is_file():
         raise SkeletonError(
             [f"lake-manifest.json is missing; run `lake build` before {_probe_purpose(label)}"]
@@ -2047,7 +2047,11 @@ def extract_skeletons(
         graph = load_graph(blueprint_dir)
     except GraphValidationError as exc:
         raise SkeletonError(exc.issues) from exc
-    root = Path(lean_root).expanduser().resolve()
+    try:
+        root = Path(lean_root).expanduser().resolve()
+    except RuntimeError as error:
+        # An unknown ~user, or before Python 3.13 a symbolic link loop.
+        raise SkeletonError([f"Lean root {lean_root} cannot be resolved: {error}"]) from error
     graph_snapshot = _graph_snapshot(graph)
     control_snapshot = _project_control_snapshot(root)
     libraries = lean_libraries(root)

tests/test_cli.py

@@ -3,6 +3,8 @@
 import json
 from pathlib import Path
 
+import pytest
+
 from autoform_cli.__main__ import main
 from autoform_cli.runtime import load_runtime_graph
 
@@ -69,6 +71,41 @@ def test_doctor_cli_returns_failure_without_traceback(tmp_path: Path, capsys) ->
     }
 
 
+def _symlink_loop(tmp_path: Path) -> str:
+    loop = tmp_path / "la"
+    try:
+        loop.symlink_to(tmp_path / "lb")
+        (tmp_path / "lb").symlink_to(loop)
+    except OSError:
+        pytest.skip("symbolic links are unavailable")
+    return str(loop)
+
+
+def _unknown_home(tmp_path: Path) -> str:
+    root = "~autoform-no-such-user/lean"
+    try:
+        Path(root).expanduser()
+    except RuntimeError:
+        return root
+    pytest.skip("this platform expands an unknown ~user")
+
+
+@pytest.mark.parametrize("lean_root", [_symlink_loop, _unknown_home])
+def test_lean_root_commands_report_an_unresolvable_root_without_traceback(tmp_path: Path, capsys, lean_root) -> None:
+    blueprint = str(_clean_blueprint(tmp_path))
+    root = lean_root(tmp_path)
+
+    # expanduser() raises RuntimeError for an unknown ~user, as resolve() does
+    # for a loop before Python 3.13; 3.13 returns the loop path, so check fails
+    # later, when it reads the sources.
+    assert main(["check", blueprint, "--lean-root", root]) == 1
+    assert capsys.readouterr().out.startswith("error: Lean sources could not be indexed")
+    assert main(["audit", blueprint, "--lean-root", root]) == 1
+    assert "error: .: invalid-lean-root: Lean root does not exist or is not a directory\n" in capsys.readouterr().out
+    assert main(["skeleton", blueprint, "--lean-root", root]) == 2
+    assert capsys.readouterr().err.startswith("error: ")
+
+
 def test_audit_cli_reports_clean_human_output(tmp_path: Path, capsys) -> None:
     blueprint = _clean_blueprint(tmp_path)
 

tests/test_impact.py

@@ -880,7 +880,6 @@ def test_probe_failures_name_the_impact_probe(
 
 
 def test_impact_probe_freshness_messages_never_mention_skeletons(tmp_path: Path, monkeypatch) -> None:
-    monkeypatch.setattr("autoform_cli.skeleton.shutil.which", lambda executable: "/bin/lake")
     monkeypatch.setattr(
         "autoform_cli.skeleton._run_bounded_command",
         lambda command, **kwargs: subprocess.CompletedProcess(command, 3, stdout="", stderr="Demo is out of date"),
@@ -892,6 +891,11 @@ def issues(label: str | None) -> tuple[str, ...]:
             skeleton.run_probe(probe, tmp_path, **({} if label is None else {"label": label}))
         return caught.value.issues
 
+    monkeypatch.setattr("autoform_cli.skeleton.shutil.which", lambda executable: None)
+    no_lake = "lake is not on PATH;"
+    assert issues("impact probe") == (f"{no_lake} running the impact probe requires a built Lean project",)
+    assert issues(None) == (f"{no_lake} extracting skeletons requires a built Lean project",)
+    monkeypatch.setattr("autoform_cli.skeleton.shutil.which", lambda executable: "/bin/lake")
     missing = "lake-manifest.json is missing; run `lake build` before"
     assert issues("impact probe") == (f"{missing} running the impact probe",)
     assert issues(None) == (f"{missing} extracting skeletons",)
@@ -977,6 +981,19 @@ def test_project_modules_select_from_captured_files_not_empty_directory_metadata
     assert project_modules([_library(src, "Demo.*")], snapshot) == (("Demo",), ("Demo",))
 
 
+def test_project_modules_read_a_dotted_file_stem_as_one_component(tmp_path: Path) -> None:
+    src = _sources(tmp_path, "Demo", "Demo.Foo")
+    # Lake names these Demo.«Foo.Bar» and Demo.«Foo.x»y», not submodules of Demo.Foo.
+    for name in ("Foo.Bar.lean", "Foo.x»y.lean"):
+        (tmp_path / "Demo" / name).write_text("", encoding="utf-8")
+    snapshot = snapshot_project_sources(tmp_path)
+
+    assert project_modules([_library(src, "Demo.Foo.*")], snapshot) == (
+        ("Demo.Foo",),
+        ("Demo", "Demo.Foo", "Demo.«Foo.Bar»"),
+    )
+
+
 @pytest.mark.parametrize(
     ("glob", "message"),
     [
@@ -986,12 +1003,18 @@ def test_project_modules_select_from_captured_files_not_empty_directory_metadata
         ("Demo.Missing.*", "module Demo.Missing has no source file"),
         ("Demo.Missing.+", "the Lake configuration selects no modules"),
         ("Demo.Odd.+", r"cannot import .*bad-name\.lean"),
+        # Lake builds this one as Demo.«Foo», which `import Demo.«Foo»` cannot name.
+        ("Demo.Quoted.+", r"cannot import .*«Foo»\.lean"),
+        ("Demo.Unquotable.+", r"cannot import .*x»y\.lean"),
         ("Demo.Empty.+", "the Lake configuration selects no modules"),
     ],
 )
 def test_project_modules_fail_closed(tmp_path: Path, glob: str, message: str) -> None:
     src = _sources(tmp_path, "Demo", "Demo.Odd.Fine")
     (tmp_path / "Demo" / "Odd" / "bad-name.lean").write_text("", encoding="utf-8")
+    for name in ("Quoted/«Foo».lean", "Unquotable/x»y.lean"):
+        (tmp_path / "Demo" / name).parent.mkdir()
+        (tmp_path / "Demo" / name).write_text("", encoding="utf-8")
     (tmp_path / "Demo" / "Empty").mkdir()
     snapshot = snapshot_project_sources(tmp_path)
 
@@ -1403,6 +1426,43 @@ def test_helpers_are_located_by_source_name_in_their_module_s_file(tmp_path: Pat
     ]
 
 
+def test_unselected_source_with_a_quoted_module_name_stays_local(tmp_path: Path, monkeypatch, capsys) -> None:
+    project = _blueprint_project(tmp_path, "Demo")
+    lean_root = _stub_lean_root(tmp_path)
+    (lean_root / "Demo").mkdir()
+    # A Finder duplicate the library's roots never select.
+    (lean_root / "Demo" / "Basic copy.lean").write_text("", encoding="utf-8")
+    (lean_root / "Demo" / "α.lean").write_text("", encoding="utf-8")
+    # Python 3.13's with_suffix("") rejects this stem; Lean names it Demo.«.».
+    (lean_root / "Demo" / "..lean").write_text("", encoding="utf-8")
+    # Nothing can import a module whose name has no quoted spelling.
+    (lean_root / "Demo" / "x»y.lean").write_text("", encoding="utf-8")
+    calls = _stub_probe(
+        monkeypatch,
+        [
+            *_STUB_RECORDS,
+            _payload("Demo.copied", module="Demo.«Basic copy»", type_uses=["Demo.base"]),
+            # Lean prints this component unquoted; it is still the same module.
+            _payload("Demo.greek", module="Demo.α", type_uses=["Demo.base"]),
+        ],
+    )
+
+    code = cli.main(["work", "impact", _BASE_ID, str(project), "--lean-root", str(lean_root), "--json"])
+
+    output = capsys.readouterr()
+    assert code == 0, output.err
+    # The probe imports only the selected root but counts the quoted module as
+    # local, and the module's constants are located by its source file.
+    (call,) = calls
+    assert str(call["probe"]).startswith("import Demo\n-- Autoform impact probe.")
+    assert 'Name.str (Name.str (Name.anonymous) "Demo") "Basic copy"' in str(call["probe"])
+    assert 'Name.str (Name.str (Name.anonymous) "Demo") "."' in str(call["probe"])
+    assert "x»y" not in str(call["probe"])
+    helpers = {helper["name"]: helper["path"] for helper in json.loads(output.out)["helpers"]}
+    assert helpers["Demo.copied"] == "Demo/Basic copy.lean"
+    assert helpers["Demo.greek"] == "Demo/α.lean"
+
+
 def _rewrite_base(project: Path) -> None:
     metadata = [f"article_id: {_BASE_ID}", "declaration: definition", "statement: formalized", "lean: Demo.base"]
     _write_article(project, "base.md", metadata=metadata, title="Base, revised")