Name why a Lean root is unusable instead of indexing nothing or crashing

autoform_cli/audit.py

@@ -26,10 +26,12 @@
 from .lean import (
     _DECLARATION,
     Declaration,
+    LeanSourceError,
     SourceIndex,
     _without_lean_comments,
     declaration_names,
     index_failure_message,
+    resolve_lean_root,
     snapshot_project_sources,
 )
 from .markdown import article_parts as _article_parts
@@ -423,18 +425,9 @@ def _coverage_findings(
 
 def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]:
     try:
-        root = Path(lean_root).expanduser().resolve()
-        valid = root.is_dir()
-    except (OSError, RuntimeError, ValueError):
-        valid = False
-    if not valid:
-        return [
-            AuditFinding(
-                ".",
-                "invalid-lean-root",
-                "Lean root does not exist or is not a directory",
-            )
-        ]
+        root = resolve_lean_root(lean_root)
+    except LeanSourceError as error:
+        return [AuditFinding(".", "invalid-lean-root", str(error))]
 
     findings: list[AuditFinding] = []
     try:

autoform_cli/doctor.py

@@ -15,6 +15,7 @@
 
 from .audit import AuditFinding, _lean_findings, audit_graph
 from .graph import GraphValidationError, load_graph
+from .lean import LeanSourceError, resolve_lean_root
 from .runtime import (
     RUNTIME_AUTHORITY,
     RUNTIME_SCHEMA,
@@ -138,8 +139,13 @@ def diagnose_project(
     if lean_root is None:
         checks.append(DoctorCheck("lean targets", True, "not checked; no Lean root supplied"))
     else:
-        lean_findings = tuple(_lean_findings(graph, lean_root))
-        checks.append(_finding_check("lean targets", lean_findings, "all asserted local Lean targets resolve"))
+        try:
+            root = resolve_lean_root(lean_root)
+        except LeanSourceError as error:
+            checks.append(DoctorCheck("lean targets", False, str(error)))
+        else:
+            lean_findings = tuple(_lean_findings(graph, root))
+            checks.append(_finding_check("lean targets", lean_findings, "all asserted local Lean targets resolve"))
     return _result(checks)
 
 

autoform_cli/impact.py

@@ -20,7 +20,7 @@
 
 from . import skeleton
 from ._tree_snapshot import TreeSnapshotError
-from .lean import IndexedSourceSnapshot, bind_project_source_snapshot
+from .lean import IndexedSourceSnapshot, LeanSourceError, bind_project_source_snapshot, resolve_lean_root
 from .runtime import load_runtime_graph
 from .skeleton import LeanLibrary, SkeletonError, _lean_name, _lean_name_parts, lean_libraries
 from .work import work_context
@@ -848,7 +848,10 @@ def revision_impact(
     if not names:
         raise ImpactError(f"{revised.id} names no lean: declaration; pass --declaration NAME")
 
-    root = Path(lean_root).expanduser().resolve()
+    try:
+        root = resolve_lean_root(lean_root)
+    except LeanSourceError as error:
+        raise ImpactError(str(error)) from error
     controls = _project_controls(root)
     with bind_project_source_snapshot(root) as (bound_sources, source_snapshot):
         libraries = lean_libraries(root)

autoform_cli/lean.py

@@ -12,6 +12,7 @@
 
 from __future__ import annotations
 
+import errno
 import hashlib
 import json
 import os
@@ -148,15 +149,44 @@ def index_failure_message(error: OSError) -> str:
     return "Lean sources could not be indexed"
 
 
+def resolve_lean_root(lean_root: str | Path) -> Path:
+    """Resolve *lean_root* to the directory it names.
+
+    Raises :class:`LeanSourceError` naming why the root cannot be used, for
+    example when it does not exist or lies under a folder that cannot be
+    searched.
+    """
+
+    try:
+        root = directory_binding.lexical_absolute_path(lean_root).resolve()
+        metadata = os.stat(root)
+    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
+    except (FileNotFoundError, NotADirectoryError) as error:
+        raise LeanSourceError("Lean root does not exist or is not a directory") from error
+    except PermissionError as error:
+        raise LeanSourceError("permission denied while resolving the Lean root") from error
+    except (OSError, ValueError) as error:
+        if getattr(error, "errno", None) == errno.ELOOP:
+            # Python 3.13 and later resolve a symbolic link loop without raising.
+            raise LeanSourceError("Lean root cannot be resolved") from error
+        raise LeanSourceError("Lean root cannot be inspected") from error
+    if not stat.S_ISDIR(metadata.st_mode):
+        raise LeanSourceError("Lean root does not exist or is not a directory")
+    return root
+
+
 def index_project(
     root: str | Path, *, exclude_roots: Iterable[str | Path] = ()
 ) -> SourceIndex:
-    """Scan ``*.lean`` beneath *root* and index declarations by full name."""
+    """Scan ``*.lean`` beneath *root* and index declarations by full name.
+
+    Raises :class:`LeanSourceError` when the root cannot be used or its
+    sources cannot be read.
+    """
+    root_path = resolve_lean_root(root)
     requested_root = directory_binding.lexical_absolute_path(root)
-    root_path = requested_root.resolve()
-    if not root_path.is_dir():
-        digest = hashlib.sha256(b"autoform-lean-source-index/v1\0").hexdigest()
-        return SourceIndex(root=root_path, declarations={}, source_digest=digest)
     remapped_exclusions = tuple(
         _remap_resolved_root_exclusion(requested_root, root_path, value)
         for value in exclude_roots
@@ -908,12 +938,8 @@ def build_linker(
     A supplied source snapshot never inherits a live Git ref; callers must bind
     that ref explicitly if they want permalinks.
     """
-    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
+    resolved_root = resolve_lean_root(lean_root)
+    requested_root = directory_binding.lexical_absolute_path(lean_root)
     remapped_exclusions = tuple(
         _remap_resolved_root_exclusion(requested_root, resolved_root, value)
         for value in exclude_roots
@@ -1276,6 +1302,7 @@ def _git_environment() -> dict[str, str]:
     "index_failure_message",
     "index_project",
     "project_source_revision",
+    "resolve_lean_root",
     "snapshot_project_sources",
     "strip_lean_comments",
     "verify_repository_snapshot",

autoform_cli/render.py

@@ -42,11 +42,13 @@
 from .coverage import COVERAGE_DISPOSITIONS, CoverageSummary, load_coverage
 from .graph import Graph, GraphValidationError, Node, _implementation_note_issues, load_graph
 from .lean import (
+    LeanSourceError,
     SourceLinker,
     declaration_names,
     detect_ref,
     detect_repository_url,
     index_failure_message,
+    resolve_lean_root,
     snapshot_project_sources,
     verify_repository_snapshot,
 )
@@ -335,7 +337,10 @@ def render_site(
     # The repository root, not the vault's parent. A blueprint nested at
     # <repo>/docs/blueprint would otherwise be described as <repo>/blueprint,
     # and every generated permalink would 404.
-    repo_root = Path(lean_root).expanduser().resolve() if lean_root is not None else blueprint.parent
+    try:
+        repo_root = resolve_lean_root(lean_root) if lean_root is not None else blueprint.parent
+    except LeanSourceError as error:
+        raise PublicationError([index_failure_message(error)]) from error
     # Everything below reads a private copy of the captured bytes. The copy keeps
     # the blueprint's place in the repository, so a path below the copy's root is
     # the repository path it had when render read the vault.

autoform_cli/runtime.py

@@ -14,7 +14,7 @@
 from urllib.parse import unquote, urlsplit
 
 from .graph import Graph, load_graph, roadmap_symlink_issues
-from .lean import declaration_names, index_failure_message, index_project
+from .lean import LeanSourceError, declaration_names, index_failure_message, index_project, resolve_lean_root
 from .status import derive, is_definition
 
 RUNTIME_SCHEMA = "autoform-runtime/v3"
@@ -315,9 +315,10 @@ def build_runtime_graph(
     statuses = derive(graph)
     lean_index = None
     if lean_root is not None:
-        root = Path(lean_root).expanduser().resolve()
-        if not root.is_dir():
-            raise RuntimeProjectionError(["Lean root does not exist or is not a directory"])
+        try:
+            root = resolve_lean_root(lean_root)
+        except LeanSourceError as error:
+            raise RuntimeProjectionError([str(error)]) from error
         try:
             lean_index = index_project(root)
         except OSError as error:

autoform_cli/search.py

@@ -12,7 +12,7 @@
 from pathlib import Path
 
 from .graph import load_graph
-from .lean import SourceIndex, index_failure_message, index_project
+from .lean import LeanSourceError, SourceIndex, index_failure_message, index_project, resolve_lean_root
 from .markdown import ArticleParts, article_parts, visible_prose
 from .runtime import RuntimeNode, build_runtime_graph, resolve_runtime_paths
 
@@ -444,9 +444,10 @@ def _fields(
 def _lean_index(lean_root: str | Path | None) -> SourceIndex | None:
     if lean_root is None:
         return None
-    root = Path(lean_root).expanduser().resolve()
-    if not root.is_dir():
-        raise SearchError("Lean root does not exist or is not a directory")
+    try:
+        root = resolve_lean_root(lean_root)
+    except LeanSourceError as error:
+        raise SearchError(str(error)) from error
     try:
         return index_project(root)
     except OSError as error:

autoform_cli/skeleton.py

@@ -41,10 +41,12 @@
     MANAGED_OUTPUT_SCHEMAS,
     PACKET_SCHEMA,
     PASSAGE_SCHEMA,
+    LeanSourceError,
     SourceIndex,
     declaration_names,
     index_failure_message,
     index_project,
+    resolve_lean_root,
 )
 
 SKELETON_SCHEMA = "autoform-skeleton/v4"
@@ -2061,7 +2063,10 @@ def extract_skeletons(
         graph = load_graph(blueprint_dir)
     except GraphValidationError as exc:
         raise SkeletonError(exc.issues) from exc
-    root = resolve_lean_root(lean_root)
+    try:
+        root = resolve_lean_root(lean_root)
+    except LeanSourceError as error:
+        raise SkeletonError([str(error)]) from error
     activity = "skeletons were being extracted"
     inputs = snapshot_inputs(graph, root)
     libraries = lean_libraries(root)
@@ -2139,16 +2144,6 @@ def check_inputs_unchanged(
     return current_graph
 
 
-def resolve_lean_root(lean_root: str | Path) -> Path:
-    """The absolute Lean project root, or a ``SkeletonError`` saying why there is none."""
-
-    try:
-        return 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
-
-
 def select_lean_targets(
     graph: Graph, node_ids: tuple[str, ...] | None = None
 ) -> tuple[list[tuple[Node, tuple[str, ...]]], list[tuple[Node, tuple[str, ...]]], str]:
@@ -3069,7 +3064,6 @@ def _where(item: TrustedDeclaration) -> str:
     "parse_probe_output",
     "path_of",
     "render_probe",
-    "resolve_lean_root",
     "run_probe",
     "select_lean_targets",
     "snapshot_inputs",

autoform_cli/unused_hypotheses.py

@@ -26,7 +26,7 @@
 from pathlib import Path
 
 from .graph import GraphValidationError, load_graph
-from .lean import index_failure_message, index_project
+from .lean import LeanSourceError, index_failure_message, index_project, resolve_lean_root
 from .skeleton import (
     DEFAULT_PROBE_TIMEOUT,
     PROBE_OUTPUT_ENV,
@@ -38,7 +38,6 @@
     check_inputs_unchanged,
     lean_libraries,
     locate_declaration,
-    resolve_lean_root,
     run_probe,
     select_lean_targets,
     snapshot_inputs,
@@ -161,7 +160,10 @@ def find_unused_hypotheses(
         graph = load_graph(blueprint_dir)
     except GraphValidationError as exc:
         raise SkeletonError(exc.issues) from exc
-    root = resolve_lean_root(lean_root)
+    try:
+        root = resolve_lean_root(lean_root)
+    except LeanSourceError as error:
+        raise SkeletonError([str(error)]) from error
     _, selected, _ = select_lean_targets(graph, node_ids)
     # An answer is about the inputs it was computed from. If they change while
     # Lean runs, it may describe a state that no longer exists.

tests/test_cli.py

@@ -3,8 +3,6 @@
 import json
 from pathlib import Path
 
-import pytest
-
 from autoform_cli.__main__ import main
 from autoform_cli.runtime import load_runtime_graph
 
@@ -71,41 +69,6 @@ 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_doctor.py

@@ -285,7 +285,7 @@ def test_invalid_lean_root_is_a_sanitized_lean_failure(tmp_path: Path) -> None:
 
     assert not result.clean
     assert _checks(result)["runtime"][0]
-    assert _checks(result)["lean targets"] == (False, "1 finding(s): invalid-lean-root")
+    assert _checks(result)["lean targets"] == (False, "Lean root does not exist or is not a directory")
     assert str(tmp_path) not in result.to_json()
 
     loop = tmp_path / "lean-loop"
@@ -295,7 +295,11 @@ def test_invalid_lean_root_is_a_sanitized_lean_failure(tmp_path: Path) -> None:
         pytest.skip("symbolic links are unavailable")
     loop_result = diagnose_project(project, lean_root=loop)
     assert len(loop_result.checks) == 6
-    assert _checks(loop_result)["lean targets"] == (False, "1 finding(s): invalid-lean-root")
+    if os.name == "nt":
+        # Windows reports a symbolic link loop by its own error code.
+        assert not _checks(loop_result)["lean targets"][0]
+    else:
+        assert _checks(loop_result)["lean targets"] == (False, "Lean root cannot be resolved")
     assert str(tmp_path) not in loop_result.to_json()