diff --git a/autoform_cli/README.md b/autoform_cli/README.md index c28694dd..9c827bfd 100644 --- a/autoform_cli/README.md +++ b/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, diff --git a/autoform_cli/doctor.py b/autoform_cli/doctor.py index 52f43b97..b932587b 100644 --- a/autoform_cli/doctor.py +++ b/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 = ( diff --git a/tests/test_doctor.py b/tests/test_doctor.py index 5e67f662..884fe0c6 100644 --- a/tests/test_doctor.py +++ b/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,