Document what stops Lean indexing by Deicyde · Pull Request #234 · facebookresearch/autoform-bot

Deicyde · 2026-10-13T00:34:37Z

Summary

Since Bind Lean source snapshots to filesystem generations #95, Lean indexing fails closed, but the README never says which entries stop it or how to clear a stop.
This adds one paragraph to the Validation section of autoform_cli/README.md: what stops indexing, that the stops apply in every folder under the Lean root, which folder render uses as the Lean root by default, which folders the walk skips, that there is no command-line exclusion, and which names match in any letter case (the skipped folder names, manifest.json, publication.json, .git; not build, and not the .lean suffix, which is exact since Count only the exact .lean suffix as Lean source #232).
What a capture guarantees (root-only retention, the cross-folder gap) is left to Prove Lean capture stability only for Lean inputs, and name what changed #257, which redefines that guarantee and replaces the same README paragraph and module docstring.

Behavior changes

None. One README paragraph (+20 lines).

Tests

No test changes. Each claim was checked by a throwaway probe that builds a Lean root and calls snapshot_project_sources, on main ae2db51 and on #257's head, with the same results. The letter-case sentence was checked against autoform_cli/lean.py and _tree_snapshot.py on main abae767.

Overlap with open PRs

The branch merges cleanly with main abae767. The paragraph sits after the permalink paragraph, away from #257's insertion point after the descriptor paragraph. If #235 lands after this, it should qualify the "render without --lean-root" sentence for hosts without descriptor capture.

Validation

tests/test_search.py and tests/test_skill_examples.py (the tests that read this README): 90 passed on Python 3.13 at 32057cf.
ruff check autoform_cli servers tests: clean.

Since #95, Lean indexing fails closed, but the documentation never said which entries stop it. An unreadable .lean file, a folder that cannot be listed or searched, an unreadable manifest.json in any subfolder, or a .lean symbolic link or special file stops the whole index, including in folders unrelated to Lean (C7, C2, NEW-MANIFEST-UNREADABLE). The .lean suffix and the manifest.json name are matched in any letter case. For render the implicit Lean root is the blueprint's parent, so this reaches folders next to the blueprint, and there is no CLI exclusion. The docs also claimed more than the capture does (C6, B-F1). Docstrings and the CLI README described a capture as one immutable or stable generation, but only the root descriptor is retained: descendants are reopened by name and rechecked by (dev, ino, file type) and their full name list, so coordinated moves across folders between those checks are not detected. The CLI README now lists the stopping entries, the letter-case rule, the remedy (permissions, or moving the entry out of the root or into a skipped folder) and the retention model, and the work impact paragraph no longer claims a retained generation. snapshot_project_sources names the stopping entries. These docstrings no longer call a capture one generation: the _tree_snapshot module docstring, TreeSnapshotError, _TreeChanged, BoundDirectoryTree.capture and bind_directory_tree in _tree_snapshot.py; IndexedSourceSnapshot, BoundProjectSources and bind_project_source_snapshot in lean.py; _captured_source_lines in audit.py; and project_modules in impact.py. Docstrings about the retained root directory itself are accurate and stay. No behavior changes.

Descriptor capture rechecks each descended folder by identity and full name list, so one file moved between two folders three times, timed to the walk, yields an accepted snapshot that no single state had (B-F1). The documentation now discloses this; nothing in the suite exercised it, so a change that closed the gap or widened it would go unnoticed. The test moves Zed/Y.lean to Proj/X.lean just before Zed is first listed, back before final verification, and to Proj/X.lean again just before Zed is relisted for verification, after Proj was verified. The listing hook wraps os.scandir and os.listdir and matches Zed by fstat identity, and every move happens only in the first capture attempt. It is xfail(strict=True) and only its own pytest.fail, reached after all three moves happened and the snapshot lacked the file, counts as the expected failure. If the moves never start, a plain assertion fails. If capture keeps the file or rejects the first attempt partway, the strict XPASS says the pin and the disclosure should go. The fix-round version moved the file after Proj was listed; main's end-of-scan relist rejects that timing and the pin would XPASS, so move 1 now happens at Zed's first listing.

Main gained #165, whose caller-named opaque markers changed the snapshot_project_sources docstring this branch also edits, so the branch no longer merged cleanly. The conflict keeps both sentences; the next commits narrow this branch's scope and update the stop list for #165.

The branch also rewrote what a capture guarantees: a README paragraph and the _tree_snapshot module docstring describing root-only retention and the cross-folder gap, generation wording in seven docstrings and the work impact paragraph, and a strict xfail pinning the three-move mixture. fix/lean-capture-unrelated-churn (#257) changes that guarantee and replaces the same README paragraph and module docstring with its own text, so the two branches conflicted and a reviewer had to read the guarantee twice. The guarantee belongs with the change that redefines it, so this branch drops all of it, including the pin, and keeps only what stays true either way: what stops Lean indexing and how to clear it. The snapshot_project_sources docstring copy of that list goes too; the README is its one home.

Since #165, render passes a publication.json marker to Lean indexing: a folder holding a complete publication manifest is skipped, and an unreadable publication.json below the root stops render's indexing like an unreadable manifest.json does. The stop list predated #165 and named neither, so a render user with an unreadable site manifest had no documented cause or remedy. Name both, and state the letter-case rule once at the end instead of per entry, so the exact-suffix change in #232 narrows one clause. The sentence promising root-relative error paths is dropped; it is not part of what stops indexing, and #237 changes which path errors name.

The stop list sat right after the descriptor paragraph, where #257 inserts its capture-guarantee paragraph, so the two branches conflicted on adjacent insertions. One paragraph later it stays in the Validation section and no open PR edits the lines around it.

The stop-list paragraph said the `.lean` suffix matches in any letter case. That holds on main, but #232 makes the suffix match exactly, so whichever of the two landed second would have left the README wrong. Drop the suffix from the sentence; the file and folder names it lists still match in any letter case except `build`, on main and with #232.

Deicyde · 2026-10-13T17:03:39Z

Review at `359f9f2`

Verdict: Needs one fix before merge. The PR adds one paragraph to the README's Validation section (+18/-0, docs only). It says Lean indexing is all-or-nothing, lists what stops it, and says how to clear a stop. Since #95, an unreadable folder anywhere under the Lean root fails check --lean-root, audit, work impact and render, even when that folder has nothing to do with Lean. Users hit this, and the README never said so. A static trace against main holds up for every claim in the paragraph. The one blocker is the closing letter-case sentence, which turns wrong once #232 makes the .lean suffix exact.

Fixes before merge

Narrow the letter-case sentence (autoform_cli/README.md:915-916). "File and folder names here match in any letter case except build" is true on main, because the .lean suffix is casefolded there (autoform_cli/lean.py:490-495). Count only the exact .lean suffix as Lean source #232 changes that check to an exact match. After Count only the exact .lean suffix as Lean source #232 the sentence tells a reader that Y.LEAN is indexed, and it is not. Plausible, from reading only: the code is fine, and the problem is a README sentence that becomes misleading. Fix: "Folder names and the manifest.json, publication.json and .git names match in any letter case except build; the .lean suffix must match exactly." Cheap.

Optional

autoform_cli/README.md:914: "or, for render, a rendered site" undersells the marker. The comment at autoform_cli/render.py:128 says every site, stage and backup carries publication.json. Consider "a rendered site or a leftover render stage". Plausible, from reading only.
No test on main exercises an unreadable manifest.json in a subfolder, or an unreadable publication.json through render. Two chmod 0 cases would pin the two stops this paragraph documents. Better done as a follow-up than in this PR.
An empty folder that can be listed but not searched does not stop indexing, because there is no child to stat. "cannot be listed or searched" slightly over-claims, but the gap is harmless. Plausible, from reading only.

Landing

Still a draft; mark it ready. GitHub reports it mergeable, and the head is main plus this one paragraph.
A textual merge of this README against the current heads of Prove Lean capture stability only for Lean inputs, and name what changed #257, Label statement approvals by the repository's code-owner review policy #219, Add verified statement-review bundles #75, Show statement review on the site #217, Harden card publication and review record #218, Render without code links where Lean sources cannot be captured #235, Capture Lean sources once per doctor run #236, Audit recursive definitions, not their compiled copies #247 and Stop refusing the _unsafe_rec copy of every recursive definition #253 is clean in every case.
Merge order: after Count only the exact .lean suffix as Lean source #232, so the narrowed sentence can state the exact suffix, and before Render without code links where Lean sources cannot be captured #235. Render without code links where Lean sources cannot be captured #235 then has to qualify this PR's "render without --lean-root uses the blueprint's parent folder as the Lean root" sentence (autoform_cli/README.md:909-910) for hosts without descriptor capture. If this PR merges before Count only the exact .lean suffix as Lean source #232 instead, Count only the exact .lean suffix as Lean source #232 should carry the narrowing.
If Prove Lean capture stability only for Lean inputs, and name what changed #257 lands first, reread the stop list against it. From reading Prove Lean capture stability only for Lean inputs, and name what changed #257's diff, an unreadable marker still raises there, so the list stays true (plausible).

Decision for the maintainer

This PR used to include docstrings and a strict-xfail test describing what a capture guarantees: retention at the root only, and cross-folder moves that go undetected. That half was dropped, and the author intends it to live in Prove Lean capture stability only for Lean inputs, and name what changed #257, which redefines the guarantee. Options: keep the disclosure in Prove Lean capture stability only for Lean inputs, and name what changed #257, drop it, or open an issue to close the gap itself. The old deferral waited on Scan descriptor trees in a closure and fold repeated tree snapshot checks #188, which has merged, so nothing blocks the issue route now. Recommendation: let Prove Lean capture stability only for Lean inputs, and name what changed #257 record the disclosure, and open an issue only if you want the gap closed rather than documented.

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

Deicyde · 2026-10-13T17:32:01Z

Merge readiness: needs one small fix (reviewed at 359f9f2)

CI is green at this head: both Linux test jobs, real Lean (fixture toolchain), and the Windows hardening job. The two tests that read the README pass.
Docs only (README +18). Every claim in the paragraph holds on main.
Fix: the last sentence, "File and folder names here match in any letter case except build", reads as covering the .lean names the paragraph mentions. Count only the exact .lean suffix as Lean source #232 has merged, so a Y.LEAN file is no longer indexed and the sentence would mislead as soon as this lands. Make it say which names fold (folder names, manifest.json, publication.json, .git) and that the .lean suffix must match exactly. The earlier reviews on Count only the exact .lean suffix as Lean source #232 and on this PR both flag it.

Merge order: any time after the fix. It merges cleanly with current main (abae767) and with every open sibling, including #257, which edits a different README paragraph.

It is a draft, so it needs to be marked ready before merging.

The closing sentence of the Lean stop list said file and folder names match in any letter case except build. Read next to the .lean entries the paragraph lists, it claimed A.LEAN is indexed. Since #232 the walk compares the .lean suffix exactly, so the sentence misled. Name the names that fold (the skipped folder names, manifest.json, publication.json and .git), keep build as the lowercase-only exception, and state that the .lean suffix must match exactly.

Deicyde · 2026-10-13T18:35:31Z

Update: fix pushed, now ready to merge (32057cf)

The last sentence now says which names match in any letter case (the skipped folder names, manifest.json, publication.json, .git; build must be lowercase), and that the .lean suffix must match exactly. Checked against main after Count only the exact .lean suffix as Lean source #232.
CI: all 9 checks pass at 32057cf, and it merges cleanly with main.

Follow-ups for whichever lands second: #270 removes lake-packages, so drop that word from this stop list; if this lands before #235, qualify the "render without --lean-root uses the blueprint's parent folder" sentence for hosts without descriptor capture. It is a draft, so it needs to be marked ready before merging.

#237 sends every by-name lookup through _lookup, which blames the folder, and every refused open, read or readlink through _access_denied. The ten _tree_snapshot.py hunks keep this branch's vanish handlers and named changes and call #237's helpers inside them. _PermissionDenied is not an OSError, so the handlers pass it through. The symbolic link branch is split: a refused readlink goes through _access_denied and the confirming lookup through _lookup. _read_file keeps this branch's keyword-only relative=. Final verification's verify_child_directory and the recorded names in verify_selected_directory use the same helpers, so anything the scan recorded is blamed by #237's rule. Refusals in the selected-mode relist and in _require_no_inputs stay changes and are never accepted; the retry's scan names the folder if the refusal lasts. test_folder_refused_to_a_selected_recheck_is_not_accepted[lookup] now expects "permission denied: site" instead of the pathless message. #268 removed expected_children, so this branch's selected-mode guard in capture_directory_descriptor (an undefined name after the merge) and test_selected_capture_refuses_expected_children go. #269 removed tolerated_links. The lean.py hunks keep this branch's lines without it; the include filter still skips .#*.lean lock links. #234 added a README stop list. This branch's capture paragraph moves after it, refers to "a folder the walk skips" instead of repeating the marker list, and says non-.lean files may change instead of "ignored unless they are .lean files", which contradicted the skipped lock links.

facebookresearch#234 documented the folders the Lean walk skips and listed lake-packages. facebookresearch#270 removed that name from _IGNORED_DIRECTORIES, so a folder named lake-packages is now indexed and moving an entry there no longer clears a stop. Remove the name from the list so the README matches lean.py and nothing in the repository names lake-packages.

Deicyde added 2 commits October 12, 2026 20:14

meta-cla Bot added the CLA Signed This label is managed by the Meta Open Source bot. label Oct 13, 2026

Deicyde added 5 commits October 13, 2026 04:12

Deicyde changed the title ~~Document what stops Lean indexing and what a capture guarantees~~ Document what stops Lean indexing Oct 13, 2026

This was referenced Oct 13, 2026

Count only the exact .lean suffix as Lean source #232

Merged

Make the tooling-folder test exercise the ignore set #233

Merged

This was referenced Oct 13, 2026

Render without code links where Lean sources cannot be captured #235

Merged

Fix roadmap loading, Lean index edge cases and undecodable JSON #212

Merged

Deicyde mentioned this pull request Oct 13, 2026

Stop ignoring the pre-.lake lake-packages folder in Lean capture #270

Merged

Deicyde marked this pull request as ready for review October 13, 2026 19:14

Deicyde merged commit 7908058 into main Oct 13, 2026
9 checks passed

Deicyde deleted the docs/lean-capture-limits branch October 13, 2026 19:15

Deicyde mentioned this pull request Oct 13, 2026

Drop lake-packages from the README Lean stop list #282

Merged

Navigation Menu

Repository navigation

Document what stops Lean indexing - #234

Document what stops Lean indexing#234
Deicyde merged 8 commits into
mainfrom
docs/lean-capture-limits

Deicyde commented Oct 13, 2026 •

edited

Loading

Uh oh!

Deicyde commented Oct 13, 2026

Uh oh!

Deicyde commented Oct 13, 2026

Uh oh!

Deicyde commented Oct 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

Deicyde commented Oct 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Behavior changes

Tests

Overlap with open PRs

Validation

Uh oh!

Deicyde commented Oct 13, 2026

Review at 359f9f2

Fixes before merge

Optional

Landing

Decision for the maintainer

Uh oh!

Deicyde commented Oct 13, 2026

Uh oh!

Deicyde commented Oct 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Deicyde commented Oct 13, 2026 •

edited

Loading

Review at `359f9f2`