From fc25bbae0593ea7aca7d5086155bad56834c550a Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Fri, 23 Oct 2026 18:03:33 -0500 Subject: [PATCH 1/3] =?UTF-8?q?tools/hypergraph:=20pinned=20repo-agnostic?= =?UTF-8?q?=20hypergraph=20package=20(companion=20to=20main#579)=20?= =?UTF-8?q?=E2=80=94=20organization=20only,=20NOT=20A=20RESULT?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- tools/hypergraph/inputs.json | 65 +++++ tools/hypergraph/math_hypergraph.py | 435 ++++++++++++++++++++++++++++ tools/hypergraph/requirements.txt | 7 + tools/hypergraph/test_artifacts.py | 52 ++++ 4 files changed, 559 insertions(+) create mode 100644 tools/hypergraph/inputs.json create mode 100644 tools/hypergraph/math_hypergraph.py create mode 100644 tools/hypergraph/requirements.txt create mode 100644 tools/hypergraph/test_artifacts.py diff --git a/tools/hypergraph/inputs.json b/tools/hypergraph/inputs.json new file mode 100644 index 0000000..8bbf7df --- /dev/null +++ b/tools/hypergraph/inputs.json @@ -0,0 +1,65 @@ +{ + "note": "Inputs for tools/hypergraph. Paths are relative to this repo's root. Repos whose checkout is absent are skipped with a message. Organization only: credit 0, OBL OPEN. Companion copy in query-: this repo is checkout '.', others are optional read-only checkouts under external/.", + "home": "main", + "default_repos": [ + "query-" + ], + "repos": { + "main": { + "github": "d6g8k5htny-coder/main", + "checkout": "external/main", + "ledger": "external/main/data/hypergraph/math_coverage_ledger_20261023.md", + "graph": "external/main/docs/site/dependency-source/GRAPH.json", + "report": "external/main/data/hypergraph/graph_binding_report_20261023.json" + }, + "Math-": { + "github": "d6g8k5htny-coder/Math-", + "checkout": "external/Math-", + "unit_depth": 2, + "artifacts": { + "review": [ + "*REVIEW*.md", + "reviews/*" + ], + "source": [ + "*PROOF*.md", + "*LEMMA*.md", + "*lemma*.md", + "*.tex", + "PROOF_INDEX.md" + ], + "formal": [ + "*.lean" + ], + "impl": [ + "*.py" + ] + } + }, + "query-": { + "github": "d6g8k5htny-coder/query-", + "checkout": ".", + "unit_depth": 1, + "artifacts": { + "test": [ + "tests/*.py", + "test_*.py" + ], + "spec": [ + "portable/*.json", + "portable/history/*.json" + ], + "source": [ + "portable/*.md", + "docs/*.md" + ], + "impl": [ + "src/*.py", + "src/*/*.py", + "scripts/*.py", + "*.py" + ] + } + } + } +} diff --git a/tools/hypergraph/math_hypergraph.py b/tools/hypergraph/math_hypergraph.py new file mode 100644 index 0000000..e287599 --- /dev/null +++ b/tools/hypergraph/math_hypergraph.py @@ -0,0 +1,435 @@ +#!/usr/bin/env python3 +"""Math artifact hypergraph (Hypergraph-DB), repo-agnostic. Organization only: credit 0, OBL OPEN, no flags. + +One hyperedge per coverage-ledger row (kind=binding) linking unit, source/review files, +implementations, graph nodes, lane and record; plus, for every repo listed in +tools/hypergraph/inputs.json with an `artifacts` section, one hyperedge per artifact +directory (kind=artifact). Every vertex key is prefixed `:` (main:, Math-:, query-:). +All paths are relative to the repo root (HG_ROOT, else `git rev-parse`, else this file). +Repos whose checkout is absent (private, or not cloned) are skipped with a message. + +Usage (from the repo root): + python -m tools.hypergraph.math_hypergraph build [--png] [--out DIR] [--repos a,b|all] [--check] + python -m tools.hypergraph.math_hypergraph export DIR [--repos a,b|all] [--png] + python -m tools.hypergraph.math_hypergraph reach [depth] + python -m tools.hypergraph.math_hypergraph gaps | validate | shared-impl [n] | repos +""" +import argparse, collections, fnmatch, hashlib, json, os, re, subprocess, sys, tempfile +from pathlib import Path +from hyperdb import HypergraphDB + +HERE = Path(__file__).resolve().parent + + +def _root(): + if os.environ.get("HG_ROOT"): + return Path(os.environ["HG_ROOT"]).resolve() + try: + out = subprocess.run(["git", "rev-parse", "--show-toplevel"], cwd=HERE, capture_output=True, + text=True, check=True).stdout.strip() + if out: + return Path(out).resolve() + except (OSError, subprocess.CalledProcessError): + pass + return HERE.parents[1] + + +ROOT = _root() +CONFIG = HERE / "inputs.json" +DATA = ROOT / "data" / "hypergraph" +LEDGER = DATA / "math_coverage_ledger_20261023.md" +GRAPH = ROOT / "docs" / "site" / "dependency-source" / "GRAPH.json" +REPORT = DATA / "graph_binding_report_20261023.json" +HUBS = ("lane", "record") +PLACEHOLDER = re.compile(r"in PR head|per census", re.I) +REQUIRED_ROLES = ("unit",) +OUTPUTS = ("math_hypergraph.json", "query_results.json") +SKIP_DIRS = {".git", ".lake", "lake-packages", "node_modules", "__pycache__", ".venv", "external"} + + +def load_config(path=CONFIG): + return json.loads(Path(path).read_text()) + + +def _vt(k): + """vertex type part of '::'""" + return k.split(":", 2)[1] + + +def _vid(k): + return k.split(":", 2)[2] + + +def parse_ledger(path=LEDGER): + rows = [] + for line in Path(path).read_text().splitlines(): + if not re.match(r"^\| \d+ \|", line): + continue + c = [x.strip() for x in line.strip().strip("|").split("|")] + rows.append(dict(n=int(c[0]), rec=c[1], repo=c[2], unit=c[3].strip("`"), lane=c[4], + src=c[5], impl=c[6], node=c[7], bound=c[8], status=c[9])) + return rows + + +def _split(cell, sep=";"): + if cell in ("", "—") or cell.upper().startswith("MISSING"): + return [] + return [s.strip() for s in cell.split(sep) if s.strip()] + + +def build(ledger=LEDGER, graph=GRAPH, report=REPORT, config=None, repos=None, hg=None, home="main"): + """Build the hypergraph. With config/repos, also add artifact hyperedges for those repos. + Returns (hg, G, skipped).""" + hg = HypergraphDB() if hg is None else hg + G, skipped = {}, [] + if ledger is not None and Path(graph).exists(): + G = _build_ledger(hg, ledger, graph, report, home) + for name in (repos or []): + spec = (config or {}).get("repos", {}).get(name) + if spec is None: + raise KeyError(f"repo {name!r} not in inputs config") + base = ROOT / spec.get("checkout", ".") + if not base.is_dir(): + msg = (f"skip {name}: checkout {spec.get('checkout')} not present " + f"(repo private or not cloned; public repos are fetched by actions/checkout)") + print(msg, file=sys.stderr); skipped.append(name); continue + if spec.get("artifacts"): + add_artifacts(hg, name, base, spec) + return hg, G, skipped + + +def _build_ledger(hg, ledger, graph, report, home): + G = json.loads(Path(graph).read_text())["nodes"] + R = json.loads(Path(report).read_text()) + bound_nodes = {b["node_id"] for b in R["bound"]} + + def V(k, typ, **d): + if not hg.has_v(k): + hg.add_v(k, {"type": typ, **d}) + return k + + for nid, nd in G.items(): + V(f"{home}:node:" + nid, "graph_node", layer=nd.get("layer"), kind=nd.get("kind"), + bound_in_527=nid in bound_nodes) + for r in parse_ledger(ledger): + rp = r["repo"] + u = V(f"{rp}:unit:{r['unit']}", "unit", row=r["n"], status=r["status"], bound=r["bound"] == "Y") + members = {u: "unit"} + members[V(f"{home}:record:" + r["rec"], "record")] = "review" + members[V(f"{home}:lane:" + r["lane"], "lane")] = "lane" + srcs = _split(r["src"]) + for s in srcs: + role = "review" if re.search(r"REVIEW", s, re.I) else "source" + members[V(f"{rp}:src:" + (s if "/" in s else r["unit"] + "/" + s), "source_file")] = role + imps = _split(r["impl"]) + placeholders = [] + for s in imps: + if s.startswith("(") or s.endswith(")") or PLACEHOLDER.search(s): + placeholders.append(s) # text, not an artifact + continue + members[V(f"{rp}:impl:" + s, "implementation")] = "impl" + for s in _split(r["node"], ","): + members[V(f"{home}:node:" + s, "graph_node")] = "node" + hg.add_e(tuple(members), { + "kind": "binding", "row": r["n"], "roles": members, "bound": r["bound"] == "Y", + "has_source": bool(srcs), "has_impl": bool(imps), + "impl_placeholder": bool(imps) and not any(_vt(k) == "impl" for k in members), + "placeholders": placeholders, "credit": 0, "obl": "OPEN"}) + return G + + +ROLE_TYPE = {"source": "source_file", "review": "source_file", "formal": "formal_file", + "impl": "implementation", "spec": "spec_file", "test": "test_file"} + + +def _walk(base): + for dp, dns, fns in os.walk(base): + dns[:] = sorted(d for d in dns if d not in SKIP_DIRS) + for f in sorted(fns): + yield (Path(dp) / f).relative_to(base).as_posix() + + +def add_artifacts(hg, repo, base, spec): + """One hyperedge per artifact directory (first `unit_depth` path parts).""" + depth = int(spec.get("unit_depth", 2)) + pats = spec["artifacts"] + units = collections.defaultdict(dict) + for rel in _walk(base): + role = next((r for r, gl in pats.items() if any(fnmatch.fnmatchcase(rel, g) for g in gl)), None) + if role is None: + continue + parts = rel.split("/")[:-1] + unit = "/".join(parts[:depth]) if parts else "(root)" + units[unit][f"{repo}:{'src' if role in ('source', 'review') else role}:{rel}"] = role + for unit in sorted(units): + u = f"{repo}:unit:{unit}" + if not hg.has_v(u): + hg.add_v(u, {"type": "unit", "row": None, "status": "artifact-scan", "bound": False}) + members = {u: "unit"} + for k, role in sorted(units[unit].items()): + if not hg.has_v(k): + hg.add_v(k, {"type": ROLE_TYPE[role]}) + members[k] = role + if len(members) > 1 and not hg.has_e(tuple(members)): + hg.add_e(tuple(members), {"kind": "artifact", "repo": repo, "unit": unit, "row": None, + "roles": members, "credit": 0, "obl": "OPEN"}) + return len(units) + + +def nbr_vertices(hg, v): + # workaround: hyperdb nbr_v()/nbr_e_of_v() raise on isolated vertices + if not hg.degree_v(v): + return set() + return set().union(*[set(e) for e in hg.nbr_e_of_v(v)]) - {v} + + +def reach(hg, start, depth=2): + if not hg.has_v(start): + raise KeyError(start) + seen, front = {start}, {start} + for _ in range(depth): + nxt = set() + for v in front: + if hg.v(v)["type"] in HUBS and v != start: + continue # hubs: do not traverse through + if hg.degree_v(v): + for e in hg.nbr_e_of_v(v): + nxt |= set(e) + front = nxt - seen + seen |= nxt + return seen - {start} + + +def validate(hg): + """Role validator: every hyperedge must carry each REQUIRED_ROLES role, and + every member must have a role. Returns a list of problems.""" + problems = [] + for e in hg.all_e: + d = hg.e(e) + roles = d.get("roles", {}) + for req in REQUIRED_ROLES: + if req not in roles.values(): + problems.append({"row": d.get("row"), "problem": f"missing role {req}"}) + for v in e: + if v not in roles: + problems.append({"row": d.get("row"), "problem": f"member without role {v}"}) + return problems + + +def gaps(hg, G): + units = [v for v in hg.all_v if hg.v(v)["type"] == "unit" and hg.v(v).get("row") is not None] + edges = {u: [hg.e(e) for e in hg.nbr_e_of_v(u) if hg.e(e).get("kind") == "binding"] for u in units} + placeholder = sorted(u for u in units if any(d["impl_placeholder"] for d in edges[u])) + no_src = sorted(u for u in units if not any(d["has_source"] for d in edges[u])) + no_impl = sorted(u for u in units if not any(d["has_impl"] for d in edges[u])) + nodes = [v for v in hg.all_v if hg.v(v)["type"] == "graph_node"] + unbound = sorted(_vid(v) for v in nodes if _vid(v) in G and not hg.v(v).get("bound_in_527")) + untouched = sorted(_vid(v) for v in nodes if not any(_vt(x) == "unit" for x in nbr_vertices(hg, v))) + return { + "units": len(units), "sourced": len(units) - len(no_src), "no_source": no_src, + "implemented": len(units) - len(no_impl), "no_impl": no_impl, + "impl_placeholder_only": placeholder, + "bound_units": sum(1 for u in units if hg.v(u)["bound"]), + "graph_nodes": len(G), "unbound_nodes_per_527": unbound, + "nodes_touched_by_no_unit": untouched, + "role_problems": validate(hg), + } + + +def shared_impl(hg, n=5): + c = collections.Counter() + for v in hg.all_v: + if hg.v(v)["type"] == "implementation": + c[v] = sum(1 for x in nbr_vertices(hg, v) if _vt(x) == "unit") + return sorted(c.items(), key=lambda kv: (-kv[1], kv[0]))[:n] + + +def summary(g): + return {k: (len(v) if isinstance(v, list) else v) for k, v in g.items()} + + +def repo_stats(hg): + c = collections.defaultdict(collections.Counter) + for v in hg.all_v: + c[v.split(":", 1)[0]][hg.v(v)["type"]] += 1 + e = collections.Counter((hg.e(x).get("repo") or "ledger") for x in hg.all_e) + return {r: {"vertices": dict(sorted(t.items())), "artifact_hyperedges": e.get(r, 0)} for r, t in sorted(c.items())} + + +def write_outputs(hg, G, out=DATA, png=False): + out.mkdir(parents=True, exist_ok=True) + (out / "math_hypergraph.json").write_text(json.dumps( + {"note": "organization only; credit 0, OBL OPEN, no flags", + "vertices": {k: hg.v(k) for k in sorted(hg.all_v)}, + "hyperedges": sorted((hg.e(e) for e in hg.all_e), key=lambda d: (d["row"] is None, d["row"] or 0, d.get("repo") or "", d.get("unit") or ""))}, + sort_keys=True, separators=(",", ":"), default=list) + "\n") + g = gaps(hg, G) + q = "main:node:math.d1-component.congruence-erratum" + res = {"note": "organization only; credit 0, OBL OPEN, no flags", + "stats": {"vertices": hg.num_v, "hyperedges": hg.num_e, + "by_type": dict(sorted(collections.Counter(hg.v(v)["type"] for v in hg.all_v).items()))}, + "gap_counts": summary(g), "gaps": g, + "by_repo": repo_stats(hg), + "reach_example": ({"start": q, "1hop": sorted(reach(hg, q, 1)), "2hop_count": len(reach(hg, q, 2))} + if hg.has_v(q) else None), + "shared_impl_top5": shared_impl(hg)} + (out / "query_results.json").write_text(json.dumps(res, indent=1, sort_keys=True, default=list) + "\n") + if png: + try: + render_png(hg, out / "bindings_hypergraph.png") + except ImportError: + print("PNG skipped: Pillow not installed (optional)", file=sys.stderr) + return res + + +def render_png(hg, path): + # library draw() only serves a web page; render with Pillow + import math + from PIL import Image, ImageDraw + E = sorted((e for e in hg.all_e if any(_vt(v) == "node" for v in e)), key=lambda e: hg.e(e)["row"] or 0) + vs = sorted({v for e in E for v in e if _vt(v) not in HUBS}) + W = 1400; img = Image.new("RGB", (W, W), "white"); d = ImageDraw.Draw(img); cx = cy = W / 2 + pos = {v: (cx + 560 * math.cos(2 * math.pi * i / len(vs)), cy + 560 * math.sin(2 * math.pi * i / len(vs))) for i, v in enumerate(vs)} + col = {"formal_file": "#9467bd", "spec_file": "#8c564b", "test_file": "#7f7f7f", "unit": "#1f77b4", "graph_node": "#d62728", "source_file": "#2ca02c", "implementation": "#ff7f0e"} + for e in E: + m = [v for v in e if v in pos] + hx = sum(pos[v][0] for v in m) / len(m) * 0.6 + cx * 0.4; hy = sum(pos[v][1] for v in m) / len(m) * 0.6 + cy * 0.4 + c = "#000000" if hg.e(e).get("bound") else "#999999" + for v in m: + d.line([pos[v], (hx, hy)], fill=c, width=1) + d.rectangle([hx - 4, hy - 4, hx + 4, hy + 4], fill=c) + for v, (x, y) in pos.items(): + d.ellipse([x - 5, y - 5, x + 5, y + 5], fill=col[hg.v(v)["type"]]) + d.text((20, 20), "Unit-to-graph-node hyperedges (square = 1 binding hyperedge; black bound, grey unbound)", fill="black") + d.text((20, 40), "blue unit, red graph node, green source, orange impl. Organization only: credit 0, OBL OPEN", fill="black") + img.convert("P", palette=Image.ADAPTIVE, colors=16).save(path, optimize=True) + + +def _sha(p): + return hashlib.sha256(Path(p).read_bytes()).hexdigest() + + +def _repos_arg(cfg, val): + if val is None: + return list(cfg.get("default_repos", [])) + if val == "all": + return list(cfg.get("repos", {})) + return [x for x in val.split(",") if x] + + +def _make(cfg, repos): + home = cfg.get("home", "main") + spec = cfg.get("repos", {}).get(home, {}) + ledger = spec.get("ledger") + if ledger and (ROOT / ledger).exists(): + return build(ROOT / ledger, ROOT / spec["graph"], ROOT / spec["report"], cfg, + [r for r in repos if r != home or spec.get("artifacts")], home=home) + return build(None, None, None, cfg, repos, home=home) + + +def check(cfg, repos, ref=DATA): + """Rebuild into a temp dir; return list of committed outputs that differ.""" + hg, G, _ = _make(cfg, repos) + with tempfile.TemporaryDirectory() as td: + write_outputs(hg, G, Path(td)) + return [f for f in OUTPUTS if not (ref / f).exists() + or (Path(td) / f).read_bytes() != (ref / f).read_bytes()] + + +def export(hg, G, out, cfg, repos, skipped, png=False): + out = Path(out); out.mkdir(parents=True, exist_ok=True) + res = write_outputs(hg, G, out, png) + manifest = {"note": "organization only; credit 0, OBL OPEN, no flags", "format": "math-hypergraph/1", + "repos_included": [r for r in repos if r not in skipped], "repos_skipped": skipped, + "hyperdb": "hypergraph-db==0.4.0", + "files": {f.name: _sha(f) for f in sorted(out.iterdir()) if f.name != "MANIFEST.json"}} + (out / "MANIFEST.json").write_text(json.dumps(manifest, indent=1, sort_keys=True) + "\n") + (out / "README.md").write_text(EXPORT_README.format( + repos=", ".join(manifest["repos_included"]) or "(none)", skipped=", ".join(skipped) or "none", + v=hg.num_v, e=hg.num_e)) + return res + + +EXPORT_README = """# Math hypergraph export bundle — organization only, NOT A RESULT + +credit 0 · OBL OPEN · no flags. Self-contained: needs only Python 3.10+ (and optionally hypergraph-db==0.4.0). + +Repos included: {repos}. Skipped: {skipped}. {v} vertices, {e} hyperedges. + +- `math_hypergraph.json` — `vertices` (key `::` -> attributes) and `hyperedges` + (each has `roles` {{member -> role}}; members are the role keys; `kind` is `binding` or `artifact`). +- `query_results.json` — gap counts, per-repo stats, reach example, shared implementations. +- `MANIFEST.json` — sha256 of every file in this bundle. + +Load anywhere: +```python +import json +from hyperdb import HypergraphDB # optional; plain dicts work too +d = json.load(open("math_hypergraph.json")) +hg = HypergraphDB() +for k, a in d["vertices"].items(): hg.add_v(k, a) +for e in d["hyperedges"]: hg.add_e(tuple(e["roles"]), e) +``` +""" + + +def load_json(path): + d = json.loads(Path(path).read_text()) + hg = HypergraphDB() + for k, a in d["vertices"].items(): + hg.add_v(k, a) + for e in d["hyperedges"]: + hg.add_e(tuple(e["roles"]), e) + return hg + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) + ap.add_argument("--config", type=Path, default=CONFIG) + sp = ap.add_subparsers(dest="cmd", required=True) + b = sp.add_parser("build"); b.add_argument("--png", action="store_true"); b.add_argument("--out", type=Path, default=DATA) + b.add_argument("--check", action="store_true", help="rebuild to a temp dir; exit 1 if committed outputs differ") + b.add_argument("--repos", default=None, help="comma list or 'all' (default: config default_repos)") + x = sp.add_parser("export"); x.add_argument("out", type=Path); x.add_argument("--repos", default="all") + x.add_argument("--png", action="store_true") + r = sp.add_parser("reach"); r.add_argument("vertex"); r.add_argument("depth", nargs="?", type=int, default=2) + sp.add_parser("gaps"); sp.add_parser("validate"); sp.add_parser("repos") + s = sp.add_parser("shared-impl"); s.add_argument("n", nargs="?", type=int, default=5) + for p in (r, s, sp.choices["gaps"], sp.choices["validate"]): + p.add_argument("--repos", default=None) + a = ap.parse_args(argv) + cfg = load_config(a.config) + if a.cmd == "repos": + for n, spec in cfg.get("repos", {}).items(): + print(f"{n}\t{spec.get('checkout')}\t{'present' if (ROOT / spec.get('checkout', '.')).is_dir() else 'absent'}") + return 0 + repos = _repos_arg(cfg, getattr(a, "repos", None)) + if a.cmd == "build" and a.check: + diff = check(cfg, repos, a.out) + if diff: + print("STALE: " + ", ".join(diff) + " differ from a fresh rebuild; run build and commit", file=sys.stderr) + return 1 + print("build --check: committed outputs match a fresh rebuild"); return 0 + hg, G, skipped = _make(cfg, repos) + if a.cmd == "build": + print(json.dumps(write_outputs(hg, G, a.out, a.png)["gap_counts"], indent=1)); return 0 + if a.cmd == "export": + export(hg, G, a.out, cfg, repos, skipped, a.png); print(f"exported {hg.num_v} vertices / {hg.num_e} hyperedges to {a.out}"); return 0 + if a.cmd == "reach": + try: + print("\n".join(sorted(reach(hg, a.vertex, a.depth)))) + except KeyError: + print(f"unknown vertex: {a.vertex}", file=sys.stderr); return 2 + return 0 + if a.cmd == "gaps": + print(json.dumps(summary(gaps(hg, G)), indent=1)); return 0 + if a.cmd == "shared-impl": + for v, k in shared_impl(hg, a.n): + print(f"{k}\t{v}") + return 0 + p = validate(hg) + print(json.dumps(p, indent=1)); return 1 if p else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/tools/hypergraph/requirements.txt b/tools/hypergraph/requirements.txt new file mode 100644 index 0000000..2f5732e --- /dev/null +++ b/tools/hypergraph/requirements.txt @@ -0,0 +1,7 @@ +hypergraph-db==0.4.0 +pillow==12.1.0 +pytest==9.1.1 +iniconfig==2.3.1 +packaging==26.3 +pluggy==1.7.0 +pygments==2.21.0 diff --git a/tools/hypergraph/test_artifacts.py b/tools/hypergraph/test_artifacts.py new file mode 100644 index 0000000..d140370 --- /dev/null +++ b/tools/hypergraph/test_artifacts.py @@ -0,0 +1,52 @@ +"""Repo-agnostic artifact-scan tests (synthetic tree; run in any repo). Organization only: credit 0, OBL OPEN.""" +import importlib.util, sys +from pathlib import Path +import pytest + +pytest.importorskip("hyperdb") +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("math_hypergraph", HERE / "math_hypergraph.py") +mh = importlib.util.module_from_spec(spec); sys.modules["math_hypergraph"] = mh; spec.loader.exec_module(mh) + +SPEC = {"unit_depth": 2, "artifacts": {"review": ["*REVIEW*.md"], "source": ["*PROOF*.md"], + "formal": ["*.lean"], "impl": ["*.py"]}} + + +def _tree(tmp_path): + for rel in ("frontiers/a/PROOF.md", "frontiers/a/A.lean", "frontiers/a/run.py", "frontiers/a/REVIEW_x.md", + "frontiers/b/deep/B.lean", "frontiers/b/notes.txt", ".lake/pkg/X.lean", "top.py"): + p = tmp_path / rel; p.parent.mkdir(parents=True, exist_ok=True); p.write_text("x") + return tmp_path + + +def test_artifact_hyperedges(tmp_path): + hg = mh.HypergraphDB() + n = mh.add_artifacts(hg, "Math-", _tree(tmp_path), SPEC) + assert n == 3 # frontiers/a, frontiers/b, (root); .lake skipped + assert all(v.startswith("Math-:") for v in hg.all_v) + roles = {hg.e(e)["unit"]: sorted(hg.e(e)["roles"].values()) for e in hg.all_e} + assert roles["frontiers/a"] == ["formal", "impl", "review", "source", "unit"] + assert roles["frontiers/b"] == ["formal", "unit"] + assert not any("X.lean" in v or "notes.txt" in v for v in hg.all_v) + assert mh.validate(hg) == [] + assert all(hg.e(e)["credit"] == 0 and hg.e(e)["obl"] == "OPEN" for e in hg.all_e) + + +def test_missing_repo_skipped(capsys): + cfg = {"repos": {"ghost": {"checkout": "external/__no_such_repo__", "artifacts": SPEC["artifacts"]}}} + hg, G, skipped = mh.build(None, None, None, cfg, ["ghost"]) + assert skipped == ["ghost"] and hg.num_v == 0 + assert "skip ghost" in capsys.readouterr().err + + +def test_unknown_repo_rejected(): + with pytest.raises(KeyError): + mh.build(None, None, None, {"repos": {}}, ["nope"]) + + +def test_config_paths_relative(): + cfg = mh.load_config() + for spec in cfg["repos"].values(): + for k in ("checkout", "ledger", "graph", "report"): + if k in spec: + assert not Path(spec[k]).is_absolute() and ".." not in Path(spec[k]).parts From 02e8fe1d519847435a8d48d4ea6b61f09c356594 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Fri, 23 Oct 2026 18:03:44 -0500 Subject: [PATCH 2/3] =?UTF-8?q?math-hypergraph=20workflow=20(Dylan=205:56/?= =?UTF-8?q?5:57pm=20CT=20approval)=20+=20README=20=E2=80=94=20organization?= =?UTF-8?q?=20only?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .github/workflows/math-hypergraph.yml | 70 +++++++++++++++++++++++++++ tools/hypergraph/README.md | 21 ++++++++ 2 files changed, 91 insertions(+) create mode 100644 .github/workflows/math-hypergraph.yml create mode 100644 tools/hypergraph/README.md diff --git a/.github/workflows/math-hypergraph.yml b/.github/workflows/math-hypergraph.yml new file mode 100644 index 0000000..66002e8 --- /dev/null +++ b/.github/workflows/math-hypergraph.yml @@ -0,0 +1,70 @@ +name: Math hypergraph (organization only) +'on': + pull_request: + paths: + - 'tools/hypergraph/**' + - '.github/workflows/math-hypergraph.yml' + - 'portable/**' + - 'src/**' + - 'docs/**' + push: + branches: [main] + paths: + - 'tools/hypergraph/**' + - '.github/workflows/math-hypergraph.yml' + - 'portable/**' + - 'src/**' + - 'docs/**' + workflow_dispatch: +permissions: + contents: read +jobs: + hypergraph: + name: math-hypergraph + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + # Read-only checkouts of the other public repos (no secrets). If one is private + # or unavailable the step is skipped and the builder prints "skip ". + - name: Checkout main (public, read-only) + continue-on-error: true + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: d6g8k5htny-coder/main + path: external/main + persist-credentials: false + - name: Checkout Math- (public, read-only) + continue-on-error: true + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + repository: d6g8k5htny-coder/Math- + path: external/Math- + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.12' + cache: pip + cache-dependency-path: tools/hypergraph/requirements.txt + - name: Install pinned requirements + run: python -m pip install -r tools/hypergraph/requirements.txt + - name: Tests + run: python -m pytest -q -p no:cacheprovider tools/hypergraph + - name: validate (query- artifacts) + run: python -m tools.hypergraph.math_hypergraph validate + - name: gaps + run: python -m tools.hypergraph.math_hypergraph gaps + - name: Build all-repo bundle with PNG + run: | + set -euo pipefail + python -m tools.hypergraph.math_hypergraph repos + python -m tools.hypergraph.math_hypergraph export "$RUNNER_TEMP/hypergraph" --repos all --png + ls -l "$RUNNER_TEMP/hypergraph" + - uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 + with: + name: math-hypergraph + path: ${{ runner.temp }}/hypergraph/ + if-no-files-found: error + retention-days: 14 diff --git a/tools/hypergraph/README.md b/tools/hypergraph/README.md new file mode 100644 index 0000000..5ad030a --- /dev/null +++ b/tools/hypergraph/README.md @@ -0,0 +1,21 @@ +# tools/hypergraph (query- companion) — organization only, NOT A RESULT + +credit 0 · OBL OPEN · no flags. Same pinned package as d6g8k5htny-coder/main `tools/hypergraph` (main#579); +this copy scans **query-** (checkout `.`) and, when present, read-only checkouts of main, Math- under `external/`. +Vertex keys are `::`. Absent/private repos are skipped with a message. + +## Run locally (Python 3.11/3.12) +``` +pip install -r tools/hypergraph/requirements.txt +pytest tools/hypergraph +python -m tools.hypergraph.math_hypergraph validate | gaps | repos +python -m tools.hypergraph.math_hypergraph export /tmp/hg-bundle --repos all --png +# optional: git clone --depth 1 https://github.com/d6g8k5htny-coder/ external/ +``` +Edit `inputs.json` to change which globs count as source / review / formal / impl / spec / test. + +## GitHub Actions — `.github/workflows/math-hypergraph.yml` +Runs on PRs/pushes to `main` touching the tool or query-'s artifacts, and via workflow_dispatch. Checks out the other public +repos read-only, installs pins on Python 3.12, runs pytest, `validate`, `gaps`, and uploads the all-repo export +(JSON, PNG, README, MANIFEST) as the `math-hypergraph` artifact. `contents: read`, no secrets, 10-minute timeout, not required. +The committed-output `build --check` gate lives in main, which owns the ledger. From 53c7412a1bf0305e66d02fb9fdc713131e31b281 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Fri, 23 Oct 2026 18:58:52 -0500 Subject: [PATCH 3/3] =?UTF-8?q?tools/hypergraph:=20mirror=20main#579=20Cop?= =?UTF-8?q?ilot=20fixes=20(identical=20builder)=20=E2=80=94=20formal/impl?= =?UTF-8?q?=20globs=20before=20reviews/*=20catch-all;=20record=20role;=20d?= =?UTF-8?q?eterministic=20path=20resolution=20(root=5Fdirs);=20home=20ledg?= =?UTF-8?q?er=20gated=20on=20--repos;=20README=20before=20MANIFEST;=20READ?= =?UTF-8?q?ME=20one=20query=20per=20line=20=E2=80=94=20organization=20only?= =?UTF-8?q?,=20credit=200,=20OBL=20OPEN?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- tools/hypergraph/README.md | 4 ++- tools/hypergraph/inputs.json | 16 ++++++---- tools/hypergraph/math_hypergraph.py | 46 +++++++++++++++++++++-------- tools/hypergraph/test_artifacts.py | 32 ++++++++++++++++++++ 4 files changed, 79 insertions(+), 19 deletions(-) diff --git a/tools/hypergraph/README.md b/tools/hypergraph/README.md index 5ad030a..56b7b65 100644 --- a/tools/hypergraph/README.md +++ b/tools/hypergraph/README.md @@ -8,7 +8,9 @@ Vertex keys are `::`. Absent/private repos are skipped with a me ``` pip install -r tools/hypergraph/requirements.txt pytest tools/hypergraph -python -m tools.hypergraph.math_hypergraph validate | gaps | repos +python -m tools.hypergraph.math_hypergraph validate +python -m tools.hypergraph.math_hypergraph gaps +python -m tools.hypergraph.math_hypergraph repos python -m tools.hypergraph.math_hypergraph export /tmp/hg-bundle --repos all --png # optional: git clone --depth 1 https://github.com/d6g8k5htny-coder/ external/ ``` diff --git a/tools/hypergraph/inputs.json b/tools/hypergraph/inputs.json index 8bbf7df..f455230 100644 --- a/tools/hypergraph/inputs.json +++ b/tools/hypergraph/inputs.json @@ -7,6 +7,7 @@ "repos": { "main": { "github": "d6g8k5htny-coder/main", + "root_dirs": [".github", "architecture", "audits", "data", "docs", "experiments", "formal", "governance", "history", "incoming", "interface", "records", "reviews", "tests", "tools"], "checkout": "external/main", "ledger": "external/main/data/hypergraph/math_coverage_ledger_20261023.md", "graph": "external/main/docs/site/dependency-source/GRAPH.json", @@ -14,9 +15,17 @@ }, "Math-": { "github": "d6g8k5htny-coder/Math-", + "root_dirs": [".github", "certificates", "claims", "coefficients", "companions", "docs", "formal", "frontiers", "imports", "incoming", "repairs", "reviews", "specifications", "tests", "tools"], "checkout": "external/Math-", "unit_depth": 2, + "artifacts_order": "first matching role wins: specific formal/impl globs precede the reviews/* catch-all", "artifacts": { + "formal": [ + "*.lean" + ], + "impl": [ + "*.py" + ], "review": [ "*REVIEW*.md", "reviews/*" @@ -27,17 +36,12 @@ "*lemma*.md", "*.tex", "PROOF_INDEX.md" - ], - "formal": [ - "*.lean" - ], - "impl": [ - "*.py" ] } }, "query-": { "github": "d6g8k5htny-coder/query-", + "root_dirs": [".github", "docs", "portable", "scripts", "src", "tests"], "checkout": ".", "unit_depth": 1, "artifacts": { diff --git a/tools/hypergraph/math_hypergraph.py b/tools/hypergraph/math_hypergraph.py index e287599..7d1264d 100644 --- a/tools/hypergraph/math_hypergraph.py +++ b/tools/hypergraph/math_hypergraph.py @@ -83,7 +83,8 @@ def build(ledger=LEDGER, graph=GRAPH, report=REPORT, config=None, repos=None, hg hg = HypergraphDB() if hg is None else hg G, skipped = {}, [] if ledger is not None and Path(graph).exists(): - G = _build_ledger(hg, ledger, graph, report, home) + G = _build_ledger(hg, ledger, graph, report, home, + config if config is not None else load_config()) for name in (repos or []): spec = (config or {}).get("repos", {}).get(name) if spec is None: @@ -98,7 +99,25 @@ def build(ledger=LEDGER, graph=GRAPH, report=REPORT, config=None, repos=None, hg return hg, G, skipped -def _build_ledger(hg, ledger, graph, report, home): +def _resolve(repo, unit, path, config=None): + """Resolve a ledger path to (repo, repo-root-relative path), deterministically (no filesystem). + `:` naming a configured repo is honored as-is. A path that starts with the unit + directory, or whose first component is one of the repo's configured `root_dirs`, is already + repo-root-relative; anything else (bare basenames, nested `C7/PROOF.md`) is unit-relative.""" + repos = (config or {}).get("repos", {}) + names = set(repos) | {"main", "Math-", "query-"} + m = re.match(r"^([A-Za-z0-9_.-]+):(.+)$", path) + if m and m.group(1) in names: + return m.group(1), m.group(2) + unit = unit.strip("/") + if path == unit or path.startswith(unit + "/"): + return repo, path + if "/" in path and path.split("/", 1)[0] in repos.get(repo, {}).get("root_dirs", ()): + return repo, path + return repo, f"{unit}/{path}" + + +def _build_ledger(hg, ledger, graph, report, home, config=None): G = json.loads(Path(graph).read_text())["nodes"] R = json.loads(Path(report).read_text()) bound_nodes = {b["node_id"] for b in R["bound"]} @@ -115,19 +134,21 @@ def V(k, typ, **d): rp = r["repo"] u = V(f"{rp}:unit:{r['unit']}", "unit", row=r["n"], status=r["status"], bound=r["bound"] == "Y") members = {u: "unit"} - members[V(f"{home}:record:" + r["rec"], "record")] = "review" + members[V(f"{home}:record:" + r["rec"], "record")] = "record" members[V(f"{home}:lane:" + r["lane"], "lane")] = "lane" srcs = _split(r["src"]) for s in srcs: role = "review" if re.search(r"REVIEW", s, re.I) else "source" - members[V(f"{rp}:src:" + (s if "/" in s else r["unit"] + "/" + s), "source_file")] = role + srp, sp = _resolve(rp, r["unit"], s, config) + members[V(f"{srp}:src:{sp}", "source_file")] = role imps = _split(r["impl"]) placeholders = [] for s in imps: if s.startswith("(") or s.endswith(")") or PLACEHOLDER.search(s): placeholders.append(s) # text, not an artifact continue - members[V(f"{rp}:impl:" + s, "implementation")] = "impl" + irp, ip = _resolve(rp, r["unit"], s, config) + members[V(f"{irp}:impl:{ip}", "implementation")] = "impl" for s in _split(r["node"], ","): members[V(f"{home}:node:" + s, "graph_node")] = "node" hg.add_e(tuple(members), { @@ -321,7 +342,7 @@ def _make(cfg, repos): home = cfg.get("home", "main") spec = cfg.get("repos", {}).get(home, {}) ledger = spec.get("ledger") - if ledger and (ROOT / ledger).exists(): + if ledger and home in repos and (ROOT / ledger).exists(): return build(ROOT / ledger, ROOT / spec["graph"], ROOT / spec["report"], cfg, [r for r in repos if r != home or spec.get("artifacts")], home=home) return build(None, None, None, cfg, repos, home=home) @@ -339,14 +360,15 @@ def check(cfg, repos, ref=DATA): def export(hg, G, out, cfg, repos, skipped, png=False): out = Path(out); out.mkdir(parents=True, exist_ok=True) res = write_outputs(hg, G, out, png) - manifest = {"note": "organization only; credit 0, OBL OPEN, no flags", "format": "math-hypergraph/1", - "repos_included": [r for r in repos if r not in skipped], "repos_skipped": skipped, - "hyperdb": "hypergraph-db==0.4.0", - "files": {f.name: _sha(f) for f in sorted(out.iterdir()) if f.name != "MANIFEST.json"}} - (out / "MANIFEST.json").write_text(json.dumps(manifest, indent=1, sort_keys=True) + "\n") + included = [r for r in repos if r not in skipped] (out / "README.md").write_text(EXPORT_README.format( - repos=", ".join(manifest["repos_included"]) or "(none)", skipped=", ".join(skipped) or "none", + repos=", ".join(included) or "(none)", skipped=", ".join(skipped) or "none", v=hg.num_v, e=hg.num_e)) + manifest = {"note": "organization only; credit 0, OBL OPEN, no flags", "format": "math-hypergraph/1", + "repos_included": included, "repos_skipped": skipped, + "hyperdb": "hypergraph-db==0.4.0", + "files": {f.name: _sha(f) for f in sorted(out.iterdir()) if f.is_file() and f.name != "MANIFEST.json"}} + (out / "MANIFEST.json").write_text(json.dumps(manifest, indent=1, sort_keys=True) + "\n") # written last return res diff --git a/tools/hypergraph/test_artifacts.py b/tools/hypergraph/test_artifacts.py index d140370..909b431 100644 --- a/tools/hypergraph/test_artifacts.py +++ b/tools/hypergraph/test_artifacts.py @@ -50,3 +50,35 @@ def test_config_paths_relative(): for k in ("checkout", "ledger", "graph", "report"): if k in spec: assert not Path(spec[k]).is_absolute() and ".." not in Path(spec[k]).parts + + +def test_specific_patterns_beat_review_catchall(tmp_path): + for rel in ("reviews/r1/check.py", "reviews/r1/L.lean", "reviews/r1/notes.md"): + p = tmp_path / rel; p.parent.mkdir(parents=True, exist_ok=True); p.write_text("x") + import json + cfg = json.loads((HERE / "inputs.json").read_text())["repos"]["Math-"] + hg = mh.HypergraphDB() + mh.add_artifacts(hg, "Math-", tmp_path, cfg) + roles = {k: r for e in hg.all_e for k, r in hg.e(e)["roles"].items()} + assert roles["Math-:impl:reviews/r1/check.py"] == "impl" + assert roles["Math-:formal:reviews/r1/L.lean"] == "formal" + assert roles["Math-:src:reviews/r1/notes.md"] == "review" + + +def test_resolve_paths(): + assert mh._resolve("Math-", "u/x", "main:architecture/a.json") == ("main", "architecture/a.json") + assert mh._resolve("Math-", "u/x", "replay.py") == ("Math-", "u/x/replay.py") + assert mh._resolve("Math-", "u/x", "u/x/C7/P.md") == ("Math-", "u/x/C7/P.md") + cfg = {"repos": {"Math-": {"root_dirs": ["frontiers"]}}} + assert mh._resolve("Math-", "u/x", "frontiers/y/P.md", cfg) == ("Math-", "frontiers/y/P.md") + assert mh._resolve("Math-", "u/x", "C7/P.md", cfg) == ("Math-", "u/x/C7/P.md") + assert mh._resolve("nochk", "u/x", "C7/P.md") == ("nochk", "u/x/C7/P.md") + + +def test_export_manifest_includes_readme(tmp_path): + hg = mh.HypergraphDB(); hg.add_v("m:unit:a", {"type": "unit"}) + mh.export(hg, {}, tmp_path, {}, [], []) + import json + man = json.loads((tmp_path / "MANIFEST.json").read_text()) + assert "README.md" in man["files"] + assert man["files"]["README.md"] == mh._sha(tmp_path / "README.md")