add(graphs): derive theorem metadata from the sources and add graphs and audit build aliases (no drift)

.gitignore

@@ -9,3 +9,5 @@ _build/
 *.cmx
 __pycache__/
 *.pyc
+.lia.cache
+.audit-work.*

dune

@@ -0,0 +1,6 @@
+(rule
+ (alias audit)
+ (deps
+  (source_tree theory)
+  (source_tree scripts))
+ (action (run bash scripts/audit.sh)))

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)))

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())

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():
+def load(path):
-    with open(META, "r", encoding="utf-8") as f:
+    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)
+        path = os.path.join(args.outdir, name)
-        with open(p, "w", encoding="utf-8") as f:
+        with open(path, "w", encoding="utf-8") as f:
             f.write(text)
-        print("wrote", os.path.relpath(p, ROOT))
+        print("wrote", os.path.relpath(path, ROOT))
-        if not run_dot(p):
+        if not run_dot(path):
             ok = False
     return 0 if ok else 1