Spaces:
Running
Running
File size: 1,873 Bytes
a6a5d8e | 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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 | #!/usr/bin/env python3
"""Validate the A11oy theorem-to-runtime manifest."""
from __future__ import annotations
import argparse
import json
from pathlib import Path
REPO_ROOT = Path.cwd()
MANIFEST = REPO_ROOT / "docs" / "theorem-runtime-manifest.json"
VALID_STATUSES = {
"verified-runtime",
"lean-backed-current-green",
"lean-backed-needs-upstream-ci",
"lean-backed-needs-runtime",
"historical-roadmap",
"roadmap",
}
def main() -> int:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--manifest", default=str(MANIFEST))
args = parser.parse_args()
path = Path(args.manifest)
data = json.loads(path.read_text(encoding="utf-8"))
errors: list[str] = []
seen = set()
for entry in data.get("entries", []):
entry_id = entry.get("id")
if not entry_id:
errors.append("entry missing id")
continue
if entry_id in seen:
errors.append(f"duplicate entry id: {entry_id}")
seen.add(entry_id)
status = entry.get("claimStatus")
if status not in VALID_STATUSES:
errors.append(f"{entry_id}: invalid claimStatus {status}")
for field in ["runtimeFile", "exportFile", "testFile"]:
value = entry.get(field)
if value and not (REPO_ROOT / value).exists():
errors.append(f"{entry_id}: missing {field} path {value}")
if status == "verified-runtime" and not entry.get("validationCommand"):
errors.append(f"{entry_id}: verified-runtime requires validationCommand")
if errors:
print("Theorem runtime manifest failed:")
for error in errors:
print(f" - {error}")
return 1
print(f"Theorem runtime manifest OK: {len(seen)} entries")
return 0
if __name__ == "__main__":
raise SystemExit(main())
|