Skip to content

Verify local Lean artifacts before publication - #69

Closed
Deicyde wants to merge 4 commits into
mainfrom
split/14-artifact-gates
Closed

Deicyde wants to merge 4 commits into
mainfrom
split/14-artifact-gates

Conversation

@Deicyde

@Deicyde Deicyde commented Oct 3, 2026

Copy link
Copy Markdown
Contributor

Moved from #36. Its head branch lived on VivienCabannes/autoform-bot, which is being deleted, so this PR uses the same-named branch in facebookresearch/autoform-bot (same commits, head 16a3033). Earlier review and discussion are on #36.


Summary

  • install one package-owned artifact verifier into generated projects
  • bind every local roadmap declaration to complete root-package .ilean, .olean, and .trace artifacts
  • run Lean at trust level zero and reject sorries, unsafe or partial declarations, unexpected axioms, malformed archives, races, and oversized inputs
  • require the same verification workflow before GitHub Pages publishes
  • reject mathlib: true claims until the separate Mathlib provenance slice lands

This builds on #28.

Validation

  • independent exact-diff review: SHIP
  • full suite: 700 passed, 3 skipped
  • focused artifact and affected-surface suites: 67 passed; 242 passed, 3 skipped
  • lint, bundled example, installed wheel import/CLI smoke, and diff check: passed

@Deicyde Deicyde added the awaiting author Review is complete and author action is required label Oct 3, 2026
@meta-cla meta-cla Bot added the CLA Signed This label is managed by the Meta Open Source bot. label Oct 3, 2026
@Deicyde

Deicyde commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

Replacement-branch review is BLOCKED at 4ef06e2; do not repoint or push this PR yet. Three real-Lean repros currently return CLEAN incorrectly: (1) a restored prior clean .ilean/.olean beside current changed source/trace/hash sidecars, because trace input/output hashes are never bound to retained source/artifact bytes; (2) a post-probe node_modules/payload.txt mutation consumed by include_str, because ignored directories are outside the claimed complete input boundary; and (3) a blueprint target naming a mangled _private... declaration with no retained lexical/source-coordinate binding. Exact-checkout tests are also red (blueprint diagnostic ordering and the 262-word develop-plugin limit), critical artifact cases are absent from real-Lean CI, and the branch bundles unresolved #95. The two uncommitted edits are not fixes: moving the final blueprint check earlier reopens an external-blueprint race, and the skill copyedit remains over limit and drops pinned guidance. Required next: verifier-owned/bound complete inputs plus trace-hash validation, fail-closed authored-name binding, isolated regressions and real-artifact CI, discard/rework the dirty edits, land/restack #95 first, then publish an artifact-only branch pinned to facebookresearch.

@Deicyde Deicyde closed this Oct 5, 2026
@Deicyde
Deicyde deleted the split/14-artifact-gates branch October 13, 2026 20:45
OrigamiClub pushed a commit to OrigamiClub/autoform-bot that referenced this pull request Oct 16, 2026
TreeSnapshot.materialize and materialize_regular_files wrote a captured
tree below a fresh directory with descriptor-relative mkdir and O_EXCL
writes, captured the result again to check it, and cleaned up after a
failure. They reached main with facebookresearch#95, and no production code on main
has ever called them: git log -S '.materialize(' is empty, and
git log -S materialize_regular_files finds only the three facebookresearch#95 commits
that added and hardened it with its tests. The callers lived only on
pull requests that never merged: facebookresearch#8 and facebookresearch#70, facebookresearch#34 and facebookresearch#72, facebookresearch#36 and facebookresearch#69,
facebookresearch#38 and facebookresearch#74, and facebookresearch#145. render writes
its private copy of the blueprint with _private_copy, and project new
has its own _materialize_project.

Delete both methods, the eleven helpers only they reached
(_materialization_parts through _cleanup_materialization), the
_WRITE_FILE_FLAGS, _DESCRIPTOR_MATERIALIZATION_SUPPORTED and
_WINDOWS_DEVICE_NAMES constants, and the two checkpoint events only they
emitted. Delete _synthetic_snapshot and the eight
test_snapshot_materialization_* tests, which covered nothing else, and
the TreeSnapshot import they leave unused.

unsupported_entries stays, with the _special_file_kind it uses: lean.py
and render.py call it to refuse links and special files. _normalized_name,
_close_descriptor, _stat_signature, _stable_entry_identity,
capture_directory_descriptor and the checkpoint hook keep their other
users. The deleted code was the last production code to set
TreeCaptureLimits.max_depth and max_file_bytes, and the only reader
besides revision of TreeSnapshot.placeholders and opaque_directories;
the next commits remove those.

TreeSnapshot keeps every field, and no capture path changes, so no
digest, revision, JSON output or CLI behavior changes.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting author Review is complete and author action is required CLA Signed This label is managed by the Meta Open Source bot.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant