Count only the exact .lean suffix as Lean source by Deicyde · Pull Request #232 · facebookresearch/autoform-bot

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

Summary

autoform_cli/lean.py matched the .lean suffix after case folding, so Proj/Y.LEAN and Proj/W.Lean were captured and indexed. Lake's module globs (extension == some "lean"), skeleton.module_of/path_of and servers/__init__.py all use the exact suffix.
Symptoms: source-aware commands such as check --lean-root resolved declarations from files Lake and skeleton never see, and a symlink, special or unreadable file with such a name stopped indexing ("unsafe Lean source Proj/W.Lean: symbolic links are not supported").
Fix: the six relative.suffix.casefold() == ".lean" checks become relative.suffix == ".lean", with one comment at the capture filter. No new helper, no README change.
On case-insensitive volumes import Proj.Y can open Y.LEAN, but such a project builds only there and Lake's globs never list it. One rule on every host, matching Lake and skeleton.

Behavior changes

A file, unreadable file, symlink or special file named *.LEAN or *.Lean (any non-exact casing) is not captured or indexed, does not stop indexing, and does not change the source digest or generation revision.
A lean: name defined only in such a file is reported as not found, as skeleton and Lake already treat it.
Unchanged: links and special files named exactly *.lean are still refused; .#*.lean editor lock links are still skipped.

Tests

tests/test_lean_sources.py::test_case_variants_of_the_lean_suffix_are_ignored puts Y.LEAN (file), L.Lean (symlink), P.LEAN (named pipe) and U.Lean (mode 0) next to Project/Basic.lean and asserts the index, line counts, revision and generation_revision equal those of Basic.lean alone.

Fails at main, and each entry alone fails at main: the file indexes variantY, the link and pipe stop indexing, the unreadable file gives "permission denied: Project/U.Lean".
Keeping the case folding only in _lean_snapshot_includes fails via U.Lean, because capture still opens it. The other five sites only see entries that filter kept; they change so lean.py states one rule.

Overlap with open PRs

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

Prove Lean capture stability only for Lean inputs, and name what changed #257: lean.py, 4 hunks (none against main). Prove Lean capture stability only for Lean inputs, and name what changed #257 rewrites _lean_snapshot_includes and three suffix filters but keeps casefold(). Take Prove Lean capture stability only for Lean inputs, and name what changed #257's lines with the exact suffix.
Scale roadmap inventories and the full DAG explorer #90 (draft): lean.py goes from 1 to 2 hunks; it rewrites tolerated_links and keeps casefold(). Use the exact suffix.
Every other open PR merges the same as with main.

Validation

tests/test_lean_sources.py at 060d3cc: 141 passed, 3 skipped, 1 xfailed on Python 3.13, on 3.10.20 and with real Lean on PATH. The skips are case-colliding-name tests on a case-insensitive volume.
Applied on main ae2db51, the same file gives 143 passed, 3 skipped, 1 xfailed.
Full non-Lean suite on Python 3.13 at 060d3cc: 2075 passed, 65 skipped, 1 xfailed.
ruff check autoform_cli servers tests: clean.

The Lean source index treated Proj/Y.LEAN and Proj/W.Lean as Lean sources: it read and indexed them, so `check --lean-root` resolved declarations from files that Lake and `autoform skeleton` never see. A symbolic link, special file or unreadable file with such a name failed the whole index ("unsafe Lean source Proj/W.Lean: symbolic links are not supported"). (C4, blockers note 3, r2-g2-exact-lean-suffix, NEW-SKELETON-SUFFIX) Root cause: six sites in lean.py compared the suffix after case folding (capture selection for links and other entries, the tolerated editor-lock links, the unsupported-entry filter, the indexed-file loop and the generation revision), while Lake's module globs (Lean.forEachModuleInDir), skeleton.module_of and path_of, and the servers' file check all require the exact ".lean" suffix. Fix: one helper, _has_lean_suffix, compares the suffix exactly and is used at all six sites. A case variant of any entry kind is now not captured, not indexed, does not fail the index and does not change the source digest or generation revision. Symbolic links and special files named exactly *.lean are still refused. On a case-insensitive volume Lean can open Y.LEAN for `import Y`; the index follows Lake's globs and skeleton instead, so it is the same on every host. The README states the rule where it describes source-aware `--lean-root` inspection, since it applies to every command that reads the sources, not only check.

The _has_lean_suffix helper wrapped a single comparison that skeleton and the servers already write inline as suffix != ".lean". Each of the six sites in lean.py now writes the exact comparison directly, and one comment at the capture filter says why the suffix is not case folded. The README sentence covered an edge case that main's README never described, and it was a second place stating the rule. The open docs PR that lists what Lean indexing reads is where the rule belongs, so this branch no longer touches the README and no longer conflicts with the render branch's sentences in that paragraph. The four parametrized cases become one test that puts a regular file, an unreadable file, a symbolic link and a named pipe with case-variant suffixes next to Basic.lean. Descriptor capture is POSIX only, so the symlink and mkfifo skips could not trigger, and as root the unreadable file is simply read, which the exact suffix still ignores. Each entry kind alone fails at main, and the unreadable one still kills the mutant that keeps case folding only in the capture filter.

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 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-13T16:58:31Z

