diff --git a/.gitignore b/.gitignore
index ec3d7611..7bfb9a24 100644
--- a/.gitignore
+++ b/.gitignore
@@ -85,3 +85,6 @@ lychee-output/
# Fetched at render time by tools/install-extensions.py, not vendored
/_extensions/coatless-quarto/
+
+# Built before each render by tools/build_dependency_graph.py
+/dependency-graph.json
diff --git a/CLAUDE.md b/CLAUDE.md
index 51bb8703..31d33b0d 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -39,6 +39,9 @@ Authoritative style guides:
Quarto resolves `@id` only within a page, so without it the reference renders as "?@def-predicate".
It also repoints the links mds text carries (`[text](#def-foo)`, `[text](number-systems.qmd#def-foo)`) at the page here that defines the id,
and sends an id no page here defines to the published mds page, so an mds subfile with such links can be included
+- `tools/build_dependency_graph.py`, `dependency-graph.js`, `dependency-tree.qmd` --- the prerequisite graph of the definitions and results on the Math Reference (top-level) pages.
+ A `pre-render` step writes `dependency-graph.json` (git-ignored), and only `dependency-tree.qmd` loads the script, because the `chapters/` pages reuse some of the same ids.
+ The builder and script are copies of the lds ones (lds `tools/` and `chapters/`), shared with mds, pds and sds: change them there and copy them back (Morrison-Lab/lds#2412, a private repository the link checker cannot reach)
- `tools/racket-engine.R`, `tools/racket-pieces.R`, `tools/racket-eval.rkt` --- the knitr engine that runs `{racket}` chunks ([mcs#131](https://github.com/Morrison-Lab/mcs/issues/131)).
knitr and Quarto have no Racket engine, so a chapter with racket chunks includes `_subfiles/_racket-setup.qmd` once, after the macros include, to register it.
Each chunk runs in a fresh `racket` process that first replays the page's earlier racket chunks silently,
diff --git a/_quarto-website.yml b/_quarto-website.yml
index 1d3e1e8f..6c59a861 100644
--- a/_quarto-website.yml
+++ b/_quarto-website.yml
@@ -3,8 +3,14 @@ project:
output-dir: _site
# A third-party extension with no license is fetched, not vendored.
# See tools/install-extensions.py.
+ # Then writes dependency-graph.json: the prerequisite graph of the
+ # definitions and results on the Math Reference pages (the top-level pages).
pre-render:
- tools/install-extensions.py
+ - python3 tools/build_dependency_graph.py --pages . --site mcs --out dependency-graph.json
+ resources:
+ - dependency-graph.js
+ - dependency-graph.json
render:
- "*.qmd"
- "chapters/*.qmd"
@@ -122,6 +128,8 @@ website:
href: expressions-algorithms.qmd
- text: "Proof Writing"
href: proof-writing.qmd
+ - text: "Dependency Tree"
+ href: dependency-tree.qmd
right:
- icon: github
href: https://github.com/Morrison-Lab/mcs
@@ -187,6 +195,7 @@ website:
- functions.qmd
- expressions-algorithms.qmd
- proof-writing.qmd
+ - dependency-tree.qmd
callouty-theorem:
thm:
diff --git a/dependency-graph.js b/dependency-graph.js
new file mode 100644
index 00000000..3b52d77e
--- /dev/null
+++ b/dependency-graph.js
@@ -0,0 +1,268 @@
+/* Prerequisite and postrequisite graph of each definition and result.
+ Reads dependency-graph.json (tools/build_dependency_graph.py): an edge [A, B]
+ means A uses B, so B is a prerequisite of A. No library: plain SVG.
+ Three graphs, all reading top to bottom (prerequisites above, what uses them below),
+ with arrows pointing from what is used to what uses it:
+ - under every #def-/#thm-/#lem-/#prp-/#cor- div, a foldable block (folded by default)
+ holds one labeled graph focused on that div, DEPTH levels each way;
+ - an element with id "dependency-graph-page" gets a folded labeled graph of every div on its page;
+ - an element with id "dependency-graph-site" gets one tree of every div on the site, and an
+ element with id "dependency-graph-all" and a data-json attribute (comma-separated URLs of
+ several sites' dependency-graph.json) gets one tree of all those sites together.
+ These have hundreds of nodes, so their boxes carry no text: the kind and title show as hovertext. */
+(function () {
+ "use strict";
+ var DEPTH = 2, NS = "http://www.w3.org/2000/svg";
+ /* A per-div graph is small, so each box carries its clipped title. A site-wide or cross-site
+ tree has hundreds of nodes, so its boxes carry no text, which keeps the structure compact. */
+ var LABELED = { W: 200, H: 34, GX: 16, GY: 36, PER_ROW: 4 };
+ var COMPACT = { W: 16, H: 16, GX: 4, GY: 22, PER_ROW: 80 };
+ /* The div colors of the notes (custom-callout in _quarto-website.yml); a theorem shares a lemma's blue. */
+ var COLOR = { def: "#1B5E20", thm: "#1565C0", lem: "#1565C0", cor: "#00838F", prp: "#827717" };
+ var NAME = { def: "Definition", thm: "Theorem", lem: "Lemma", cor: "Corollary", prp: "Proposition" };
+ var script = document.currentScript;
+ var base = script ? script.src.replace(/[^/]*$/, "") : "";
+ var page = location.pathname.split("/").pop().replace(/\.html$/, "") || "index";
+
+ function el(tag, attrs, parent) {
+ var e = document.createElementNS(NS, tag);
+ for (var k in attrs) e.setAttribute(k, attrs[k]);
+ if (parent) parent.appendChild(e);
+ return e;
+ }
+ function href(n, g) {
+ if (n.site !== g.site && g.bases && g.bases[n.site]) return g.bases[n.site] + n.page + ".html#" + n.div;
+ if (n.url) return n.url;
+ if (n.site !== g.site) return null; // a site whose graph has no base yet: no link beats a broken one
+ return (n.page === page ? "" : n.page + ".html") + "#" + n.div;
+ }
+ function clip(s) { return s.length > 30 ? s.slice(0, 29) + "…" : s; }
+ function tip(n, g) {
+ return (NAME[n.kind] || n.kind) + ": " + n.title +
+ (n.site !== g.site ? " (" + n.site + ")" : n.external ? " (another site)" : "");
+ }
+
+ /* Draw `levels` (top to bottom; arrays of nodes) with `edges` ([prereq, dependent] key pairs).
+ A level wider than PER_ROW wraps onto further rows. `compact` draws unlabeled boxes. */
+ function draw(levels, edges, focus, g, compact) {
+ var D = compact ? COMPACT : LABELED, W = D.W, H = D.H, GX = D.GX, GY = D.GY, PER_ROW = D.PER_ROW;
+ var rows = [];
+ levels.forEach(function (l) {
+ for (var i = 0; i < l.length; i += PER_ROW) rows.push(l.slice(i, i + PER_ROW));
+ });
+ var cols = Math.max.apply(null, rows.map(function (r) { return r.length; }));
+ var w = cols * (W + GX) - GX, h = rows.length * (H + GY) - GY;
+ var uid = "dg-arrow-" + (draw.n = (draw.n || 0) + 1);
+ var svg = el("svg", { viewBox: "0 0 " + w + " " + h, width: w, role: "img",
+ "aria-label": "Prerequisites above, postrequisites below" }), pos = {};
+ var defs = el("defs", {}, svg);
+ var mk = el("marker", { id: uid, viewBox: "0 0 10 10", refX: 9, refY: 5, markerWidth: compact ? 4 : 6,
+ markerHeight: compact ? 4 : 6, orient: "auto-start-reverse" }, defs);
+ el("path", { d: "M0 0L10 5L0 10z", fill: "#888" }, mk);
+ rows.forEach(function (r, i) {
+ var off = (w - (r.length * (W + GX) - GX)) / 2;
+ r.forEach(function (n, j) { pos[n.id] = { x: off + j * (W + GX), y: i * (H + GY) }; });
+ });
+ edges.forEach(function (e) {
+ var a = pos[e[0]], b = pos[e[1]];
+ if (!a || !b) return;
+ var x1 = a.x + W / 2, y1 = a.y + H, x2 = b.x + W / 2, y2 = b.y, my = (y1 + y2) / 2;
+ el("path", { d: "M" + x1 + " " + y1 + "C" + x1 + " " + my + " " + x2 + " " + my + " " + x2 + " " + y2,
+ fill: "none", stroke: "#888", "stroke-width": compact ? 0.6 : 1.2, "stroke-opacity": compact ? 0.5 : 1,
+ "marker-end": "url(#" + uid + ")" }, svg);
+ });
+ rows.forEach(function (r) {
+ r.forEach(function (n) {
+ var p = pos[n.id];
+ var h = href(n, g);
+ var a = el("a", h === null ? {} : { href: h }, svg);
+ var attrs = { x: p.x, y: p.y, width: W, height: H, rx: compact ? 3 : 6, fill: COLOR[n.kind] || "#555",
+ stroke: n.id === focus ? "#000" : "#fff", "stroke-width": n.id === focus ? 3 : 1 };
+ if (n.external) attrs["stroke-dasharray"] = "4 2";
+ el("rect", attrs, a);
+ var label = tip(n, g);
+ el("title", {}, a).textContent = label;
+ a.setAttribute("aria-label", label);
+ if (!compact) {
+ var t = el("text", { x: p.x + 8, y: p.y + H / 2 + 4, "font-size": 12, fill: "#fff" }, a);
+ t.textContent = clip(n.title);
+ }
+ });
+ });
+ return svg;
+ }
+
+ function legend(kinds, compact) {
+ var p = document.createElement("p");
+ p.style.cssText = "font-size:0.85em;margin:0.4em 0";
+ Object.keys(NAME).filter(function (c) { return kinds[c]; }).forEach(function (c) {
+ var sw = document.createElement("span");
+ sw.style.cssText = "display:inline-block;width:0.9em;height:0.9em;border-radius:3px;margin:0 0.3em 0 0.9em;" +
+ "vertical-align:-0.1em;background:" + COLOR[c];
+ p.appendChild(sw);
+ p.appendChild(document.createTextNode(NAME[c]));
+ });
+ var note = document.createElement("span");
+ note.style.cssText = "display:block;margin-top:0.2em";
+ note.textContent = (compact ? "Hover a box for its name; click it to open the page. " : "") +
+ "Arrows point from what is used to what uses it. A dashed box is on another site.";
+ p.appendChild(note);
+ return p;
+ }
+
+ function neighbors(adj, start, depth) {
+ var dist = {}, queue = [start];
+ dist[start] = 0;
+ while (queue.length) {
+ var v = queue.shift();
+ if (dist[v] >= depth) continue;
+ (adj[v] || []).forEach(function (w) { if (!(w in dist)) { dist[w] = dist[v] + 1; queue.push(w); } });
+ }
+ return dist;
+ }
+
+ function perDiv(g, nodes, uses, usedBy) {
+ Object.keys(nodes).forEach(function (k) {
+ var n = nodes[k];
+ if (n.site !== g.site || n.page !== page) return;
+ var host = document.getElementById(n.div);
+ if (!host || (!(uses[k] || []).length && !(usedBy[k] || []).length)) return;
+ var pre = neighbors(uses, k, DEPTH), post = neighbors(usedBy, k, DEPTH);
+ var levels = [], d;
+ for (d = DEPTH; d >= 1; d--) levels.push(Object.keys(pre).filter(function (x) { return pre[x] === d; }));
+ levels.push([k]);
+ for (d = 1; d <= DEPTH; d++) levels.push(Object.keys(post).filter(function (x) { return post[x] === d; }));
+ levels = levels.filter(function (l) { return l.length; }).map(function (l) { return l.map(function (x) { return nodes[x]; }); });
+ var ids = {};
+ levels.forEach(function (l) { l.forEach(function (x) { ids[x.id] = 1; }); });
+ var edges = g.edges.filter(function (e) { return ids[e[0]] && ids[e[1]]; }).map(function (e) { return [e[1], e[0]]; });
+ var det = document.createElement("details");
+ det.className = "dependency-graph";
+ var sum = document.createElement("summary");
+ sum.textContent = "Dependencies (" + (Object.keys(pre).length - 1) + " prerequisites, " +
+ (Object.keys(post).length - 1) + " postrequisites, up to " + DEPTH + " levels)";
+ det.appendChild(sum);
+ var kinds = {};
+ levels.forEach(function (l) { l.forEach(function (x) { kinds[x.kind] = 1; }); });
+ det.appendChild(legend(kinds, false));
+ var drawn = false;
+ det.addEventListener("toggle", function () {
+ if (det.open && !drawn) { drawn = true; var s = document.createElement("div"); s.style.overflowX = "auto";
+ s.appendChild(draw(levels, edges, k, g, false)); det.appendChild(s); }
+ });
+ host.appendChild(det);
+ });
+ }
+
+ /* Rows of a graph over `keys`: a div sits one row below the lowest div it uses.
+ `uses` maps a key to the keys it uses; a cycle is cut where it is first entered. */
+ function layers(keys, nodes, uses) {
+ var inSet = {}, level = {};
+ keys.forEach(function (k) { inSet[k] = 1; });
+ function lv(k, seen) {
+ if (k in level) return level[k];
+ if (seen[k]) return 0;
+ seen[k] = 1;
+ var m = 0;
+ (uses[k] || []).forEach(function (p) { if (inSet[p]) m = Math.max(m, lv(p, seen) + 1); });
+ return (level[k] = m);
+ }
+ keys.forEach(function (k) { lv(k, {}); });
+ var levels = [];
+ keys.slice().sort().forEach(function (k) { (levels[level[k]] = levels[level[k]] || []).push(nodes[k]); });
+ return levels.filter(Boolean);
+ }
+
+ function foldedGraph(host, summary, levels, edges, g, compact) {
+ var kinds = {};
+ levels.forEach(function (l) { l.forEach(function (x) { kinds[x.kind] = 1; }); });
+ var det = document.createElement("details");
+ det.className = "dependency-graph";
+ var sum = document.createElement("summary");
+ sum.textContent = summary;
+ det.appendChild(sum);
+ if (compact) det.appendChild(legend(kinds, true));
+ var drawn = false;
+ det.addEventListener("toggle", function () {
+ if (det.open && !drawn) { drawn = true; var s = document.createElement("div"); s.style.overflowX = "auto";
+ s.appendChild(draw(levels, edges, null, g, compact)); det.appendChild(s); }
+ });
+ host.appendChild(det);
+ return det;
+ }
+
+ /* Optional: an element with id "dependency-graph-page" gets a folded graph of every
+ div on the page, prerequisites at the top. */
+ function wholePage(g, nodes, uses) {
+ var host = document.getElementById("dependency-graph-page");
+ if (!host) return;
+ var mine = Object.keys(nodes).filter(function (k) { return nodes[k].site === g.site && nodes[k].page === page; });
+ if (!mine.length) return;
+ var ids = {};
+ mine.forEach(function (k) { ids[k] = 1; });
+ var edges = g.edges.filter(function (e) { return ids[e[0]] && ids[e[1]]; }).map(function (e) { return [e[1], e[0]]; });
+ foldedGraph(host, "Dependencies of every definition and result on this page (" + mine.length + ")",
+ layers(mine, nodes, uses), edges, g, false);
+ }
+
+ /* Draw the whole of `g` (a merged graph) into `host`, unlabeled and unfolded. */
+ function tree(host, g, nodes, uses, keys) {
+ var ids = {};
+ keys.forEach(function (k) { ids[k] = 1; });
+ var edges = g.edges.filter(function (e) { return ids[e[0]] && ids[e[1]]; }).map(function (e) { return [e[1], e[0]]; });
+ var levels = layers(keys, nodes, uses), kinds = {};
+ keys.forEach(function (k) { kinds[nodes[k].kind] = 1; });
+ var p = document.createElement("p");
+ p.textContent = keys.length + " definitions and results, " + edges.length + " dependencies, " + levels.length + " levels.";
+ host.appendChild(p);
+ host.appendChild(legend(kinds, true));
+ var s = document.createElement("div");
+ s.style.overflowX = "auto";
+ s.appendChild(draw(levels, edges, null, g, true));
+ host.appendChild(s);
+ }
+
+ /* An element with id "dependency-graph-site" gets a tree of every div on this site. */
+ function wholeSite(g, nodes, uses) {
+ var host = document.getElementById("dependency-graph-site");
+ if (!host) return;
+ var mine = Object.keys(nodes).filter(function (k) { return nodes[k].site === g.site && !nodes[k].external; });
+ tree(host, g, nodes, uses, mine);
+ }
+
+ /* An element with id "dependency-graph-all" and a data-json list of several sites' graphs
+ gets one tree of all of them: a node a site only links to (external) is replaced by the
+ real node from the site that defines it. */
+ function allSites(host) {
+ var urls = (host.getAttribute("data-json") || "").split(",").map(function (u) { return u.trim(); }).filter(Boolean);
+ Promise.all(urls.map(function (u) {
+ return fetch(u).then(function (r) { return r.json(); }).catch(function () { return null; });
+ })).then(function (all) {
+ var nodes = {}, seen = {}, edges = [], bases = {}, uses = {};
+ all.filter(Boolean).forEach(function (j) {
+ bases[j.site] = j.base;
+ j.nodes.forEach(function (n) { if (!nodes[n.id] || (nodes[n.id].external && !n.external)) nodes[n.id] = n; });
+ j.edges.forEach(function (e) { var key = e[0] + " " + e[1]; if (!seen[key]) { seen[key] = 1; edges.push(e); } });
+ });
+ var keys = Object.keys(nodes);
+ if (!keys.length) return;
+ edges.forEach(function (e) { (uses[e[0]] = uses[e[0]] || []).push(e[1]); });
+ tree(host, { site: "", edges: edges, bases: bases }, nodes, uses, keys);
+ });
+ }
+
+ var all = document.getElementById("dependency-graph-all");
+ if (all) allSites(all);
+ fetch(base + "dependency-graph.json").then(function (r) { return r.json(); }).then(function (g) {
+ var nodes = {}, uses = {}, usedBy = {};
+ g.nodes.forEach(function (n) { nodes[n.id] = n; });
+ g.edges.forEach(function (e) {
+ (uses[e[0]] = uses[e[0]] || []).push(e[1]);
+ (usedBy[e[1]] = usedBy[e[1]] || []).push(e[0]);
+ });
+ g.bases = {};
+ perDiv(g, nodes, uses, usedBy);
+ wholePage(g, nodes, uses);
+ wholeSite(g, nodes, uses);
+ }).catch(function () { /* the graph is an extra; a missing file leaves the page as it was */ });
+})();
diff --git a/dependency-tree.qmd b/dependency-tree.qmd
new file mode 100644
index 00000000..73bc5330
--- /dev/null
+++ b/dependency-tree.qmd
@@ -0,0 +1,22 @@
+---
+title: "Dependency Tree"
+format:
+ html:
+ # The tree is drawn in the browser, so the page is HTML only,
+ # as lds's all-notes tree is.
+ # Only this page loads the script: the chapters/ pages reuse some of
+ # the same ids, so a per-div graph there would point at the wrong page.
+ include-after-body:
+ - text: ''
+---
+
+# How to read the tree {.unnumbered}
+
+Every definition and [theorem](proof-writing.qmd#def-theorem) on the Math Reference pages is one box, colored by kind.
+A box sits below each definition and theorem it uses,
+so the ones that use no others are at the top.
+Hover over a box to see its name,
+and click it to open its page.
+
+::: {#dependency-graph-site}
+:::
diff --git a/tools/build_dependency_graph.py b/tools/build_dependency_graph.py
new file mode 100644
index 00000000..28dc08db
--- /dev/null
+++ b/tools/build_dependency_graph.py
@@ -0,0 +1,250 @@
+#!/usr/bin/env python3
+# check-one-function-per-file: allow-multiple
+"""Build the prerequisite graph of a notes site's definitions and results.
+
+Parses every `#def-`, `#thm-`, `#lem-`, `#prp-` and `#cor-` div in
+`//*.qmd` (`chapters` by default; following `{{< include >}}` subfiles) and records the
+other such divs each one uses, through an `@id` cross-reference or a link to
+`page.qmd#id` / `page.html#id` / a cross-site URL. An edge A -> B means
+"A uses B", so B is a prerequisite of A and A is a postrequisite of B.
+
+Writes JSON (default `/dependency-graph.json`) and prints cycles and
+forward references (a div that uses one defined later on the same page).
+Stdlib only, so it can run in any notes repo's pre-render step.
+
+ python3 tools/build_dependency_graph.py [--root .] [--pages chapters] [--out FILE] [--site lds] [--fail]
+"""
+import argparse
+import json
+import re
+import sys
+from pathlib import Path
+
+KINDS = ("def", "thm", "lem", "prp", "cor")
+DIV_OPEN = re.compile(r"^(:{3,})\s*\{[^}]*#((?:%s)-[A-Za-z0-9_-]+)[^}]*\}\s*$" % "|".join(KINDS))
+DIV_ANY = re.compile(r"^(:{3,})(?:\s*\{.*\}|\s*\S+)?\s*$")
+INCLUDE = re.compile(r"\{\{<\s*include\s+(\S+?)\s*>\}\}")
+AT_REF = re.compile(r"(?]*?)#((?:%s)-[A-Za-z0-9_-]+)>?[^)]*\)" % "|".join(KINDS))
+URL_SITE = re.compile(r"https?://[^/]+/([^/]+)/([^/#?]+?)\.(?:html|qmd)$")
+PROOF_OPEN = re.compile(r"^:{3,}\s*(?:proof|(\{[^}]*\}))\s*$")
+PROOF_CLASS = re.compile(r"[{\s]\.proof(?![\w-])")
+QUOTED = re.compile(r"\"[^\"]*\"|'[^']*'")
+
+
+def is_proof_open(line):
+ """True for a bare `::: proof` or a brace form with an exact .proof class token."""
+ m = PROOF_OPEN.match(line)
+ if not m:
+ return False
+ attrs = m.group(1)
+ return attrs is None or bool(PROOF_CLASS.search(QUOTED.sub('""', attrs)))
+HEADING = re.compile(r"^#{2,6}\s+(.*?)\s*(?:\{.*\})?\s*$")
+
+
+def expand(path, seen=()):
+ """Yield (line, source_path) of a .qmd with includes expanded in place."""
+ in_code = False
+ for line in path.read_text(encoding="utf-8").splitlines():
+ if line.lstrip().startswith("```"):
+ in_code = not in_code
+ m = None if in_code else INCLUDE.search(line)
+ if m and not line.lstrip().startswith("