Skip to content

Commit cf6ce25

Browse files
authored
Merge pull request #455 from facebookresearch/fix/explorer-math
Typeset the TeX the dependency explorer draws
2 parents 7677dbf + a8e753f commit cf6ce25

10 files changed

Lines changed: 293 additions & 123 deletions

File tree

‎.github/workflows/tests.yml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,10 +51,23 @@ jobs:
5151
run: uv sync --frozen --extra dev --extra browser
5252
- name: Install WebKit and Linux system dependencies
5353
run: uv run --frozen --extra browser playwright install --with-deps webkit
54+
# The explorer's typesetting runs the real MathJax, served in place of
55+
# the CDN from the same checked tarball as the MathJax job's.
56+
- name: Install pinned MathJax 3.2.2
57+
run: |
58+
set -euo pipefail
59+
timeout --signal=TERM --kill-after=15s 2m curl -sSfL \
60+
https://registry.npmjs.org/mathjax/-/mathjax-3.2.2.tgz -o mathjax.tgz
61+
echo "1b9c0a1c44df864e915690558e72adb9cc5203360daefd385084ced3b6c64c09 mathjax.tgz" \
62+
| sha256sum --check --strict
63+
mkdir mathjax
64+
tar xzf mathjax.tgz -C mathjax
65+
echo "AUTOFORM_MATHJAX_DIR=$PWD/mathjax/package" >> "$GITHUB_ENV"
5466
- name: Run dependency explorer browser regressions
5567
run: uv run --frozen --extra dev --extra browser pytest -q tests/test_dag_viewer_browser.py
5668
env:
5769
AUTOFORM_REQUIRE_BROWSER_TESTS: "1"
70+
AUTOFORM_REQUIRE_MATHJAX_TESTS: "1"
5871

5972
mathjax:
6073
name: MathJax read-back cards (Node)

