Skip to content

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

Merged
Deicyde merged 8 commits into
mainfrom
fix/lean-root-errors
Oct 13, 2026
Merged

Name why a Lean root is unusable instead of indexing nothing or crashing#231
Deicyde merged 8 commits into
mainfrom
fix/lean-root-errors

Conversation

@Deicyde

@Deicyde Deicyde commented Oct 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Summary

Root Reason
missing, a file, or under a file Lean root does not exist or is not a directory
under a folder without search permission permission denied while resolving the Lean root
~name for an unknown user, or a symbolic link loop Lean root cannot be resolved

Behavior changes

Exit codes are unchanged. Messages:

  • check, render: "Lean sources could not be indexed: " instead of "directory tree cannot be inspected safely: ..." (and, on Python 3.13, "must not be a symbolic link" for a loop). render with an unknown ~user root gives the reason instead of a RuntimeError traceback.
  • audit: invalid-lean-root carries the reason instead of "does not exist or is not a directory" for every failure.
  • search, work list/context/impact: the reason instead of "project, blueprint, or Lean root path cannot be read" or "does not exist".
  • skeleton, unused-hypotheses: the root is checked before the Lake files, so a missing root gives the reason instead of "no lakefile.toml or lakefile.lean in ".
  • doctor: the "lean targets" detail is the reason instead of "1 finding(s): invalid-lean-root".
  • API: lean.resolve_lean_root is new; index_project raises LeanSourceError for an unusable root; skeleton.resolve_lean_root leaves skeleton.__all__.

Tests

  • tests/test_lean_root.py (new, 15 cases): the helper with each of five roots (missing, file, under a mode-000 folder, unknown ~user, self-loop) gives exactly its reason; index_project gives the same reason for a missing and an unknown ~user root; one case per command path through main() (check, search, work list, work impact, unused-hypotheses, audit) asserts exit code, exact output and no host path, plus check and render with an unknown ~user root. These replace test_lean_sources.py::test_missing_project_keeps_the_empty_index_contract.
  • Updated: the render, skeleton, doctor and unused-hypotheses tests that pin those commands' messages. Removed: Keep work impact working beside Lean files whose names are not identifiers #182's prefix-only test_cli.py::test_lean_root_commands_report_an_unresolvable_root_without_traceback, now covered exactly.
  • Fail before: every new or changed test fails on main (the new file cannot import resolve_lean_root; render with an unknown ~user root raises RuntimeError there). Swapping resolve_lean_root and lexical_absolute_path in build_linker fails check-unknown-home. Dropping the helper's RuntimeError, PermissionError, ELOOP or S_ISDIR branch fails exactly one helper case; expanding the root before the helper in index_project fails the unknown ~user case.
  • Skips: the permission case on Windows and as root, the unknown-home and loop cases on Windows, the loop case without symbolic links.

Overlap with open PRs

Main abae767 is merged in. Its doctor.py conflict with #236 is resolved by the recipe in #236's body: the lean targets check calls resolve_lean_root and reports its reason, otherwise passes the resolved root to _lean_findings. MAIN_REF=upstream/main pr_conflicts.sh at fd7b518, conflicts this branch adds:

Validation

At fd7b518:

  • The 13 touched test files: 784 passed, 39 skipped, 1 xfailed on Python 3.13 and 3.10.20.
  • Full non-Lean suite on macOS, Python 3.13: 2304 passed, 71 skipped, 1 xfailed.
  • ruff check autoform_cli servers tests: clean.
  • With Lean on PATH, at 46a4bb0: test_unused_hypotheses_in_a_built_project, test_the_probe_reads_a_built_project and the four skeleton lakefile tests pass.

@Deicyde
Refuse an unusable Lean root by name instead of indexing nothing
906b030 
Commands resolved --lean-root with Path.resolve() and then asked
Path.is_dir(), each in its own way. is_dir() re-raises EACCES on Python
3.10 to 3.13 and returns False for it on 3.15 (3.14 was not checked), so
a root under a folder that cannot be searched gave render --ref the bare
"Lean sources could not be indexed", made audit call the root missing,
and on newer Pythons made index_project return an empty index, so every
lean: name read as missing (F-F5, NEW-AUDIT-TRACEBACK, NEW-PY314-EMPTY).
render with an explicit --ref indexed through index_project, whose empty
index for a missing or non-directory root published the site with 0 code
links and exit 0 (B-F4). #182 typed the RuntimeError that an unknown
~user or (before Python 3.13) a symbolic link loop raises, in
build_linker, audit and skeleton only; render still crashed with a
traceback on such a root, audit described it as missing, and on Python
3.13 a loop reached the source capture.

