From 9f7696eb2fe058b211defca6f441668e8eba0683 Mon Sep 17 00:00:00 2001 From: milner Date: Tue, 22 Sep 2026 12:02:00 +0200 Subject: [PATCH] add(graphs): derive theorem metadata from the sources and add graphs and audit build aliases (no drift) --- .gitignore | 2 + dune | 6 ++ graphs/dune | 23 ++++++ scripts/extract_metadata.py | 148 ++++++++++++++++++++++++++++++++++++ scripts/gen_graphs.py | 35 +++++++-- 5 files changed, 207 insertions(+), 7 deletions(-) create mode 100644 dune create mode 100644 graphs/dune create mode 100755 scripts/extract_metadata.py diff --git a/.gitignore b/.gitignore index e8eff97..853bd96 100644 --- a/.gitignore +++ b/.gitignore @@ -9,3 +9,5 @@ _build/ *.cmx __pycache__/ *.pyc +.lia.cache +.audit-work.* diff --git a/dune b/dune new file mode 100644 index 0000000..8b5913f --- /dev/null +++ b/dune @@ -0,0 +1,6 @@ +(rule + (alias audit) + (deps + (source_tree theory) + (source_tree scripts)) + (action (run bash scripts/audit.sh))) diff --git a/graphs/dune b/graphs/dune new file mode 100644 index 0000000..6913097 --- /dev/null +++ b/graphs/dune @@ -0,0 +1,23 @@ +(rule + (alias graphs) + (deps + ../scripts/gen_graphs.py + ../scripts/extract_metadata.py + (source_tree ../theory)) + (targets + theorems.json + dependency.dot + dependency.svg + dependency.png + rules.dot + rules.svg + rules.png + reduction.dot + reduction.svg + reduction.png) + (mode promote) + (action + (run python3 ../scripts/gen_graphs.py + --outdir . + --meta theorems.json + --theory ../theory))) diff --git a/scripts/extract_metadata.py b/scripts/extract_metadata.py new file mode 100755 index 0000000..425950f --- /dev/null +++ b/scripts/extract_metadata.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +import argparse +import json +import os +import re +import sys + +DECLS = ( + "Lemma", + "Theorem", + "Corollary", + "Proposition", + "Example", + "Definition", + "Fixpoint", + "Inductive", +) +PAPER = re.compile(r"^(lemma_|theorem_|corollary_|proposition_)") +MILESTONE = { + "ExecReducer": "M0", + "Binding": "M1", + "Reduction": "M1", + "Metatheory": "M2", + "Tests": "M2", +} +MILESTONE_ORDER = ["M0", "M1", "M2", "M3", "M4", "M5", "M6"] +PAPER_META = { + "title": "Milner's Lambda-Calculus with Partial Substitutions", + "authors": ["Delia Kesner", "Shane Ó Conchúir"], + "url": "https://arxiv.org/abs/2312.13270", + "html": "https://arxiv.org/html/2312.13270v1", +} + + +def split_decls(text): + pat = re.compile(r"^\s*(" + "|".join(DECLS) + r")\s+([A-Za-z0-9_']+)") + closer = re.compile(r"\b(Qed|Defined|Admitted)\.\s*$") + decls = [] + cur = None + closed = True + for line in text.splitlines(): + m = pat.match(line) + if m: + if cur is not None: + decls.append(cur) + cur = {"kind": m.group(1), "name": m.group(2), "lines": [line]} + closed = False + elif cur is not None and not closed: + cur["lines"].append(line) + if closer.search(line): + closed = True + if cur is not None: + decls.append(cur) + return decls + + +def status_of(decl): + body = "\n".join(decl["lines"]) + if decl["kind"] in ("Definition", "Fixpoint", "Inductive"): + return "defined" + if "Admitted" in body or re.search(r"\badmit\b", body): + return "blocked" + if re.search(r"\b(Qed|Defined)\.", body): + return "proved" + return "stated" + + +def section_of(name): + m = re.match(r"^[a-z]+_(\d+)_(\d+)", name) + if m: + return m.group(1) + "." + m.group(2) + m = re.match(r"^[a-z]+_(\d+)$", name) + if m: + return m.group(1) + return "" + + +def extract(theory_dir): + nodes = [] + for fname in sorted(os.listdir(theory_dir)): + if not fname.endswith(".v"): + continue + mod = fname[:-2] + path = os.path.join(theory_dir, fname) + with open(path, "r", encoding="utf-8") as fh: + text = fh.read() + for decl in split_decls(text): + if decl["kind"] not in ("Lemma", "Theorem", "Corollary", "Proposition", "Example"): + continue + name = decl["name"] + nodes.append( + { + "id": name, + "label": name, + "kind": "paper" if PAPER.match(name) else "infra", + "status": status_of(decl), + "milestone": MILESTONE.get(mod, "M0"), + "section": section_of(name), + "file": "theory/" + fname, + "depends": [], + } + ) + ids = {n["id"] for n in nodes} + raw = {} + for fname in sorted(os.listdir(theory_dir)): + if not fname.endswith(".v"): + continue + with open(os.path.join(theory_dir, fname), "r", encoding="utf-8") as fh: + text = fh.read() + for decl in split_decls(text): + if decl["name"] in ids: + raw[decl["name"]] = "\n".join(decl["lines"]) + for n in nodes: + body = raw.get(n["id"], "") + deps = [] + for other in sorted(ids): + if other == n["id"]: + continue + if re.search(r"\b" + re.escape(other) + r"\b", body): + deps.append(other) + n["depends"] = deps + milestones = [m for m in MILESTONE_ORDER if any(n["milestone"] == m for n in nodes)] + return { + "paper": PAPER_META, + "milestones": milestones, + "current": milestones[-1] if milestones else "M0", + "nodes": nodes, + } + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--theory", default="theory") + ap.add_argument("--out", default="graphs/theorems.json") + args = ap.parse_args() + data = extract(args.theory) + outdir = os.path.dirname(args.out) + if outdir: + os.makedirs(outdir, exist_ok=True) + with open(args.out, "w", encoding="utf-8") as fh: + json.dump(data, fh, ensure_ascii=False, indent=2) + fh.write("\n") + print("wrote", args.out, "with", len(data["nodes"]), "nodes") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/gen_graphs.py b/scripts/gen_graphs.py index a572dd9..7dd2502 100755 --- a/scripts/gen_graphs.py +++ b/scripts/gen_graphs.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +import importlib.util import json import os import subprocess @@ -36,8 +37,8 @@ def q(s): return '"' + str(s).replace("\\", "\\\\").replace('"', '\\"') + '"' -def load(): - with open(META, "r", encoding="utf-8") as f: +def load(path): + with open(path, "r", encoding="utf-8") as f: return json.load(f) @@ -159,7 +160,27 @@ def run_dot(path): def main(): - data = load() + import argparse + ap = argparse.ArgumentParser() + ap.add_argument("--outdir", default=GRAPH_DIR) + ap.add_argument("--meta", default=os.path.join(GRAPH_DIR, "theorems.json")) + ap.add_argument("--theory", default=None) + args = ap.parse_args() + os.makedirs(args.outdir, exist_ok=True) + if args.theory: + spec = importlib.util.spec_from_file_location( + "extract_metadata", + os.path.join(ROOT, "scripts", "extract_metadata.py"), + ) + extract = importlib.util.module_from_spec(spec) + spec.loader.exec_module(extract) + data = extract.extract(args.theory) + with open(args.meta, "w", encoding="utf-8") as fh: + json.dump(data, fh, ensure_ascii=False, indent=2) + fh.write("\n") + print("wrote", os.path.relpath(args.meta, ROOT)) + else: + data = load(args.meta) outputs = { "dependency.dot": dependency_dot(data), "rules.dot": rules_dot(), @@ -167,11 +188,11 @@ def main(): } ok = True for name, text in outputs.items(): - p = os.path.join(GRAPH_DIR, name) - with open(p, "w", encoding="utf-8") as f: + path = os.path.join(args.outdir, name) + with open(path, "w", encoding="utf-8") as f: f.write(text) - print("wrote", os.path.relpath(p, ROOT)) - if not run_dot(p): + print("wrote", os.path.relpath(path, ROOT)) + if not run_dot(path): ok = False return 0 if ok else 1