‎CHANGELOG.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,11 @@ date when the release is tagged.
3838
articles that proof uses, and keeps the source's route in the proof sketch,
3939
so the article is not blocked on steps its proof never needs; Agent Review
4040
checks the same (#443).
41+
- **Dependency explorer.** The rail and the details typeset the TeX in titles
42+
and summaries, with the articles' input and the project's macros, where the
43+
explorer's own MathJax calls had typeset nothing on a generated site. Map
44+
cards, the Contents list, search and the explorer's head still show a title
45+
as typed (#455).
4146

4247
## 0.6.0 (2026-10-22)
4348

‎CONTRIBUTING.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,9 @@ each `AUTOFORM_REQUIRE_*` variable below, so it fails where a local run skips:
1919

2020
- Browser tests skip without the `browser` extra and WebKit; `make test-browser`
2121
installs both and runs them as CI does (`AUTOFORM_REQUIRE_BROWSER_TESTS=1`).
22-
- MathJax read-back card tests skip unless `node` is on `PATH` and
23-
`AUTOFORM_MATHJAX_DIR` names an unpacked MathJax 3.2.2 package
24-
(`AUTOFORM_REQUIRE_MATHJAX_TESTS=1`).
22+
- MathJax tests skip unless `AUTOFORM_MATHJAX_DIR` names an unpacked MathJax
23+
3.2.2 package, and the Node ones unless `node` is on `PATH`; CI's MathJax and
24+
WebKit jobs unpack it (`AUTOFORM_REQUIRE_MATHJAX_TESTS=1`).
2525
- Lean tests skip without `lake` on `PATH`, and most without the toolchain in
2626
`tests/fixtures/skeleton-project/lean-toolchain`, which only the real-Lake
2727
test in `tests/test_project_inspect.py` lets elan download

‎autoform_cli/README.md‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1044,11 +1044,11 @@ projection uses the same JSON-derived explorer. A formal statement links to the
10441044
smallest scope holding it, as `<scope>.html#node=<id>`; only a legacy
10451045
`dependencies/full.html#node=<id>` link redirects. A `lean:` declaration that
10461046
resolves to a repository permalink gets a source link; a catalog's Lean row
1047-
shows its first eight names and counts the rest. The explorer shows a title as
1048-
typed, and render percent-encodes each link it writes from file and folder
1049-
names, such as the book's previous and next links, while a Markdown link it
1050-
moves keeps its decoded spelling and starts with `./` when its first segment
1051-
holds a colon, so no name can make a `javascript:` URL.
1047+
shows its first eight names and counts the rest. The explorer typesets only the
1048+
TeX in its rail's and details' titles and summaries. Render percent-encodes each
1049+
link it writes from file and folder names, such as the book's previous and next
1050+
links; a Markdown link it moves keeps its decoded spelling and starts with `./`
1051+
when its first segment holds a colon, so no name can make a `javascript:` URL.
10521052

10531053
Render writes no Mermaid graph of its own. Authored Mermaid remains supported in
10541054
the vault and book, drawn in strict mode with plain-text labels and loaded only
@@ -1107,12 +1107,12 @@ do nothing, however a formula or macro reaches them. A macro may not take one of
11071107
their names; `check` and `render` warn about a macro they leave out, judging the
11081108
copy of `tex-macros.json` that `render` reads once and publishes. Each read-back
11091109
card has its own TeX input with only base, ams, and noundefined. Only formulas
1110-
the site's Markdown marks, such as `$...$` or `$$...$$` in an article, are
1111-
typeset; a statement's heading title, a `discussion:` value, the home page's
1112-
lead, the navigation, and a table of contents show as typed. A formula paints
1113-
only within its own line and block, and an inline formula wider than its
1114-
paragraph is cut at its edge, so write one that wide as a display, which
1115-
scrolls.
1110+
the site's Markdown marks, such as `$...$`, and the explorer's rail and details
1111+
titles and summaries are typeset, with no MathJax tab stop or menu in a link or
1112+
button; a heading's title, a `discussion:` value, the home page's lead, the
1113+
navigation, and a table of contents show as typed. A formula paints only within
1114+
its own line and block, and an inline formula wider than its paragraph is cut at
1115+
its edge, so write one that wide as a display, which scrolls.
11161116

11171117
### Upgrading from an earlier Autoform
11181118

‎autoform_cli/dag_viewer.py‎

Lines changed: 30 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919

2020
from .graph_views import FLATTENED_ROLES, INVENTORY_STATUSES, GraphView, ViewNode
2121
from .lean import declaration_names
22+
from .markdown import FORMULA_CLASS
2223
from .status import INVENTORY_STATES, MEANINGS, STATES
2324

2425
SCHEMA = "autoform-dag-view/v2"
@@ -482,7 +483,7 @@ def viewer_script() -> str:
482483
# that browsers do not need. Internal spaces and the line breaks between
483484
# code lines stay intact.
484485
# Whole-line comments explain the source, not the page, so they stay here.
485-
lines = (line.lstrip() for line in _SCRIPT.splitlines())
486+
lines = (line.lstrip() for line in _SCRIPT.replace("FORMULA_CLASS_JSON", json.dumps(FORMULA_CLASS)).splitlines())
486487
return "\n".join(line for line in lines if line and not line.startswith("//")) + "\n"
487488

488489

@@ -602,6 +603,7 @@ def viewer_script() -> str:
602603
.bp-dag-filter-popover fieldset + fieldset { margin-top: 8px; padding-top: 8px; border-top: 1px solid var(--dag-border); }
603604
.bp-dag-filter-popover legend { margin-bottom: 6px; }
604605
.bp-dag-filter-popover legend, .bp-dag-viewer.bp-dag-viewer .bp-dag-navigation-group h2 { color: var(--dag-muted); font-size: 11px; font-weight: 600; letter-spacing: .06em; line-height: 1.3; text-transform: uppercase; }
606+
.bp-dag-viewer mjx-container { text-transform: none; }
605607
.bp-dag-check { display: flex; align-items: center; gap: 7px; min-height: 32px; padding: 3px 5px; border-radius: var(--dag-radius-row); }
606608
.bp-dag-check:hover { background: var(--dag-panel); }
607609
.bp-dag-check input { accent-color: var(--dag-link); }
@@ -759,6 +761,9 @@ def viewer_script() -> str:
759761
if (window.__AUTOFORM_DAG_VIEWER_V2__) return;
760762
window.__AUTOFORM_DAG_VIEWER_V2__ = true;
761763
764+
// The class of the site's formulas: the authored titles and summaries the
765+
// rail and the details draw carry it, so the site's MathJax typesets them.
766+
var TEX = FORMULA_CLASS_JSON;
762767
var NODE_W = 196, NODE_H = 56, MAX_MAP_NODES = 120, LIST_PAGE = 100;
763768
var SEARCH_PAGE = 50, RELATION_PAGE = 50, MIN_SCALE = .002, MIN_READABLE_SCALE = .8, MIN_ATLAS_SCALE = .68, hostSequence = 0;
764769
var clamp = function (value, low, high) { return Math.max(low, Math.min(high, value)); };
@@ -979,32 +984,29 @@ def viewer_script() -> str:
979984
if (refs.ctx.font.indexOf("11px") < 0) family = "sans-serif";
980985
}
981986
982-
function trailList(entries, className) {
987+
function trailList(entries, className, tex) {
983988
var list = element("ol", className);
984989
entries.forEach(function (entry, index) {
985-
var item = element("li"), href = safeHref(entry.url);
990+
// The class goes on the element that holds the text: the link, when there is one.
991+
var href = safeHref(entry.url), item = element("li", href ? "" : tex);
986992
item.title = entry.label;
987-
if (href) { var link = element("a", "", entry.label); link.href = href; link.title = entry.label; item.appendChild(link); }
993+
if (href) { var link = element("a", tex, entry.label); link.href = href; link.title = entry.label; item.appendChild(link); }
988994
else { item.textContent = entry.label; if (!className && index === entries.length - 1) item.setAttribute("aria-current", "page"); }
989995
list.appendChild(item);
990996
});
991997
return list;
992998
}
993-
// MathJax typesets authored TeX after the calling render, forgetting the old math first.
994-
function typeset(container) {
995-
var M = window.MathJax;
996-
if (!M || !M.typesetPromise) return;
997-
M.typesetClear([container]);
998-
M.startup.promise = M.startup.promise.then(function () { return M.typesetPromise([container]); }).catch(function () {});
999-
}
999+
// The site's javascripts/mathjax.js typesets the text marked TEX as it does articles' formulas, after the
1000+
// calling render; before MathJax starts, its first pass reads it.
1001+
function typeset() { document.dispatchEvent(new Event("autoform:typeset")); }
10001002
function renderNavigation() {
10011003
if (!refs.navigationInner) return;
1002-
typeset(refs.navigationInner); refs.navigationInner.textContent = ""; refs.navigationNodes = new Map();
1004+
typeset(); refs.navigationInner.textContent = ""; refs.navigationNodes = new Map();
10031005
if (intro) { if (!state.introInSheet) refs.navigationInner.appendChild(intro); } else {
10041006
// The h1 names the current scope, so the rail's trail lists only its ancestors.
1005-
if (trail.length > 1) refs.navigationInner.appendChild(trailList(trail.slice(0, -1), "bp-dag-navigation-path"));
1006-
refs.navigationInner.appendChild(element("h1", "bp-dag-navigation-title", data.title || "Mathematics"));
1007-
if (view.summary) refs.navigationInner.appendChild(element("p", "bp-dag-navigation-summary", view.summary));
1007+
if (trail.length > 1) refs.navigationInner.appendChild(trailList(trail.slice(0, -1), "bp-dag-navigation-path", TEX));
1008+
refs.navigationInner.appendChild(element("h1", "bp-dag-navigation-title " + TEX, data.title || "Mathematics"));
1009+
if (view.summary) refs.navigationInner.appendChild(element("p", "bp-dag-navigation-summary " + TEX, view.summary));
10081010
refs.navigationInner.appendChild(element("p", "bp-dag-navigation-counts", plural(data.nodes.length, atlas ? "topic" : "item",
10091011
atlas ? "topics" : "items") + " · " + plural(data.edge_count || data.edges.length, "dependency", "dependencies")));
10101012
}
@@ -1016,7 +1018,7 @@ def viewer_script() -> str:
10161018
});
10171019
groups.forEach(function (nodes, label) {
10181020
var section = element("section", "bp-dag-navigation-group");
1019-
if (groups.size > 1) section.appendChild(element("h2", "", label));
1021+
if (groups.size > 1) section.appendChild(element("h2", TEX, label));
10201022
var list = element("ul", "bp-dag-navigation-list");
10211023
nodes.forEach(function (node) {
10221024
var item = element("li"), href = safeHref(node.url), control;
@@ -1026,7 +1028,7 @@ def viewer_script() -> str:
10261028
control.addEventListener("click", function () { activateNode(node, true); });
10271029
}
10281030
control.dataset.navigationNodeId = node.id;
1029-
control.appendChild(element("span", "", node.title));
1031+
control.appendChild(element("span", TEX, node.title));
10301032
// A scope counts its items; a leaf shows its status as a swatch, so the rows end evenly.
10311033
var mark = node.kind === "scope" ? element("span", "bp-dag-navigation-meta", (node.member_count || 0).toLocaleString()) : swatch(node.status);
10321034
if (node.kind !== "scope") { mark.title = statusLabel(node.status); mark.setAttribute("role", "img"); mark.setAttribute("aria-label", mark.title); }
@@ -1138,7 +1140,7 @@ def viewer_script() -> str:
11381140
var section = element("section", "bp-dag-section"), list = element("div", "bp-dag-distribution");
11391141
section.appendChild(element("h3", "", title));
11401142
rows.forEach(function (row) {
1141-
var line = element("div", "bp-dag-distribution-row"), name = element("span", "bp-dag-distribution-label");
1143+
var line = element("div", "bp-dag-distribution-row"), name = element("span", "bp-dag-distribution-label " + TEX);
11421144
if (row[2]) name.appendChild(swatch(row[2]));
11431145
name.appendChild(document.createTextNode(row[0])); line.appendChild(name);
11441146
line.appendChild(element("span", "", String(row[1]))); list.appendChild(line);
@@ -1705,11 +1707,13 @@ def viewer_script() -> str:
17051707
}
17061708
17071709
function renderInspector() {
1708-
typeset(refs.inspector); refs.inspectorInner.textContent = ""; refs.sheetHandle.textContent = state.selected ? state.selected.title : introTitle || "Graph details";
1710+
typeset(); refs.inspectorInner.textContent = ""; refs.sheetHandle.textContent = state.selected ? state.selected.title : introTitle || "Graph details";
1711+
// The handle repeats a node's title; the landing page's title it shows otherwise is printed as typed.
1712+
refs.sheetHandle.classList.toggle(TEX, !!state.selected);
17091713
if (!state.selected) {
17101714
if (intro) { if (state.introInSheet) refs.inspectorInner.appendChild(intro); } else {
1711-
refs.inspectorInner.appendChild(element("h2", "", data.title || "Dependencies"));
1712-
if (view.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary", view.summary));
1715+
refs.inspectorInner.appendChild(element("h2", TEX, data.title || "Dependencies"));
1716+
if (view.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary " + TEX, view.summary));
17131717
}
17141718
var overview = element("p", "bp-dag-overview"); overview.appendChild(element("strong", "", plural(data.nodes.length, atlas ? "topic" : "node", atlas ? "topics" : "nodes")));
17151719
overview.appendChild(document.createTextNode(" · " + plural(data.edge_count || data.edges.length,
@@ -1731,8 +1735,8 @@ def viewer_script() -> str:
17311735
"Inventory statuses are neutral: an inventory records inspection, not a mathematical proof.")); return;
17321736
}
17331737
var node = state.selected, header = element("div", "bp-dag-inspector-header");
1734-
if (node.declaration) header.appendChild(element("p", "bp-dag-kicker", node.declaration + (node.area ? " · " + node.area : "")));
1735-
header.appendChild(element("h2", "", node.title));
1738+
if (node.declaration) header.appendChild(element("p", "bp-dag-kicker " + TEX, node.declaration + (node.area ? " · " + node.area : "")));
1739+
header.appendChild(element("h2", TEX, node.title));
17361740
var close = button("bp-dag-close", "×", "Close details"); close.addEventListener("click", function () {
17371741
// Hiding the details takes focus out of them; it returns to the selection, not to the page.
17381742
setSheet(false, state.selected);
@@ -1753,7 +1757,7 @@ def viewer_script() -> str:
17531757
}
17541758
if (node.lean) refs.inspectorInner.appendChild(element("p", "bp-dag-lean",
17551759
"Lean: " + node.lean + (node.lean_more ? " and " + node.lean_more + " more" : "")));
1756-
if (node.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary", node.summary));
1760+
if (node.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary " + TEX, node.summary));
17571761
if (node.kind === "scope" && node.internal_dependency_count) refs.inspectorInner.appendChild(element("p", "bp-dag-overview",
17581762
plural(node.internal_dependency_count, "authored dependency connects", "authored dependencies connect") + " results inside this topic."));
17591763
var before = prerequisites.get(node.id) || [], after = dependents.get(node.id) || [];
@@ -1786,14 +1790,14 @@ def viewer_script() -> str:
17861790
var next = Math.min(visible + RELATION_PAGE, ids.length);
17871791
ids.slice(visible, next).forEach(function (id) {
17881792
var related = byId.get(id); if (!related) return;
1789-
var item = element("li"), choose = button("bp-dag-relation-button", related.title);
1793+
var item = element("li"), choose = button("bp-dag-relation-button " + TEX, related.title);
17901794
choose.addEventListener("click", function () { activateNode(related, true); }); item.appendChild(choose); list.appendChild(item);
17911795
});
17921796
visible = next;
17931797
more.hidden = visible >= ids.length;
17941798
more.textContent = more.hidden ? "" : "Show " + Math.min(RELATION_PAGE, ids.length - visible) + " more";
17951799
}
1796-
more.addEventListener("click", function () { appendNextBatch(); typeset(list); }); appendNextBatch();
1800+
more.addEventListener("click", function () { appendNextBatch(); typeset(); }); appendNextBatch();
17971801
section.appendChild(list); section.appendChild(more); refs.inspectorInner.appendChild(section);
17981802
}
17991803

‎autoform_cli/markdown.py‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,9 @@
5959

6060
#: The class pymdownx.arithmatex gives each formula it finds in the site's
6161
#: Markdown. The page's MathJax reads these elements and no other text, so a
62-
#: title or the navigation shows its TeX as typed.
62+
#: title or the navigation shows its TeX as typed, but for the titles and
63+
#: summaries the dependency explorer draws in its rail and details, which it
64+
#: marks with this class.
6365
FORMULA_CLASS = "arithmatex"
6466

6567
#: The Markdown extensions the generated `mkdocs.yml` enables, and their

0 commit comments

Comments
 (0)