Review at `060d3cc`

Verdict: Merge-ready. This PR replaces the six relative.suffix.casefold() == ".lean" checks in autoform_cli/lean.py with an exact relative.suffix == ".lean" comparison (head lean.py:479, 484, 568, 576, 589, 629) and adds one test. Before it, a stray Foo.Lean symlink, FIFO or unreadable file stopped every source-aware command (check/audit/doctor --lean-root, render, search), and lean: names resolved from files that Lake and skeleton.py never read. After it, lean.py matches skeleton.py:1292, servers/__init__.py:49 and Lake's globs. It also restores the rule from before d834528, when sources came from rglob("*.lean"). The new test fails on main (confirmed by trace) and passes at this head. The PR is still a draft, so it needs to be marked ready first.

Optional

No test pins the four checks after the capture filter (autoform_cli/lean.py:568, 576, 589, 629), so a mutant that keeps casefold() at any of them passes. Confirmed by trace. That code can't be reached today because the filter only keeps exact .lean entries plus manifest.json, so nothing needs to change now. A future change that widens the filter (as Prove Lean capture stability only for Lean inputs, and name what changed #257 does) would lose that guarantee without a failing test.
In test_case_variants_of_the_lean_suffix_are_ignored (tests/test_lean_sources.py), only the unreadable U.Lean entry catches a mutant that folds case in the capture filter alone. Running as root, that mutant survives. Confirmed by trace. CI does not run as root, so this is a note only.

Landing

Merges cleanly with main ae2db51.
Land it before Document what stops Lean indexing #234. After this PR, Document what stops Lean indexing #234's README sentence "File and folder names here match in any letter case except build" is wrong for the .lean suffix (confirmed by reading Document what stops Lean indexing #234's diff). Document what stops Lean indexing #234 should limit that sentence to folder names and the fixed file names, and say the .lean suffix must match exactly. If Document what stops Lean indexing #234 merges first, this PR takes that one-line narrowing instead.
Land it before Prove Lean capture stability only for Lean inputs, and name what changed #257. Prove Lean capture stability only for Lean inputs, and name what changed #257 still adds suffix.casefold() == ".lean" checks and conflicts with this PR in autoform_cli/lean.py. Its rebase should adopt the exact suffix.
Scale roadmap inventories and the full DAG explorer #90 merges cleanly onto main but conflicts in autoform_cli/lean.py once this lands, because it rewrites tolerated_links and keeps casefold(). Whichever of the two lands second should use the exact suffix.

Decision for the maintainer

Case-insensitive volumes: on default macOS APFS, a project with Proj/Y.LEAN and import Proj.Y builds, but after this PR autoform check --lean-root reports a lean: name defined only in that file as not found. The PR body states the rule as a recorded choice, but that can't be attributed to you, so please confirm it. Options: accept the exact suffix on every host, or keep case folding and accept that capture depends on the filesystem. Recommendation: accept. Such a project already fails on Linux CI, main's README never documented the case-folded behavior, and the old rule let one stray .Lean entry take down every source-aware command.

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

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.

#232 made the .lean suffix exact. The four conflicting lean.py hunks keep this branch's lines (no in_ignored_root, ignored_roots or manifest.json clause, since selected mode already leaves marker-hidden and excluded folders out) with the exact suffix, relative.suffix == ".lean". The index digest loop, which merged cleanly, gets the same exact comparison, so no casefolded .lean suffix check remains.

…ock-link-check Conflict in autoform_cli/lean.py with facebookresearch#232: keep main's exact .lean suffix comparison and this branch's removal of tolerated_links.

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

This was referenced Oct 13, 2026

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

Merged

Document what stops Lean indexing #234

Merged

Deicyde mentioned this pull request Oct 13, 2026

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

Merged

Deicyde marked this pull request as ready for review October 13, 2026 17:20

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

Deicyde deleted the fix/exact-lean-suffix branch October 13, 2026 17:20

This was referenced Oct 13, 2026

Drop the second editor lock link check from Lean source indexing #269

Merged

Wait for Lean's diagnostics barrier instead of a quiet gap #256

Merged

Navigation Menu

Repository navigation

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

Count only the exact .lean suffix as Lean source#232
Deicyde merged 2 commits into
mainfrom
fix/exact-lean-suffix

Deicyde commented Oct 13, 2026 •

edited

Loading

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 060d3cc

Optional

Landing

Decision for the maintainer

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Deicyde commented Oct 13, 2026 •

edited

Loading

Review at `060d3cc`