Capture Lean sources once per doctor run

autoform_cli/README.md

@@ -1405,8 +1405,11 @@ graph counts, reference invariants, roadmap audit, and optional local Lean
 targets. It exits zero only when every required check passes. Omitting
 `--lean-root` records an explicit advisory pass; supplying it performs only a
 lexical local-source check, not a Lean build, kernel check, or proof-honesty
-review. The bundled example intentionally exits nonzero while its declared
-coverage still holds `MAPPED` rows.
+review. Only the `lean targets` check reads Lean sources, once. It holds every
+finding that needs the Lean root, including `node-too-large`, and an unusable
+Lean root or unreadable source fails only that check. The bundled example
+intentionally exits nonzero while its declared coverage still holds `MAPPED`
+rows.
 
 This command is strictly read-only and local. It does not invoke Git, GitHub,
 subprocesses, network services, claims, queues, reviews, recovery state,

autoform_cli/doctor.py

@@ -13,7 +13,7 @@
 from dataclasses import asdict, dataclass
 from pathlib import Path, PureWindowsPath
 
-from .audit import AuditFinding, audit_graph
+from .audit import AuditFinding, _lean_findings, audit_graph
 from .graph import GraphValidationError, load_graph
 from .runtime import (
     RUNTIME_AUTHORITY,
@@ -25,15 +25,6 @@
     resolve_runtime_paths,
 )
 
-_LEAN_FINDING_CODES = frozenset(
-    {
-        "invalid-lean-root",
-        "lean-target-deprecated",
-        "lean-target-kind-mismatch",
-        "lean-target-not-found",
-        "unreadable-lean-sources",
-    }
-)
 _CHECK_NAMES = ("blueprint", "runtime", "graph", "references", "audit", "lean targets")
 _QUOTED_STRING = re.compile(r"'(?:\\.|[^'\\])*'|\"(?:\\.|[^\"\\])*\"")
 
@@ -105,13 +96,10 @@ def diagnose_project(
         checks.append(DoctorCheck("graph", False, reason))
         return _blocked_result(checks, "graph validation failed", lean_root=lean_root)
 
-    resolved_lean_root, lean_root_valid = _resolve_lean_root(lean_root)
+    # No runtime field the doctor reports depends on Lean, so the projection
+    # runs without it and the lean targets check is the only Lean capture.
     try:
-        runtime = build_runtime_graph(
-            graph,
-            project_root=paths.project_root,
-            lean_root=resolved_lean_root,
-        )
+        runtime = build_runtime_graph(graph, project_root=paths.project_root)
     except RuntimeProjectionError as error:
         checks.append(DoctorCheck("runtime", False, _issues(error.issues)))
     else:
@@ -146,18 +134,11 @@ def diagnose_project(
         )
     )
 
-    audit = audit_graph(graph, lean_root=resolved_lean_root)
-    lean_findings = tuple(finding for finding in audit.findings if finding.code in _LEAN_FINDING_CODES)
-    if lean_root is not None and not lean_root_valid:
-        lean_findings = (
-            AuditFinding(".", "invalid-lean-root", "Lean root does not exist or is not a directory"),
-            *lean_findings,
-        )
-    roadmap_findings = tuple(finding for finding in audit.findings if finding.code not in _LEAN_FINDING_CODES)
-    checks.append(_finding_check("audit", roadmap_findings, "roadmap audit passed"))
+    checks.append(_finding_check("audit", audit_graph(graph).findings, "roadmap audit passed"))
     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"))
     return _result(checks)
 
