Skip to content

Capture Lean sources once per doctor run - #236

Merged
Deicyde merged 5 commits into
mainfrom
fix/doctor-single-lean-capture
Oct 13, 2026
Merged

Capture Lean sources once per doctor run#236
Deicyde merged 5 commits into
mainfrom
fix/doctor-single-lean-capture

Conversation

@Deicyde

@Deicyde Deicyde commented Oct 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

  • autoform doctor --lean-root captured the Lean sources twice (for the runtime projection and for the audit) and never compared the two. A source the capture refused, such as a named pipe or an edit during every attempt, failed runtime and marked graph, references and audit as not checked even when the roadmap was fine.
  • The runtime capture fed nothing the doctor shows: it reports only the runtime's schema, authority, source revision and counts, and none of them read Lean (source_revision ignores Lean, see runtime: build_runtime_graph labels stale node data with the current files' source_revision #59).
  • The doctor now projects the runtime without Lean, runs audit_graph without Lean for the audit check, and takes the lean targets findings from audit._lean_findings, its only capture.
  • autoform_cli/doctor.py is +6/-36: _LEAN_FINDING_CODES, the step that split audit findings by code, and the doctor's own _resolve_lean_root are gone. The README's doctor paragraph says which check reads Lean. runtime.py and audit.py are unchanged.

Behavior changes

  • A Lean capture failure fails only lean targets, as 1 finding(s): unreadable-lean-sources; runtime, graph, references and audit still judge the roadmap. autoform audit --lean-root prints the reason. On Windows, which has no descriptor traversal, doctor --lean-root now fails only lean targets the same way.
  • node-too-large reports under lean targets instead of audit. It needs --lean-root, and audit_graph without a Lean root never produces it. The exit code is unchanged; the check lines and JSON change.

Tests

All in tests/test_doctor.py; each fails at main ae2db51:

  • test_an_unindexable_lean_source_fails_only_the_lean_targets_check replaces test_unreadable_lean_sources_are_a_lean_target_failure, which patched the audit's capture and never saw the runtime one. A FIFO named F.lean fails only lean targets, with no host path in the JSON. At main, runtime fails.
  • test_an_oversized_node_fails_the_lean_targets_check_not_the_audit: at main, audit fails with node-too-large and lean targets passes.
  • test_doctor_captures_the_lean_sources_once counts the capture's before-final-verification checkpoint: 2 at main, 1 now. It also kills passing lean_root to build_runtime_graph again.

Overlap with open PRs

MAIN_REF=upstream/main pr_conflicts.sh on this branch merged with main ae2db51, conflicts it adds:

Validation

At d37e50e:

  • test_doctor, test_runtime, test_audit, test_work, test_cli: 155 passed on Python 3.13 and 3.10.
  • This tests/test_doctor.py on main ae2db51: 3 failed (the tests above), 13 passed.
  • Full non-Lean suite: 2203 passed, 70 skipped, 1 xfailed. ruff check autoform_cli servers tests: clean.

@Deicyde
Capture Lean sources once per doctor run
47c671b 
diagnose_project handed the Lean root to build_runtime_graph and to
audit_graph, and each captured the sources on its own. A source that
could not be captured (a named pipe, an unreadable folder, an edit
during the capture) made the runtime projection raise first, so the
runtime check carried the reason while graph, references and audit were
marked as not run although the Markdown roadmap was fine, and lean
targets said it was not checked. When only the second capture failed,
lean targets reported a bare unreadable-lean-sources code instead. The
two captures were never compared, so the projection and the Lean target
checks could also judge different source sets in one run (B-F5,
contracts-note-1).