The root cause is that the root check was a boolean pre-check repeated in
every caller, with no reason attached, in front of an index function that
answers a missing root with an empty index. lean.resolve_lean_root now
resolves the root once, stats it, and raises LeanSourceError with the
reason, never a host path: "Lean root does not exist or is not a
directory", "permission denied while resolving the Lean root", or #182's
"Lean root cannot be resolved" for an unknown ~user or a symbolic link
loop on every Python version. build_linker, render's explicit root,
audit, the runtime projection (work) and search call it, and then
capture with snapshot_project_sources, which fails closed, so no command
can reach the empty index if the root vanishes after the check. Audit
keeps its invalid-lean-root code and now gives the reason as its text.
index_project keeps its empty index for a root that does not exist or is
not a directory, which a test pins as API, and raises the typed error
for every other reason.

The explicit-ref alias swap test hooks the capture the linker now calls.
The runtime failure test patches the capture the runtime now calls. The
#182 command test expects the audit reason instead of the missing-root
text.
@Deicyde
Check the Lean root before Lake files and show its reason in doctor
f72f18c 
The previous commit gave commands one place to resolve a Lean root, but
three commands still kept their own check (F-F9, C5).

skeleton and work impact read lakefile.toml and lakefile.lean before
looking at the root, so a missing root was "no lakefile.toml or
lakefile.lean in <host path>" and a root under an unsearchable folder a
lakefile stat error naming the host path (F-F9's main trigger); #182
covered only the unknown ~user and pre-3.13 loop cases in skeleton, with
their own message. Both now call resolve_lean_root first, and skeleton
captures its sources with snapshot_project_sources, like the other
commands, instead of index_project's empty index.

doctor turned every failure into invalid-lean-root and showed only that
code, so an unsearchable parent, an unknown home and a loop all read as
"1 finding(s): invalid-lean-root", the same as a missing root. Its lean
targets check now shows the reason as its detail.

The Lean root matrix gains skeleton, work impact and doctor. It covers
check, audit and skeleton for an unknown ~user and a symbolic link loop
with exact messages, so #182's weaker command test is removed. The
skeleton test that expected the lakefile message for a missing root and
the doctor test that expected the bare code now expect the reason; on
Windows the doctor loop case asserts only a failing check with no host
path, because Windows reports the loop by its own error code.
@meta-cla meta-cla Bot added the CLA Signed This label is managed by the Meta Open Source bot. label Oct 13, 2026
@Deicyde Deicyde mentioned this pull request Oct 13, 2026
Merged
@Deicyde
Merge main c070c36 into Lean root errors
87476b1 
Main gained #198, which added skeleton.resolve_lean_root for the same job
as this branch's lean.resolve_lean_root, and #188, which folded the
skeleton input re-checks into check_inputs_unchanged.

Keep one helper, as promised on #198: skeleton.resolve_lean_root is
dropped, and extract_skeletons and unused_hypotheses call
lean.resolve_lean_root and wrap its LeanSourceError as a SkeletonError
with the same reason. unused-hypotheses now names an unusable root the
way skeleton does, with no host path, instead of the lakefile message or
the raw Python error.

extract_skeletons takes #188's snapshot_inputs and check_inputs_unchanged,
and both those re-checks and unused_hypotheses capture with
snapshot_project_sources instead of index_project, so no command reaches
the empty index of a root that vanished after the check.

tests/test_lean_root.py gains an unused-hypotheses row for all five
roots, and #198's test for an unknown home now pins the shared reason.
This was referenced Oct 13, 2026
Merged
Merged
Merged
Draft
@Deicyde
Merge main ae2db51 into Lean root errors
52e45d9 
Takes #165 (transactional render publication), which conflicted in
render.py: render no longer builds a linker, it resolves the Lean root
and captures it with snapshot_project_sources. The resolution keeps
#165's structure and resolves the explicit root with resolve_lean_root
inside a guard, so an unknown ~user or a symbolic link loop is an error
instead of a traceback and every unusable root names its reason.
#165's test_lasting_capture_failures_name_their_cause now expects that
reason for a missing root.
@Deicyde
Make index_project fail closed and test each root path once
5fe3967 
index_project answered a missing or non-directory root with an empty
index. That contract is what let render --ref publish a site with no
code links, and the branch worked around it by moving every caller to
snapshot_project_sources and splitting the root check into
_inspect_lean_root so the contract could survive with no caller left.

index_project now calls resolve_lean_root, so it fails closed like the
capture it wraps, and the empty-index contract and its test are gone.
The runtime projection, search, skeleton, unused-hypotheses and the
explicit-ref linker keep calling index_project as they do on main, and
the three monkeypatch retargets that followed the call swap are
reverted. resolve_lean_root is one function again: it resolves and
stats the root in one guarded step instead of passing a tuple through
_inspect_lean_root and _lean_root_failure.

The 44-case command by root matrix becomes one test of the helper's
five reasons plus one case per command code path, each with a root that
command misreported at main (check, search, work list, work impact,
unused-hypotheses, audit). render, skeleton and doctor were already
pinned by their own changed tests. index_project's unsearchable-root
test is covered by the helper test; a missing root is pinned by
test_index_project_refuses_a_missing_root.
@Deicyde
Resolve the Lean root before index_project expands it
46a4bb0 
index_project called directory_binding.lexical_absolute_path(root) before
resolve_lean_root(root). lexical_absolute_path expands ~, which raises a raw
RuntimeError for an unknown ~user, so index_project leaked that error instead
of the typed LeanSourceError its docstring promises. build_linker already
called the helper first. Call resolve_lean_root first so the helper decides
every root failure, then compute the lexical path for exclusion remapping.

Pin it by moving the missing-root test next to the unusable_root fixture in
tests/test_lean_root.py and parametrizing it over the missing and unknown-home
cases. The unknown-home case fails at 5fe3967 with RuntimeError.

render caught OSError around resolve_lean_root, although the helper only
raises LeanSourceError and every other call site catches that. Narrow the
catch to LeanSourceError. Behavior does not change.
This was referenced Oct 13, 2026
Merged
Merged
Merged
Merged
@Deicyde

Deicyde commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Review at 46a4bb0

Verdict: Needs small fixes before merge. The PR adds lean.resolve_lean_root and routes every command that takes --lean-root through it, replacing eight separate root resolutions. On main, render --lean-root ~nosuchuser/x dies with a RuntimeError traceback, skeleton and unused-hypotheses report a missing root as a missing lakefile with the absolute host path, and search, work list and doctor print generic messages. After this PR each of these names its cause without a host path, and index_project fails closed instead of returning an empty index; no caller outside autoform_cli uses the old contract. The code is right; the blocker is one ordering that only a deleted test used to pin.

Fixes before merge

  1. Pin the unknown-home ordering for check and render (autoform_cli/lean.py:938-939, tests/test_lean_root.py:109-117). build_linker has to call resolve_lean_root (line 938) before lexical_absolute_path (line 939), because the latter calls expanduser(), which raises a raw RuntimeError for an unknown user. _check catches only OSError and main() has no catch-all. The PR deletes Keep work impact working beside Lean files whose names are not identifiers #182's test_lean_root_commands_report_an_unresolvable_root_without_traceback, which ran check with an unknown ~user root and a link loop; the new main() matrix runs check only with a missing root, and no test runs render with an unknown-home root. So swapping lines 938 and 939 would bring the traceback back and no test would fail, and the render traceback fix listed under "Behavior changes" is also unpinned. Confirmed by a trace of the call path and a grep of tests/ (the mutant was not run). Fix: add pytest.param(["check", "{blueprint}"], "unknown-home", 1, "error: Lean sources could not be indexed: {}\n", id="check-unknown-home") to the matrix, plus one render case through main() with the unknown-home root. Cheap.
  2. PR body names a work next command that does not exist. "work list/next/impact" appears twice. The work subcommands that take --lean-root are list, context and impact. Confirmed by reading. Cheap.

Optional

  • autoform_cli/lean.py:171: on Windows with Python 3.13+, Path.resolve() no longer raises for a link loop and os.stat reports winerror 1921 rather than ELOOP, so a loop gives "cannot be inspected" instead of "cannot be resolved". Plausible, from CPython's error mapping; low value since every --lean-root command fails closed on Windows anyway. Fix: also accept getattr(error, "winerror", None) == 1921 in that branch.
  • The Windows job lists its test files explicitly and runs neither tests/test_lean_root.py nor tests/test_doctor.py, so the os.name == "nt" skips and the relaxed doctor assertion are never exercised. If Windows behavior matters here, add tests/test_lean_root.py to that job.

Landing

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
Draft
Draft
Draft
@Deicyde

Deicyde commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Merge readiness: needs small fixes (reviewed at 46a4bb0)

  • CI is green at this head: both Linux test jobs, real Lean (fixture toolchain), and the Windows hardening job.
  • The two fixes from the previous round are in: an unknown ~user root gets the typed error in index_project, and render catches LeanSourceError.
  • Fix 1, confirmed: build_linker must call resolve_lean_root before lexical_absolute_path (lean.py:938-939). This PR deletes Keep work impact working beside Lean files whose names are not identifiers #182's test_lean_root_commands_report_an_unresolvable_root_without_traceback, and nothing replaces it for check or render. I swapped those two lines: build_linker("~autoform-no-such-user/x") raises a raw RuntimeError again, and all 603 tests in the 12 files that reach build_linker still pass. Add a check unknown-home case to the main() matrix in tests/test_lean_root.py, plus one render case.
  • Fix 2: the body says "work list/next/impact" twice, but there is no work next. The work commands that take --lean-root are list, context and impact.

Rebase needed: #236 has merged, so this now conflicts with main in doctor.py, 3 hunks. Use the recipe in #236's body. #235 then gets a one-hunk render.py import conflict: keep LeanSourceError, IndexedSourceSnapshot and SourceIndex.

Caveat: index_project now raises for a missing root instead of returning an empty index. It is a draft, so it needs to be marked ready before merging.

@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
Pin that check and render resolve an unknown-home Lean root first
fd7b518 
build_linker must call resolve_lean_root before lexical_absolute_path, and
render must resolve the root before anything expands it, because expanduser()
raises a raw RuntimeError for an unknown ~user and neither command catches it.
Removing #182's test_lean_root_commands_report_an_unresolvable_root_without_traceback
left that ordering unpinned: swapping the two lines in build_linker brought the
traceback back and every test still passed (merge-readiness fix 1).

Add check and render cases with an unknown-home root to the main() matrix in
tests/test_lean_root.py, asserting the exit code, the exact reason and no host
path.
This was referenced Oct 13, 2026
Merged
Merged
@Deicyde

Deicyde commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Update: fixes pushed, now ready to merge (fd7b518)

  • Merged main (abae767). The doctor.py conflict with Capture Lean sources once per doctor run #236 is resolved: the lean targets check calls resolve_lean_root and reports its reason.
  • check and render with an unknown ~user root are now pinned in the main() matrix in tests/test_lean_root.py. Swapping the two lines in build_linker fails the check case. Expanding the root before the helper in render fails the render case.
  • The body now says work list/context/impact.
  • CI: all 9 checks pass at fd7b518, and it merges cleanly with main.

Remaining conflict: #235, one import hunk in render.py (keep LeanSourceError, IndexedSourceSnapshot and SourceIndex). It is a draft, so it needs to be marked ready before merging.

@Deicyde
Deicyde marked this pull request as ready for review October 13, 2026 19:16
@Deicyde
Deicyde merged commit e6bcf8a into main Oct 13, 2026
9 checks passed
@Deicyde
Deicyde deleted the fix/lean-root-errors branch October 13, 2026 19:16
Deicyde added a commit that referenced this pull request Oct 13, 2026
@Deicyde
Merge origin/main into feat/import-impact-policy
3c4631e 
Brings in main up to b1b0094, including #248 (package srcDir), #231
(Lean root errors) and #165. Two files conflicted, and every resolution
keeps both sides:

- autoform_cli/impact.py: this branch's claims import and main's
  LeanSourceError and resolve_lean_root import. Main's switch to
  resolve_lean_root merged into _load_impact_evidence, where this
  branch moved revision_impact's body.
- autoform_cli/skeleton.py: lean_libraries computes this branch's root
  artifact directory and main's package srcDir. Library srcDirs are
  relative to the package srcDir, and a package without library
  targets uses the package srcDir and the artifact directory.
@Deicyde Deicyde mentioned this pull request Oct 13, 2026
Merged
Deicyde added a commit that referenced this pull request Oct 13, 2026
@Deicyde
Merge origin/main into cleanup/build-linker-unused-params
eca72ca 
Brings in main up to f169a4d. One hunk conflicted, at the top of
build_linker, because #231 replaced the inline root resolution with
resolve_lean_root. The resolution keeps this branch's one-argument
signature and takes resolve_lean_root, as this PR's description planned.
_remap_resolved_root_exclusion stays: open_project_sources still uses it.
@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 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.
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