improved HTML rendering of the ASL Reference with MathJax

asllib/doc/Expressions.tex

@@ -853,7 +853,7 @@ \subsection{Abstract Syntax}
 We refer to a \rhsexpression{} of the form \verb|b[[i]]|,
 where $b, i$ are subexpressions, as an \arrayaccessterm\ expression.
 We refer to $b$ and $i$ as the \emph{base}
-and the $\emph{index}$ subexpressions, respectively.
+and the \emph{index} subexpressions, respectively.
 \end{definition}
 
 \ExampleDef{Array Access Expressions}

asllib/doc/Makefile

@@ -3,6 +3,10 @@ LATEX=pdflatex
 BIBTEX=bibtex
 
 GENERATED_MACROS_TEX=generated_macros.tex
+HEVEA_DIR=hevea
+MATHJAX_CONFIG_JS=HTML/ASL-mathjax-config.js
+HTML_STYLESHEET=$(HEVEA_DIR)/asl-html.css
+HEVEA_HTML_INPUTS=book.hva mathjaxauto.hva $(HEVEA_DIR)/mathjax_config.hva macros.hva ASLReference.tex
 
 all: ASLReference.pdf
 
@@ -21,12 +25,22 @@ ASLReference.pdf: generated_spec *.tex *.bib
 	fi
 	python3 doclint.py --console_macros --aslref $(ASLREF)
 
