Repair incomplete Autoform projects conservatively

[Deicyde]

Summary

• add autoform project repair for existing compatible Lean projects
• preserve every existing managed file and add only unambiguous missing canonical files
• require explicit title, repository URL, and verified workflow provenance when reconstruction needs them
• serialize repair, traverse through retained descriptors, and publish each file with atomic no-replace semantics
• detect concurrent configuration, parent, workflow, preserved-file, and destination changes
• report files already or possibly published and retain ambiguous staging files for manual recovery

Depends on #26. The reviewable changes are commits 9db7332 and 3b85315; earlier commits belong to the dependency stack.

Status on 2026-10-02: this branch predates the current stack. It is 98 commits behind #26 and still carries the first version of #14's inspector. 3b85315 makes repair hash lakefile.toml and lean-toolchain itself, before inspection, instead of reading hashes from the inspection report, which #14 no longer provides. Porting onto the current #26 is still to do: _scaffold_plan now takes a template snapshot, the release catalog is flat, and the inspection report renamed lean and lake.path.

Validation

• affected surface on Python 3.10: 247 passed
• affected surface on Python 3.13: 247 passed
• full suite: 894 passed, 1 skipped (895 passed, 1 skipped at 3b85315)
• installed-wheel repair smoke: passed
• make lint
• make check-example
• git diff --check
• three adversarial review rounds; final exact-diff verdict: SHIP

[Deicyde]

Reviewed exact head 9db73321681d8662d7bba3766c3e471ee9976c9b.

I found five issues that should be addressed before merging:

1. The supported unpinned creation path cannot later install CI. project new without provenance omits every .github/* file and therefore the .github directory. A subsequent project repair --autoform-source ... --autoform-ref ... rejects the missing parent instead of creating the canonical parent chain. This leaves no documented repair transition once provenance becomes available.

2. Workflow reconstruction does not validate the helper the workflow executes. _scope_workflow_files treats only the two YAML files as a provenance-compatible set. Replacing .github/autoform_audit.py with arbitrary bytes, deleting both YAML files, and repairing with the original pin succeeds and preserves the bogus helper; both newly generated workflows then execute it. Validate the helper together with the workflow files before adding any missing member of that bundle.

3. Recovery paths can be false after a parent or root rename. Publication through the retained directory descriptor can put the file in a detached tree, but the error reports only the logical in-project path in written and tells the user to inspect it. That path is absent, the actual artifact is unreported, and a retry can create a second copy. Recovery output needs to identify a reachable artifact, or publication must stop while the ancestry is still name-bound.

4. Atomic no-replace support is preflighted only by libc symbol presence. On a filesystem that rejects RENAME_NOREPLACE, repair creates and fsyncs a temporary, receives EINVAL/ENOTSUP, then rewrites project-repair-safety-unavailable as project-repair-recovery-required and poisons retries with retained debris. The same early check also rejects a complete no-op repair. Probe the bound target filesystem after planning, or preserve the capability error and safely handle the known-unpublished temporary.

5. Retrying does not repair a reported durability failure. I injected a failure at the parent-directory fsync; the first call reported project-repair-durability-failed with mkdocs.yml written. The same repair then returned success with an empty plan and performed zero directory fsyncs. A retry must synchronize the preserved published entry before claiming success.

Validation: 247 focused project/CLI tests passed. The worktree remained clean.

[Deicyde]

Restacking against final #26 confirms the earlier review blockers and adds three
parent-contract failures: the new bounded scaffold snapshot is not supplied,
inspection reopens the root pathname instead of using the retained descriptor,
and the race guard omits the authoritative manifest/override/lakefile.lean
inputs from #14.

More importantly, the current recovery claim cannot be made honest by adding
prechecks. If a retained parent/root is renamed during descriptor-relative
publication, the file can be written into a detached tree while the result
reports a logical path that no longer reaches it. POSIX has no atomic primitive
that both proves an ancestor generation is still name-bound and renames a
child. The existing no-replace capability check and retry-after-fsync behavior
also do not provide durable recovery.

Recommended rewrite boundary: retain the pure planner and descriptor-bound
inspection, but replace the mutation engine with a durable transaction journal,
central same-filesystem staging, descriptor-relative hard-link publication,
first-class directory plan entries, and resumable per-step fsync/recovery state.
Treat both workflows plus autoform_audit.py as one provenance-validated
bundle. If arbitrary ancestor renames remain in scope, default to exporting a
deterministic repair bundle/patch rather than claiming portable in-place
recovery.

[Deicyde]

Moved to #71. VivienCabannes/autoform-bot is being deleted, so this PR now lives on the same-named branch in facebookresearch/autoform-bot (head 3b85315, unchanged). Please continue review on #71; new commits go to facebookresearch:split/08-project-repair, not the fork.