feat: land superpaper v1 notes scaffold
Add the ledger schema, class router, lint codes, ingest/build pipeline, and three work-tree examples: align derivation, superfig delegation, and supertensor delegation.
This commit is contained in:
Executable
+243
@@ -0,0 +1,243 @@
|
||||
#!/usr/bin/env python3
|
||||
"""Ledger and notes lint for superpaper. Codes live in DESIGN.md §10."""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import os
|
||||
import re
|
||||
import sys
|
||||
from copy import deepcopy
|
||||
from pathlib import Path
|
||||
|
||||
import yaml
|
||||
from jsonschema import Draft7Validator
|
||||
|
||||
ROOT = Path(__file__).resolve().parent.parent
|
||||
sys.path.insert(0, str(ROOT / "scripts"))
|
||||
from router import SIBLING, check_row, phase_from_env # noqa: E402
|
||||
|
||||
SCHEMA_PATH = ROOT / "assets" / "ledger.schema.yaml"
|
||||
KNOWN_TOP = {
|
||||
"schema", "retired_ids", "paper", "coverage", "questions", "claims",
|
||||
"definitions", "assumptions", "lemmas", "symbols", "derivations",
|
||||
"figures", "evidence", "terms", "source_assets",
|
||||
}
|
||||
ID_GROUPS = (
|
||||
"questions", "claims", "definitions", "assumptions", "lemmas",
|
||||
"derivations", "figures", "evidence", "source_assets",
|
||||
)
|
||||
KIND_ALIASES = {
|
||||
"activation": "value",
|
||||
"value / activation": "value",
|
||||
"logit": "score",
|
||||
"score / logit": "score",
|
||||
"coordinate": "index",
|
||||
"index / coordinate": "index",
|
||||
"order": "rank",
|
||||
"rank / order": "rank",
|
||||
"support": "mask",
|
||||
"mask / support": "mask",
|
||||
"shape-parameter": "shape parameter",
|
||||
"shape_parameter": "shape parameter",
|
||||
}
|
||||
STY_RE = re.compile(r"\\usepackage(?:\[[^\]]*\])?\{(superfig|supertensor|superderive)\}")
|
||||
LABEL_RE = re.compile(r"\\splabel\{(C[1-9][0-9]*)\}")
|
||||
|
||||
|
||||
def emit(path: Path, messages: list[str]) -> None:
|
||||
print(f"!! {path}", file=sys.stderr)
|
||||
for msg in messages:
|
||||
print(f" {msg}", file=sys.stderr)
|
||||
|
||||
|
||||
def normalize_kinds(data: dict) -> dict:
|
||||
out = deepcopy(data)
|
||||
for sym in out.get("symbols") or []:
|
||||
if isinstance(sym, dict) and "kind" in sym:
|
||||
kind = sym["kind"]
|
||||
if kind in KIND_ALIASES:
|
||||
sym["kind"] = KIND_ALIASES[kind]
|
||||
return out
|
||||
|
||||
|
||||
def collect_ids(data: dict) -> list[str]:
|
||||
ids: list[str] = []
|
||||
for key in ID_GROUPS:
|
||||
for row in data.get(key) or []:
|
||||
if isinstance(row, dict) and "id" in row:
|
||||
ids.append(str(row["id"]))
|
||||
return ids
|
||||
|
||||
|
||||
def notes_text(notes_paths: list[Path]) -> str:
|
||||
chunks: list[str] = []
|
||||
for path in notes_paths:
|
||||
if path.is_file():
|
||||
chunks.append(path.read_text(encoding="utf-8"))
|
||||
return "\n".join(chunks)
|
||||
|
||||
|
||||
def find_notes(work: Path | None, notes: Path | None) -> list[Path]:
|
||||
found: list[Path] = []
|
||||
if notes is not None:
|
||||
found.append(notes)
|
||||
if work is not None:
|
||||
nd = work / "notes"
|
||||
if (nd / "notes.tex").is_file():
|
||||
found.append(nd / "notes.tex")
|
||||
found.extend(sorted(nd.glob("sections/*.tex")))
|
||||
# unique, keep order
|
||||
seen: set[Path] = set()
|
||||
uniq: list[Path] = []
|
||||
for p in found:
|
||||
rp = p.resolve()
|
||||
if rp not in seen:
|
||||
seen.add(rp)
|
||||
uniq.append(p)
|
||||
return uniq
|
||||
|
||||
|
||||
def lint(
|
||||
ledger_path: Path,
|
||||
*,
|
||||
work: Path | None,
|
||||
extra_notes: Path | None,
|
||||
disk: bool,
|
||||
notes_scan: bool,
|
||||
) -> tuple[list[str], list[str]]:
|
||||
errors: list[str] = []
|
||||
warnings: list[str] = []
|
||||
raw = yaml.safe_load(ledger_path.read_text(encoding="utf-8"))
|
||||
if not isinstance(raw, dict):
|
||||
return ["SP001 ledger is not a mapping"], warnings
|
||||
|
||||
data = normalize_kinds(raw)
|
||||
schema = yaml.safe_load(SCHEMA_PATH.read_text(encoding="utf-8"))
|
||||
validator = Draft7Validator(schema)
|
||||
for err in validator.iter_errors(data):
|
||||
loc = ".".join(str(p) for p in err.absolute_path) or "$"
|
||||
errors.append(f"SP001 {loc}: {err.message}")
|
||||
if errors:
|
||||
return errors, warnings
|
||||
|
||||
for key in data:
|
||||
if key not in KNOWN_TOP:
|
||||
warnings.append(f"unknown top-level key {key!r}")
|
||||
|
||||
coverage = data.get("coverage") or {}
|
||||
if coverage.get("mode") == "full" and not coverage.get("sections_in"):
|
||||
warnings.append("coverage.mode=full and sections_in is empty")
|
||||
|
||||
ids = collect_ids(data)
|
||||
seen: set[str] = set()
|
||||
for i in ids:
|
||||
if i in seen:
|
||||
errors.append(f"SP002 duplicate id {i}")
|
||||
seen.add(i)
|
||||
|
||||
retired = set(data.get("retired_ids") or [])
|
||||
for row_key in ID_GROUPS:
|
||||
for row in data.get(row_key) or []:
|
||||
if not isinstance(row, dict):
|
||||
continue
|
||||
rid = row.get("id")
|
||||
if rid in retired and row.get("status") != "dropped":
|
||||
errors.append(f"SP023 {rid} is in retired_ids")
|
||||
|
||||
claim_ids = {c["id"] for c in (data.get("claims") or []) if "id" in c}
|
||||
phase = phase_from_env()
|
||||
notes_paths = find_notes(work, extra_notes)
|
||||
body = notes_text(notes_paths) if notes_scan else ""
|
||||
|
||||
if notes_scan:
|
||||
for path in notes_paths:
|
||||
text = path.read_text(encoding="utf-8")
|
||||
if STY_RE.search(text):
|
||||
errors.append(f"SP003 {path.name} loads a figure package")
|
||||
|
||||
labels = set(LABEL_RE.findall(body)) if notes_scan else set()
|
||||
|
||||
for fig in data.get("figures") or []:
|
||||
fid = fig.get("id", "F?")
|
||||
signals = set(fig.get("signals") or [])
|
||||
toolkit = fig.get("toolkit")
|
||||
status = fig.get("status", "planned")
|
||||
include = fig.get("include", None)
|
||||
code = check_row(
|
||||
signals, toolkit, status=status, include=include,
|
||||
fig_id=fid, phase=phase,
|
||||
)
|
||||
if code:
|
||||
errors.append(f"{code} {fid}")
|
||||
if toolkit == "superderive" and phase < 2:
|
||||
errors.append(f"SP022 {fid} toolkit superderive is v2; use align")
|
||||
if toolkit in SIBLING and status != "dropped" and disk:
|
||||
req = fig.get("request")
|
||||
req_path = (work / "notes" / req) if (work and req) else None
|
||||
if not req or req_path is None or not req_path.is_file():
|
||||
errors.append(f"SP012 {fid} missing request file")
|
||||
if include and disk and work is not None:
|
||||
on_disk = work / "notes" / include
|
||||
if not on_disk.is_file():
|
||||
errors.append(f"SP021 {fid} include not on disk: {include}")
|
||||
claim = fig.get("claim")
|
||||
if claim and claim not in claim_ids:
|
||||
errors.append(f"SP024 {fid} claim {claim} is not a known C*")
|
||||
|
||||
for der in data.get("derivations") or []:
|
||||
claim = der.get("claim")
|
||||
if claim and claim not in claim_ids:
|
||||
errors.append(f"SP024 {der.get('id')} claim {claim} is not a known C*")
|
||||
|
||||
if notes_scan:
|
||||
for claim in data.get("claims") or []:
|
||||
if claim.get("status") == "core" and claim.get("id") not in labels:
|
||||
errors.append(f"SP020 core {claim['id']} has no \\splabel")
|
||||
for sym in data.get("symbols") or []:
|
||||
name = str(sym.get("name", ""))
|
||||
latex = str(sym.get("latex", ""))
|
||||
if name and name not in body and latex and latex not in body:
|
||||
warnings.append(f"symbol {name} never appears in notes")
|
||||
|
||||
return errors, warnings
|
||||
|
||||
|
||||
def main() -> int:
|
||||
parser = argparse.ArgumentParser(description="lint a superpaper ledger / notes tree")
|
||||
parser.add_argument("--work", help="work tree root (ledger.yaml + notes/)")
|
||||
parser.add_argument("--out", dest="work_alias", help="alias of --work")
|
||||
parser.add_argument("--ledger", help="ledger.yaml (skips disk/notes codes unless --notes)")
|
||||
parser.add_argument("--notes", help="extra notes.tex for SP003/SP020")
|
||||
args = parser.parse_args()
|
||||
|
||||
work = Path(args.work or args.work_alias).resolve() if (args.work or args.work_alias) else None
|
||||
if work is not None:
|
||||
ledger = work / "ledger.yaml"
|
||||
disk = True
|
||||
notes_scan = True
|
||||
elif args.ledger:
|
||||
ledger = Path(args.ledger).resolve()
|
||||
disk = False
|
||||
notes_scan = args.notes is not None
|
||||
else:
|
||||
parser.error("need --work or --ledger")
|
||||
return 2
|
||||
|
||||
extra = Path(args.notes).resolve() if args.notes else None
|
||||
if not ledger.is_file():
|
||||
print(f"!! {ledger}", file=sys.stderr)
|
||||
print(" SP000 no such ledger", file=sys.stderr)
|
||||
return 2
|
||||
|
||||
errors, warnings = lint(ledger, work=work, extra_notes=extra, disk=disk, notes_scan=notes_scan)
|
||||
if errors:
|
||||
emit(ledger, errors)
|
||||
return 1
|
||||
for warn in warnings:
|
||||
print(f"warning: {warn}", file=sys.stderr)
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
Reference in New Issue
Block a user