scripts/README.md

scripts/

check_lean_manifest.py

Cross-checks data/lean_status.json against the actual lean-taf Lean source repo. Run before pushing to catch:

• Theorems renamed / deleted in source but still in manifest.
• Line numbers in manifest no longer matching the source declaration (e.g. after a refactor moved theorems).
• New theorems in source not yet captured in manifest.
• Commit-hash drift between manifest and current lean-taf HEAD.

Usage

# default — auto-detects ../lean-taf or ../NeurIPS/lean_taf/taf
python scripts/check_lean_manifest.py

# explicit path
python scripts/check_lean_manifest.py --lean-taf-path /path/to/lean-taf

# rewrite manifest in-place to match source (backs up to .bak first)
python scripts/check_lean_manifest.py --regenerate

Exit 0 = clean, 1 = drift detected. Suitable as a pre-push hook or CI gate once lean-taf is checked out alongside.

Workflow

1. After committing changes in lean-taf (renaming a theorem, adding a new one, etc.):
2. In tafagent/, run python scripts/check_lean_manifest.py to see what drifted.
3. If line numbers shifted but theorem set is unchanged: python scripts/check_lean_manifest.py --regenerate rewrites in-place.
4. If new theorems appeared: regenerate captures them with file/line only — manually fill claim, tactic, tags, etc. before committing.
5. Commit data/lean_status.json to tafagent.

What --regenerate preserves vs overwrites

• Overwrites: file, line, lean_repo.commit, lean_repo.commit_short.
• Preserves: claim, tactic, preconditions, status, tags, source, ui_badge, plus findings, groups[].title/id, summary, ui_bindings. The schema is rewritten with the same keys — anything not derivable from source is kept verbatim.