The doctor now resolves the root once, captures it once with
snapshot_project_sources, and shares that capture: build_runtime_graph
takes it through a new keyword-only lean_index and audit_graph through
a new keyword-only lean_snapshot. Callers that pass lean_root keep the
previous behavior, and passing both raises TypeError. audit's Lean
target evaluation is split from its capture into _lean_target_findings,
which takes the whole IndexedSourceSnapshot because the deprecation
check reads the captured source files. A capture failure is reported
once, by lean targets, with index_failure_message's reason, and the
other checks still judge the roadmap; when the runtime projection fails
for a Markdown reason, _blocked_result takes the capture failure as its
lean targets check, so lean targets still names it.
unreadable-lean-sources is dropped from the doctor's Lean finding codes
because the audit can no longer return it to the doctor.

The doctor section of autoform_cli/README.md now says the sources are
captured once and where a capture failure is reported
(README-doctor-indexes-twice). The test that pinned a failure of the
audit's second capture is rewritten as a real edit during every capture
attempt.
@meta-cla meta-cla Bot added the CLA Signed This label is managed by the Meta Open Source bot. label Oct 13, 2026
@Deicyde
Merge main c070c36 into doctor single Lean capture
aa508cb 
Main reworked tests/test_audit.py imports (os, Graph and Node for the implementation note tests). The conflict is resolved as the union with this branch's shutil and snapshot_project_sources imports.
This was referenced Oct 13, 2026
Merged
Merged
Open
@Deicyde
Pass Lean captures in instead of adding a second Lean parameter
05c541b 
47c671b gave build_runtime_graph a lean_index keyword and audit_graph a
lean_snapshot keyword next to their lean_root keywords, with a TypeError
when both were passed. That left two ways to hand each function Lean
sources, and the doctor still sorted the audit's findings into roadmap
and Lean findings by code.

build_runtime_graph now takes only lean_index; load_runtime_graph, the one
caller that passes a Lean root, resolves and captures it before projecting.
audit_graph is unchanged: the doctor runs it without a Lean root and calls
_lean_target_findings on its own capture, so _LEAN_FINDING_CODES and the
code filter go away. An invalid Lean root is now the same lean targets
failure as an unreadable source, so it is also reported when the runtime
projection fails instead of "not checked".