-html: generated_spec *.tex *.bib *.hva
+html: generated_spec *.tex *.bib *.hva $(HEVEA_DIR)/*.hva $(HEVEA_DIR)/generate_mathjax_config.py $(HTML_STYLESHEET)
 	mkdir -p HTML
-	hevea -fix0 -O -o HTML/ASL.html book.hva macros.hva ASLReference.tex
+	cp $(HTML_STYLESHEET) HTML/asl-html.css
+	@# The first run is expected to generate warnings because bibhva
+	@# and the second hevea pass have not run, so we silence them via -s.
+	@# MathJax mode intentionally omits -O: Esponja does not understand the raw
+	@# TeX fragments that HeVeA leaves for MathJax to typeset in the browser.
+	hevea -fix0 -s -o HTML/ASL.html $(HEVEA_HTML_INPUTS)
 	bibhva HTML/ASL
-	hevea -fix -O -o HTML/ASL.html book.hva macros.hva ASLReference.tex
+	@# bibhva makes citations available after the first pass; run one more
+	@# silent pass so the final unsilenced pass starts from stable references.
+	hevea -fix0 -s -o HTML/ASL.html $(HEVEA_HTML_INPUTS)
+	hevea -fix -o HTML/ASL.html $(HEVEA_HTML_INPUTS)
+	python3 $(HEVEA_DIR)/generate_mathjax_config.py $(MATHJAX_CONFIG_JS) HTML/ASL.html
 	cd HTML && hacha ASL.html
+	python3 $(HEVEA_DIR)/generate_mathjax_config.py $(MATHJAX_CONFIG_JS) HTML/ASL[0-9][0-9][0-9].html
 
 generated_spec: asl.spec
 	dune exec -- aslspec asl.spec --render;

asllib/doc/StandardLibrary.tex

@@ -2,7 +2,7 @@ \chapter{Standard Library\label{chap:StandardLibrary}}
 
 In addition to the operations, ASL provides some standard subprograms.
 The standard subprograms are available from the following address:
-\url{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}.
+\href{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}{\texttt{https://github.com/herd/herdtools7/blob/\VERSION/asllib/libdir/stdlib.asl}}.
 %
 The standard subprograms given there provide one way of implementing them.
 ASL implementations can implement the subprograms in any way that provides equivalent behaviour.

asllib/doc/hevea/README.md

@@ -0,0 +1,234 @@
+# ASL HTML HeVeA Support
+
+This directory contains the source-controlled support files for the ASL Reference HTML build. Generated files are written under `asllib/doc/HTML/` and
+should not be edited by hand.
+
+Run the build from `asllib/doc`:
+
+```sh
+make html
+```
+
+## Build Flow
+
+The `html` Makefile target:
+
+1. Generates `generated_macros.tex` from `asl.spec`.
+2. Runs HeVeA on `ASLReference.tex` with:
+   - `book.hva`
+   - `mathjaxauto.hva`
+   - `hevea/mathjax_config.hva`
+   - `macros.hva`
+3. Runs `bibhva` and additional HeVeA passes so citations and cross-references
+   settle.
+4. Runs `hevea/generate_mathjax_config.py` on the unsplit `HTML/ASL.html`.
+   This prepares the MathJax source in that file and writes
+   `HTML/ASL-mathjax-config.js`.
+5. Runs `hacha` to split `HTML/ASL.html` into chapter pages.
+6. Runs `generate_mathjax_config.py` again on the split `HTML/ASLNNN.html`
+   pages. This updates the generated MathJax configuration with the final
+   split-page anchor map and prepares MathJax source in each split page.
+
+The first HeVeA passes use `-s` because citations and references are expected
+to be incomplete until `bibhva` and the later HeVeA pass have run. The final
+HeVeA pass is not silenced.
+
+The HTML build intentionally omits HeVeA's `-O` optimization flag. MathJax mode
+leaves raw TeX fragments for the browser to typeset, and the optimizer does not
+understand those fragments reliably.
+
+## Files
+
+### `mathjax_config.hva`
+
+Overrides HeVeA's default MathJax hook.
+
+HeVeA's built-in `mathjax.hva` loads an older MathJax setup directly. This file instead injects:
+- `asl-html.css`, the ASL-specific stylesheet.
+- `ASL-mathjax-config.js`, generated by `generate_mathjax_config.py`.
+- MathJax from jsDelivr, pinned to an exact version and protected with Subresource Integrity (SRI).
+
+Keep this file small. Most ASL-specific behavior belongs in the generated MathJax config or in the stylesheet.
+
+#### MathJax Loading And Security
+
+The MathJax script is loaded from jsDelivr as:
+
+```html
+https://cdn.jsdelivr.net/npm/mathjax@4.0.0/tex-chtml.js
+```
+
+The URL intentionally pins the exact `4.0.0` release instead of using a rolling
+selector such as `mathjax@4`. A rolling selector is convenient, but the browser
+may receive different JavaScript when MathJax publishes a new 4.x release.
+
+The script tag also includes an SRI hash and `crossorigin="anonymous"`. SRI
+means the browser verifies the fetched script against the expected SHA-384
+digest and refuses to execute it if the CDN serves different content.
+
+This is the safest lightweight option for this build:
+
+- It avoids mutable CDN content by pinning the exact MathJax release.
+- It detects CDN tampering or unexpected content changes via SRI.
+- It avoids vendoring a large third-party MathJax distribution into the source
+  tree.
+
+Vendoring MathJax locally would remove the runtime CDN dependency entirely, but
+would add a substantial third-party asset tree to the repository. If this
+project later needs fully offline or CDN-free HTML, vendor the complete MathJax
+distribution and update `mathjax_config.hva` to load it from `HTML/` or another
+local path.
+
+When upgrading MathJax:
+
+1. Change the exact version in `mathjax_config.hva`.
+2. Recompute the SRI hash for the new `tex-chtml.js`.
+3. Update the `integrity` attribute.
+4. Rebuild with `make html`.
+5. Inspect representative formula-heavy pages.
+
+### `generate_mathjax_config.py`
+
+Prepares generated HTML pages for MathJax and writes
+`HTML/ASL-mathjax-config.js`.
+
+The script does several related jobs:
+
+- Reads macro definitions from:
+  - `ASLmacros.tex`
+  - `variable_name_macros.tex`
+  - `generated_macros.tex`
+- Converts simple LaTeX macro definitions into MathJax `configmacros` definitions.
+- Resolves simple `\let` aliases, such as `\OldEmptyset`, before translating macro bodies.
+- Provides manual MathJax definitions only for macros whose LaTeX definition is too complex, too PDF-specific, or visually unsuitable when translated directly.
+- Wraps MathJax source fragments in temporary placeholder elements so the page can show animated grey formula placeholders while MathJax typesets.
+- Moves `\hypertarget`, `\mathhypertarget`, and `\texthypertarget` out of
+  MathJax source and into static HTML anchors. MathJax should typeset formulas,
+  not create the document's structural anchors.
+- Rewrites some TeX constructs before MathJax sees them, such as `\verb`,
+  `\textfunc`, and `\inferrule` labels.
+- Builds a split-page anchor map after `hacha`, so generated MathJax hyperlinks
+  can point to the correct `ASLNNN.html#anchor` target.
+- Writes `HTML/ASL-mathjax-fallbacks.txt`, a diagnostic report for macro
+  translations that should be reviewed.
+
+#### Hyperlinks In MathJax Macros
+
+MathJax macro bodies use `#` for macro arguments, which conflicts with URL
+fragments such as `ASL011.html#type-ResultExpr`. The generator therefore writes
+the temporary sentinel `__ASL_HASH__` inside generated `\href` targets and emits
+JavaScript that repairs those links after MathJax creates real anchors.
+
+The repair code also runs on click, so links are corrected before navigation
+even if MathJax updates the DOM late.
+
+#### Placeholder Rendering
+
+The generated HTML wraps formula source in:
+
+- `span.asl-mathjax-pending.asl-mathjax-inline` for inline formulas.
+- `div.asl-mathjax-pending.asl-mathjax-display` for display formulas.
+
+`asl-html.css` renders those wrappers as animated grey placeholders. Once
+MathJax finishes, `ASL-mathjax-config.js` removes the pending class and the real
+formula becomes visible. A timeout fallback also removes the pending state if
+MathJax fails to load.
+
+#### Diagnostics
+
+`HTML/ASL-mathjax-fallbacks.txt` contains:
+
+- `Unknown Macro Fallbacks`: macros used in MathJax source but not defined by
+  MathJax or the generated config.
+- `Generic Operator Fallbacks`: argument-taking macros translated to generic
+  `\operatorname{name}(...)` forms.
+- `Suspicious Zero-Argument Macro Translations`: zero-argument macros whose
+  source definition looks symbolic but whose generated expansion fell back to
+  the macro name.
+
+The last section is intended to catch issues like a macro whose PDF rendering is `\geq_{\text{pure}}` but whose HTML rendering would otherwise become the text `puritygeq`.
+
+#### Macro Translation Maintenance
+
+Do not add a macro to `MANUAL_MACROS` if the generator can derive the same
+MathJax definition from the TeX source. The automatic translator handles the
+common one-line cases: linked symbols, `\let` aliases, simple text/style
+wrappers, simple superscript/subscript forms, and simple argument-taking
+operators.
+
+Keep an entry in `MANUAL_MACROS` when the direct TeX expansion is not the HTML
+rendering we want. Examples include:
+
+- Document-only helpers such as `\hva`, `\frontmatter`, and `\mainmatter`.
+- MathJax structural shims such as `\inferrule`, `\hyperlink`, and
+  `\mathhypertarget`.
+- Visual overrides where the PDF macro is technically valid TeX but looks poor
+  in MathJax, such as `\disjointunion`, `\parallelgraphs`, and empty-set
+  variants rendered with `\varnothing`.
+- Multi-line macros or layout-sensitive macros whose `[H]`/`[V]` branches would
+  require real TeX interpretation.
+
+When a TeX macro changes, rebuild and inspect `HTML/ASL-mathjax-fallbacks.txt`.
+If the generated definition is already correct, prefer improving the automatic
+translator over adding another manual entry.
+
+### `asl-html.css`
+
+Additional styling for the generated ASL HTML pages.
+
+This stylesheet is copied to `HTML/asl-html.css` by `make html`. It layers on
+top of the structural CSS emitted by HeVeA and should contain only ASL HTML
+presentation rules, such as:
+
+- Page typography and spacing.
+- Display-math overflow handling.
+- MathJax placeholder styling and animation.
+- Small ASL-specific visual rules, such as the red wrapped-line marker.
+
+Do not edit `HTML/asl-html.css` directly; edit this source file instead.
+
+## Generated Files
+
+The important generated files are:
+
+- `HTML/ASL.html`: the unsplit HeVeA output and `hacha` input.
+- `HTML/ASLNNN.html`: split chapter/section pages.
+- `HTML/index.html`: split HTML table of contents.
+- `HTML/ASL-mathjax-config.js`: generated MathJax configuration and runtime
+  repair code.
+- `HTML/ASL-mathjax-fallbacks.txt`: generated macro translation diagnostics.
+- `HTML/asl-html.css`: copy of `hevea/asl-html.css`.
+
+These files are regenerated by `make html`.
+
+## Common Maintenance Tasks
+
+When a formula shows a macro name rather than the intended symbol:
+
+1. Check `HTML/ASL-mathjax-fallbacks.txt`.
+2. If the macro appears in a fallback section, either improve the simple parser
+   in `generate_mathjax_config.py` or add a focused manual definition in
+   `MANUAL_MACROS`.
+3. Rebuild with `make html`.
+4. Inspect the affected `HTML/ASLNNN.html` page.
+
+When a MathJax hyperlink points to a bad URL:
+
+1. Check that the target has a real `id` in the split page.
+2. Check the generated macro in `HTML/ASL-mathjax-config.js`.
+3. If the URL contains `__ASL_HASH__` after clicking, review the link-repair
+   JavaScript in `generate_mathjax_config.py`.
+
+When raw LaTeX flashes before formulas render:
+
+1. Confirm the formula is wrapped in an `asl-mathjax-pending` element.
+2. Check `asl-html.css` placeholder styles.
+3. Check `finishAslMathJaxLoading()` in the generated config.
+
+## Constraints
+
+- Avoid adding new runtime or build dependencies unless they are really needed.
+- Keep generated artifacts under `HTML/`; keep source changes in this directory
+  or the LaTeX sources.
+- Prefer targeted manual MathJax definitions for hard PDF-specific macros over
+  broad parser changes that may affect unrelated output.