[M3-1a] Combining marks break when base and mark land in different JuliaMono subsets

[williamdemeo]

Raised out of #24, where make font-audit caught it on a real page. It is a bug in the #17 font build, not in that page.

What happens

≈̇ — standard Agda notation, produced by agda-input.el's \~~., and the identity relation used throughout agda-algebras — renders in DejaVu Sans Mono instead of JuliaMono. Any base-plus-combining-mark cluster can hit this.

Both codepoints ship. They just ship in different files:

codepoint	shipped in
≈ U+2248	juliamono-text.woff2
combining dot U+0307	juliamono-symbols.woff2

Neither file contains both, and a browser cannot compose a grapheme cluster across two @font-face rules — sharing a font-family name does not help, because the cluster has to be shaped by a single font. So it falls back to whichever system font has both, which is exactly the substitution make font-audit exists to fail on.

Confirmed in a browser, not inferred

Measured with the repo's own _browser.mjs over HTTP, asking Chromium which face it actually rasterised with:

cluster	base and mark	result
⊫ U+22AB + U+0307	both in symbols	JuliaMono
⊨ U+22A8 + U+0307	both in symbols	JuliaMono
≈ U+2248 + U+0307	split across files	DejaVu Sans Mono
≈ alone	text file	JuliaMono
⊫ alone	symbols file	JuliaMono

Same-file clusters compose; the split one does not. That isolates the cause to the subset split rather than to a missing glyph or to JuliaMono's repertoire.

A false start worth recording, because it is an easy trap when reproducing this: testing the combining mark "alone" by putting it after a space proves nothing, since space is itself in the text file and space-plus-mark is also a split cluster. It looks like a missing glyph and is not.

Why it happens

build_fonts.py splits JuliaMono three ways by Unicode block. Combining Diacritical Marks is in SYMBOL_BLOCKS, so every combining mark goes to the symbols subset. But some plausible bases are in the text subset — ≈ is in the hand-listed PROSE core, which exists precisely to put common-in-running-text characters in the always-loaded file. Any base in PROSE (or in ASCII, or in TEXT_BLOCKS) combined with any mark is therefore unshapeable.

This is a near-relative of the bug ADR-005 already records — the first subset was a character list and silently missed ℓ, Π and the subscript digits. Same lesson, one level up: a subset can be correct character-by-character and still wrong, because shaping operates on clusters, not codepoints.

Suggested fix

Ship the combining blocks in every JuliaMono subset rather than only in symbols. Combining Diacritical Marks (U+0300–U+036F) and Combining Diacritical Marks for Symbols are small — well under a kilobyte of outlines between them — so duplicating them across the three files costs almost nothing and removes the entire class of failure, in the same spirit as shipping whole blocks rather than character lists.

Worth checking at the same time whether any base character can appear in two subsets, which would be the mirror-image problem.

Tasks

• Add the combining blocks to all three JuliaMono charsets in scripts/python/build_fonts.py.
• Regenerate with make fonts and commit the rebuilt WOFF2 files.
• Confirm make fonts-check is clean afterwards.
• Add ≈̇ (and one other base+mark cluster with the base in PROSE) to the font-audit probe set, so a regression fails rather than waits for a content page to trip it.
• Restore the V-id1 signature on docs/projects/agda-algebras.md, which [M4-2] agda-algebras project page #24 rewrote as prose to get around this.

Acceptance criteria

• ≈̇ renders in JuliaMono, verified by make font-audit rather than by eye.
• make font-audit covers at least one split-subset cluster in its probe set.
• Total shipped font weight does not grow materially.

Notes

Not urgent for correctness of what is published today: #24 avoids the one cluster it needed, and no other page currently uses a combining sequence — checked across docs/. It will bite the next Agda-heavy page, which is #25 and #71 territory.