Tests: the runtime and audit tests that pinned the two-keyword API are
removed (load_runtime_graph and audit_blueprint tests cover the capture
paths). The doctor test that edited sources at an internal checkpoint is
removed; the named-pipe test covers a capture failure failing only lean
targets. The blocked-path test now also covers a missing Lean root.
@Deicyde
Run the doctor's runtime projection without Lean
a483df7 
The previous commit handed the doctor's one Lean capture to both the
runtime projection and the lean targets check. The runtime half did
nothing visible: the doctor reports only the runtime's schema,
authority, source revision and counts, and none of them read Lean
(source_revision ignores Lean, see #59). Its one Lean-dependent
refusal, a source path escaping the Lean root, cannot come from a
capture, whose paths are relative and whose entry names are checked.
A mutant passing no Lean index survived every touched test.

The doctor now projects the runtime without Lean and takes the lean
targets findings from audit._lean_findings, so the audit's capture is
the doctor's only one. That reverts runtime.py and audit.py to main,
drops the doctor's own root resolution and its blocked-path Lean
check, and leaves the blocked path saying "not checked because runtime
projection failed" as on main. An unreadable source now reports
"1 finding(s): unreadable-lean-sources" like every other finding;
autoform audit --lean-root gives the reason.

node-too-large needs the Lean root, so it now reports under lean
targets instead of audit. The earlier rework made that move without
saying so; a doctor test now pins it and the README states it.
@Deicyde
Keep the doctor test Lean root flat as on main
d37e50e 
The nested Project/ folder only fixed the path in the capture failure text, which the doctor no longer prints. The flat layout from main is enough for the FIFO and capture-count tests.
@Deicyde

Deicyde commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Review at d37e50e

Verdict: Merge-ready. On main, diagnose_project captures the Lean tree twice: once inside build_runtime_graph and once inside audit_graph. A tree the capture refuses (a FIFO, a tree that keeps changing, any --lean-root on Windows) makes the runtime projection raise, so the doctor fails runtime and reports graph, references, audit and lean targets as not checked, even when the roadmap is fine. This PR builds the runtime projection and the audit check without Lean (autoform_cli/doctor.py:101-102) and calls _lean_findings once for lean targets, so only that check fails and the roadmap checks still run. Nothing the doctor prints is lost: the runtime and graph lines never read Lean targets, and audit_graph adds Lean findings only through _lean_findings (autoform_cli/audit.py:305-306), so the split is exact and the hand-kept _LEAN_FINDING_CODES list can go. Each of the three new tests fails on main by trace, and the PR body reports the same from a run on main.

Optional

  • autoform_cli/doctor.py:142: lean targets now also carries node-too-large, so the clean detail "all asserted local Lean targets resolve" covers only part of the check. Something like "local Lean targets resolve and are in size" would match. Nit, confirmed by reading.
  • When the capture fails, lean targets prints only unreadable-lean-sources (or invalid-lean-root), because _finding_check prints codes only. The reason is in the finding's detail, which is free of host paths. Printing it when the single finding has path . would save a trip to autoform audit --lean-root. Main behaves the same when only the audit capture fails. Cheap.
  • doctor.py imports the private audit._lean_findings. There is precedent (autoform_cli/render.py:43) and ruff passes; renaming it to lean_findings is optional.
  • The commit message says an escaping source path "cannot come from a capture". That is not quite true: the snapshot allows : in names (autoform_cli/_tree_snapshot.py:1366-1374), and _is_portable_relative_path (autoform_cli/runtime.py:444-452) treats C:/F.lean as absolute, so on POSIX a directory named C: still makes autoform work list --lean-root raise. Confirmed by trace; negligible, since Lean module paths cannot contain :. No change needed here.

Landing

Decision for the maintainer

  • node-too-large moves from the doctor's audit line to lean targets. The exit code is unchanged; the check lines and JSON output change. It is documented in the README and pinned by a test, and no caller parses doctor check lines for it. Options: accept the move, or keep size findings under audit. Recommendation: accept, because the finding needs the Lean root and lean targets is the only check that reads it.

This was a static review: no tests were run locally. CI at this head: all 9 checks pass.

Posted by PR swarm: PR Swarm Lead

This was referenced Oct 13, 2026
Merged
Merged
Merged
Merged
@Deicyde
Deicyde marked this pull request as ready for review October 13, 2026 17:21
@Deicyde
Deicyde merged commit abae767 into main Oct 13, 2026
9 checks passed
@Deicyde
Deicyde deleted the fix/doctor-single-lean-capture branch October 13, 2026 17:21
@Deicyde Deicyde mentioned this pull request Oct 13, 2026
Merged
Deicyde added a commit that referenced this pull request Oct 13, 2026
@Deicyde
Merge main abae767 into Lean root errors
6312c25 
#236 made the lean targets check the doctor's only Lean capture and dropped the
runtime projection's Lean root, so this branch's _resolve_lean_root helper and
its audit split no longer apply. The lean targets branch now calls
resolve_lean_root itself: an unusable root reports the reason, otherwise the
resolved root goes to _lean_findings, as the recipe in #236's body describes.
Deicyde added a commit that referenced this pull request Oct 13, 2026
@Deicyde
Merge main 2eae76d into the explorer branch
7a8f594 
Resolves the conflicts the merged PRs' descriptions point at:
- runtime: resolve the Lean root with resolve_lean_root before the
  name-filtered index (#231).
- render: keep #235's no-capture path around the name-filtered capture,
  and warn when code links are skipped.
- graph pages: count each chapter's formalization targets as #250 does,
  with the explorer's collapsed-node wording.
- lean: take #265's section forms and mutual scopes. #269 removed
  tolerated_links, so the generation revision now filters the omitted
  entries that editor lock links leave.
- tests: take #236's doctor test; keep the targeted-index tests beside
  #265's scope test.
@Deicyde Deicyde mentioned this pull request Oct 14, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

CLA Signed This label is managed by the Meta Open Source bot.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Deicyde