dela
5170111823
Rewrite references/pedagogy.md around recite-vs-teach: reader model,
coverage density (sections_in is cite permission, not a to-do list),
intuition-before-formula three-beat, and paper-jump filling.
Every notes/sections/sec-*.tex must now answer gap / takeaway / jump /
omit above the first \section. lint.py checks presence only (it cannot
judge honesty); files opening with "% generated by" are exempt.
- scripts/lint.py: SP025 + is_writer_section / teach_gaps helpers
- tests/no-teach-block/: fixture with takeaway only, wired into test.sh
- examples/*: all 14 writer sections get real teach blocks
- SKILL.md, references/{agents,antipatterns,checklist}.md, DESIGN.md,
assets/notes-template.tex: route writers and consistency agent
through pedagogy.md
270 lines
9.1 KiB
Python
Executable File
270 lines
9.1 KiB
Python
Executable File
#!/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]*)\}")
|
|
SECTION_RE = re.compile(r"^\s*\\section\b", re.MULTILINE)
|
|
GENERATED_RE = re.compile(r"^\s*%.*generated by", re.IGNORECASE)
|
|
TEACH_KEYS = ("gap", "takeaway", "jump", "omit")
|
|
TEACH_RE = {
|
|
key: re.compile(rf"^%\s*{key}\s*:\s*\S", re.MULTILINE)
|
|
for key in TEACH_KEYS
|
|
}
|
|
|
|
|
|
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 is_writer_section(path: Path) -> bool:
|
|
return path.parent.name == "sections" and path.name.startswith("sec-")
|
|
|
|
|
|
def teach_gaps(text: str) -> list[str]:
|
|
"""Keys missing from the `% teach:` block above the first \\section."""
|
|
if GENERATED_RE.match(text):
|
|
return []
|
|
match = SECTION_RE.search(text)
|
|
head = text[: match.start()] if match else text
|
|
return [key for key in TEACH_KEYS if not TEACH_RE[key].search(head)]
|
|
|
|
|
|
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")
|
|
if is_writer_section(path):
|
|
missing = teach_gaps(text)
|
|
if missing:
|
|
errors.append(
|
|
f"SP025 {path.name} % teach: block missing {', '.join(missing)}"
|
|
)
|
|
|
|
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 off; set SUPERPAPER_PHASE=2 or 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())
|