[Deicyde]

Summary

• capture Lean source trees as one stable filesystem generation, retaining
  directory identity through descriptor APIs where available and using a
  repeatable, revalidated portable fallback elsewhere
• derive declaration links, source revisions, and generation revisions from
  the same captured bytes
• exclude tooling, publication output, and caller-specified roots without
  accepting case-alias escapes
• provide opt-in hard limits for observed entries, path depth, per-file bytes,
  and aggregate captured bytes
• fail closed on concurrent replacement, special files, unsafe materialization
  paths, and unavailable bounded enumeration
• translate source-index I/O failures at CLI, audit, render, runtime, and
  skeleton caller boundaries without exposing host paths

Stack and scope restoration

PR #15 is merged in upstream main. Commit 758ede0 additively merged that main
into reviewed candidate 5e34514; c54be00 then repaired Windows path-stat vs
descriptor-stat normalization while preserving full same-interface checks.

Four later commits attempted the independent follow-up work now tracked in
#63, #64, and #65, but expanded this PR and introduced new source-classification
regressions. Current head f7acc1e contains four ordinary revert commits—no
force-push—and its tree is byte-for-byte identical to reviewed c54be00:

• tree ID: 30b140806c706114c232fd3967077a74e6accc9d
• git diff c54be00..f7acc1e: empty

The follow-up hardening remains in its focused issues rather than inflating or
changing #28's reviewed contract.

Validation

• Python 3.10 source/snapshot matrix: 131 passed, 3 skipped
• Python 3.13 source/snapshot matrix: 131 passed, 3 skipped
• Exact restored tree's prior Actions run 37068399307: Python 3.10, Python
  3.13, Windows hardening, real Lean, and CLA all green
• make lint
• make check-example
• independent scope/tree verification: exact match with approved c54be00

Fresh CI on f7acc1e remains the merge gate; the PR will be relabeled ready
only after every required job passes.

[Deicyde]

Review result: changes needed at b9fc9e9.

• The portable fallback is not a safe generation boundary. _capture_portable checks a child with lstat, then descends through its live pathname. A concurrent directory-to-symlink or junction swap can redirect traversal outside the root; repeating the swap for both comparison passes produced an accepted a/b/secret.lean from outside the tree. Use native no-follow handles, or fail closed when safe descriptor traversal is unavailable.
• BoundDirectoryTree.capture() reuses one retained directory descriptor. Concurrent captures interfere through the shared directory offset: on an unchanged 300-file tree, 196 of 200 paired captures failed with TreeSnapshotError, while sequential capture returned all 300 files. Serialize capture/verify/close or open an independent directory handle per operation.
• Root and exclusion normalization disagree. The direct snapshot APIs reject ordinary macOS paths under /tmp and /var because those ancestors are symlinks, while index_project resolves them first. In addition, index_project(alias, exclude_roots=(alias / "generated",)) silently ignores the absolute exclusion when alias is a supported symlinked root, and indexes the excluded Lean file. Normalize the root and its exclusions as one mapping.
• build_linker(source_index=...) detects live HEAD independently from the supplied snapshot. Capturing at commit A, advancing to B, then building the linker emitted a B permalink for a declaration that existed only in A. Downstream #35 uses this sequence. Require a ref bound to the snapshot or an explicit matching ref.

The focused snapshot suite passes (103 passed, 3 skipped), and the full suite passes (649 passed, 4 skipped), so these need concurrency and temporal-binding regressions rather than adjustments to existing assertions.

[Deicyde]

Second pass on exact head b9fc9e9. Additional findings:

• [P1] Audit escapes the captured Lean generation. _source_spans() rereads index.root / path at audit.py:428 even though the new SourceIndex already stores captured line_counts. In a deterministic repro, a one-line captured file was rewritten to 251 lines after indexing; index.line_counts remained 1 while _source_spans(index) returned 251. This can produce false size findings from a mixture of generations. Consume only the captured line counts.
• [P2] The new fail-closed source errors escape public CLI boundaries. With a valid bundled blueprint and a Lean root containing Linked.lean -> outside, autoform check printed its initial OK line and then raised an uncaught OSError: unsafe Lean source ...; audit, render, and runtime callers have the same unadapted boundary. Translate snapshot failures into stable command-specific errors/exit codes, and do not print success before all requested validation completes.
• [P2] Publication-root classification is quadratic. lean.py:326-341 scans the growing publication_roots set for every candidate, then repeats linear root scans per entry. Synthetic snapshots took 1.19s, 4.71s, and 19.45s for 500, 1,000, and 2,000 sibling roots. The capture limits do not bound this post-capture CPU. Use a prefix index or a linear sorted ancestor walk.
• [P2] Valid bounded inputs can leak raw exceptions. TreeCaptureLimits(max_file_bytes=sys.maxsize) on a one-byte file raises OverflowError because _read_file requests max_bytes + 1; a 5 KB non-marker publication.json with an integer over Python's digit limit raises plain ValueError because _is_publication_manifest_bytes catches only JSONDecodeError. Chunk/cap reads safely and convert all bounded parser failures to the documented snapshot/index error contracts.

Validation: focused snapshot/graph/runtime tests 133 passed, 3 skipped; four independent regression repros passed; Ruff passed.

[Deicyde]

Ready-review blockers are fixed at bc4179f.

The final design fails closed where descriptor-safe source traversal is unavailable instead of accepting repeatable path captures. It also prunes managed outputs before source capture, restores exact source/output casing semantics, sanitizes path failures, binds captured indexes by root identity, and prevents Git-ref/source-generation mismatches.

Validation is green: Python 3.10, Python 3.13, Windows capability/publication hardening, and the real-Lean fixture job all pass. Local affected tests, focused regressions, lint, and the bundled example/site build pass as recorded in the updated PR description.

[Deicyde]

Current head f7acc1e is a normal, non-force history-preserving restoration whose tree exactly equals independently approved c54be00 (git diff c54be00..f7acc1e is empty). The four reverted commits are tracked as focused follow-ups in #63–#65 rather than expanding this PR. Fresh exact-head Python 3.10, Python 3.13, Windows hardening, real Lean, and CLA checks are all green; the ready label is restored.

[Deicyde]

Re-audit result: current head f7acc1e is not merge-ready.

The four reverts restore the exact c54be00 tree, but also restore the original
P1 portable-traversal escape. I independently reproduced a directory admitted
as local, swapped to an outside symlink for the recursive read, restored before
verification, and repeated in both comparison passes. Descriptor traversal
rejected it; forced portable traversal accepted the outside Escaped.lean.
Two matching pathname snapshots are therefore not a filesystem-generation
boundary.

Two further blockers reproduce:

• build_linker() can detect ref A and then capture source generation B,
  emitting an A permalink for a declaration that exists only in B.
• Atomic generated-output churn under a recognized managed-output manifest is
  still captured before classification and fails source indexing, contradicting
  the stated exclusion contract.

The follow-up mapping in the body is also incorrect: #63–#65 do not track the
portable source-tree escape or linker ref/source race; #64 reinforces the need
to fail closed where descriptor-safe traversal is unavailable.

Recommended repair: reapply 0cfd6bc's fail-closed traversal policy and
bc4179f's Windows publication-fixture decoupling; salvage only the ref/source
retry from 3100c9d; fix managed-output projection separately without restoring
that commit's casing/pruning regressions; then update the body and rerun review.
Current green CI does not exercise the repeatable ABA repro.

[Deicyde]

Superseded by #95, which carries this PR's commits from a facebookresearch branch, follows #79's directory binding, and classifies snapshot failures.