Spaces:
Running
Running
File size: 1,803 Bytes
6e2328e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 | # 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
```bash
# 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.
|