@@ -187,17 +168,6 @@ def _finding_check(name: str, findings: tuple[AuditFinding, ...], clean_detail:
     return DoctorCheck(name, False, f"{len(findings)} finding(s): {codes}")
 
 
-def _resolve_lean_root(lean_root: str | Path | None) -> tuple[Path | None, bool]:
-    if lean_root is None:
-        return None, True
-    try:
-        root = Path(lean_root).expanduser().resolve()
-        valid = root.is_dir()
-    except (OSError, RuntimeError, ValueError):
-        return None, False
-    return (root if valid else None), valid
-
-
 def _sanitize_issues(issues: tuple[str, ...], paths: RuntimePaths) -> str:
     sanitized = []
     replacements = (

tests/test_doctor.py

@@ -1,11 +1,12 @@
 from __future__ import annotations
 
+import os
 from pathlib import Path
 
 import pytest
 
+from autoform_cli import _tree_snapshot as tree_snapshot_module
 from autoform_cli.doctor import diagnose_project
-from autoform_cli.lean import LeanSourceError
 
 
 def _article(
@@ -191,26 +192,27 @@ def test_a_deprecated_lean_target_fails_the_lean_targets_check(tmp_path: Path) -
     assert _checks(result)["audit"][0]
 
 
-def test_unreadable_lean_sources_are_a_lean_target_failure(
-    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
-) -> None:
-    project = _clean_project(
-        tmp_path,
-        metadata=(
-            "declaration: theorem",
-            "statement: formalized",
-            "proof: formalized",
-            "lean: Project.result",
-        ),
-    )
+_LEAN_METADATA = (
+    "declaration: theorem",
+    "statement: formalized",
+    "proof: formalized",
+    "lean: Project.result",
+)
+
+
+def _lean_root(tmp_path: Path) -> Path:
     lean_root = tmp_path / "lean"
     lean_root.mkdir()
     (lean_root / "Project.lean").write_text("theorem Project.result : True := trivial\n", encoding="utf-8")
+    return lean_root
 
-    def changed_after_projection(_root):
-        raise LeanSourceError("Lean sources kept changing while they were indexed")
 
-    monkeypatch.setattr("autoform_cli.audit.snapshot_project_sources", changed_after_projection)
+def test_an_unindexable_lean_source_fails_only_the_lean_targets_check(tmp_path: Path) -> None:
+    if not hasattr(os, "mkfifo"):
+        pytest.skip("named pipes are unavailable")
+    project = _clean_project(tmp_path, metadata=_LEAN_METADATA)
+    lean_root = _lean_root(tmp_path)
+    os.mkfifo(lean_root / "F.lean")
 
     result = diagnose_project(project, lean_root=lean_root)
 
@@ -221,6 +223,42 @@ def changed_after_projection(_root):
     assert str(tmp_path) not in result.to_json()
 
 
+def test_an_oversized_node_fails_the_lean_targets_check_not_the_audit(tmp_path: Path) -> None:
+    project = _clean_project(tmp_path)
+    lean_root = tmp_path / "lean"
+    lean_root.mkdir()
+    spans = {f"small{index}": 6 for index in range(5)} | {"big": 420}
+    for name, lines in spans.items():
+        _article(project, f"{name}.md", metadata=(*_LEAN_METADATA[:3], f"lean: Project.{name}"))
+        steps = "".join(f"  -- step {step}\n" for step in range(lines - 2))
+        (lean_root / f"{name}.lean").write_text(f"theorem Project.{name} : True := by\n{steps}  trivial\n", encoding="utf-8")
+
+    result = diagnose_project(project, lean_root=lean_root)
+
+    assert _checks(result)["audit"] == (True, "roadmap audit passed")
+    assert _checks(result)["lean targets"] == (False, "1 finding(s): node-too-large")
+
+
+def test_doctor_captures_the_lean_sources_once(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None:
+    project = _clean_project(tmp_path, metadata=_LEAN_METADATA)
+    lean_root = _lean_root(tmp_path)
+    original = tree_snapshot_module._tree_snapshot_checkpoint
+    captures = 0
+
+    def count_captures(event: str, relative: str) -> None:
+        nonlocal captures
+        original(event, relative)
+        if event == "before-final-verification":
+            captures += 1
+
+    monkeypatch.setattr(tree_snapshot_module, "_tree_snapshot_checkpoint", count_captures)
+
+    result = diagnose_project(project, lean_root=lean_root)
+
+    assert result.clean
+    assert captures == 1
+
+
 def test_runtime_projection_failure_is_reported_without_traceback(tmp_path: Path) -> None:
     project = _clean_project(
         tmp_path,