[M3-3c] The 404 as an open goal

[williamdemeo]

Closes #98 (M3-3c, from the 2026-08-03 design review).

What

overrides/404.html shadows Material's boilerplate not-found page — the same
custom_dir mechanism as overrides/partials/source.html — and turns the one
page every typo'd URL reaches into an unfillable Agda goal that names the
page the visitor asked for. Requesting, say, /cv/index.html.bak shows:

_ : ∃ cv/index.html.bak
_ = {! !}

-- The hole cannot be filled.  Try the index, or search.

set in JuliaMono, the hole wearing the accent tokens the way agda2-mode
paints an interactive hole green — and the comment line types itself
out below the goal, in editor green, a beat after the page paints.
Below the box, three ways out: index, projects, search. Search
is a real <button> dressed in the site's link clothes — Copilot's review
rightly flagged the earlier <label> as unreachable by Tab — and click,
Enter, and Space all open Material's overlay through the __search
checkbox and put the caret in the query field (Material only auto-focuses
it from its own s shortcut, so the button does that part explicitly;
verified with trusted CDP input on both layouts). (∃ cv/index.html.bak
is even parseable Agda — / is legal in a name, so the path reads as a
qualified identifier.)

Details that took deciding:

• The typing is CSS only, and honest about accessibility. The full
  sentence is in the DOM from the first byte; the animation is a
  steps(56) reveal over a clip-path (56 steps, 56 characters), so the
  box never changes size, screen readers never wait, prefers-reduced-motion
  shows the line standing whole (verified by emulation: zero animation
  objects), and below 45em — where the line must wrap and a horizontal
  reveal over two lines would be a curtain, not typing — the comment
  simply appears, wrapped. Verified against the animation timeline: it
  plays exactly once, starting at first paint + 0.8s, no restart.
• The comment is --, not # (it is an Agda comment), and it is
  green per scheme like the syntax colours in extra.css: dark carries the
  palette's own string green (12.5:1 on the raised surface); in light that
  token measures 4.59:1 there — thinner than anything else on the site —
  so light wears a deeper leaf of the same green at 6.0:1.
• The path is substituted at runtime, because it cannot exist at build
  time: GitHub Pages serves this one static file for every missing URL.
  Six lines of inline script write location.pathname into the goal —
  through textContent only (the path is attacker-chosen text and must
  never be parsed as markup), with encoded whitespace flattened so a crafted
  URL cannot re-shape the goal, long paths keeping their tail, and the
  static ThisPage standing when scripts are off. This is the page's only
  script; nothing moves or fetches.
• The box is the site's own wire-frame: the hairline-and-radius
  .highlight box every real Agda block wears, with the code at the same
  --type-code size — the block is supposed to read as authentic Agda, and
  authentic Agda on this site looks exactly like this. Only the padding is
  more generous, so the box holds the centre of an otherwise empty page.
  (A terminal-window chrome — title bar, dots, 404.agda — was tried and
  reverted on review; heading-size type likewise.)
• The sidebars are gone on this page (site_nav block emptied): the nav
  sidebar is the docs frame, and a wrong URL is not a docs page. Header and
  footer stay, so search and the archive link remain one interaction away.
• Styles live in the template's extrahead block, not extra.css —
  scoped to this one page, written entirely in tokens.css vocabulary, and
  deliberately out of the file [M3-2a] Rebuild the landing page as a stage: hide nav/TOC on home, hero region #93–[M3-2c] Evidence strip: computed counts, each linking to its proof #95 are working in.
• The goal block is coloured like every other Agda block on the site:
  the spans follow the AgdaLexer vocabulary, and the path span wears nf
  deliberately — it is the name the goal is about.
• base_url handling: MkDocs renders error templates with base_url
  taken from site_url's path (/), so every href and stylesheet URL
  survives however deep the missing path is. (nav.homepage.url | url
  renders as /. on this page; the template says why base_url is used
  instead.)
• The constellation hook ([M3-2b] Constellation component: Hasse diagrams as star charts, and ADR-009 (motion) #94): an empty, inert .goal-404__sky
  element sits behind the composition as the mount point, shipped
  text-first as the issue allows.
• One stale comment in mkdocs.yml ("One partial only") updated to name
  both overrides.

Verification

• make check (strict build): clean.
• make design-audit: all three audits green with site/404.html crawled
  like any other page — no font fallback (∃ comes from the shipped
  JuliaMono symbols subset), no cross-origin request, 0 elements below WCAG
  AA in either theme.
• The first contrast pass measured the hole itself at 4.63:1 in light —
  passing, but the thinnest ratio on the entire site, which is the kind of
  margin ADR-005 exists to refuse. The hole's text now leans 20% toward
  the ink token (color-mix), which widens both themes (fg opposes bg
  in each): light 4.63 → 5.88:1, dark 5.76 → 6.48:1 (computed from the
  rendered colours), hue intact.
• That widening exposed a bug in the contrast audit, fixed here.
  Chromium serialises a color-mix() result in the css-color-4 form
  color(srgb r g b), whose channels are 0..1; the audit's parser read
  them as 0..255, i.e. near-black — a false fail at 1.22:1 in dark and,
  worse, a false pass at ~17.9:1 in light, on the same wrong colour.
  audit_contrast.mjs now scales color(…) channels (and survives
  Chromium's 6e-05-style exponents). This was the first text colour on
  the site produced by color-mix(), which is why the gap never showed;
  [M3-2a] Rebuild the landing page as a stage: hide nav/TOC on home, hero region #93–[M3-2c] Evidence strip: computed counts, each linking to its proof #95 are likely to produce more of them.
• mkdocs serve returns HTTP 404 with this page for a nested bogus path,
  and the goal names it (_ : ∃ cv/index.html.bak verified end-to-end);
  screenshotted in both schemes at 1280px and at 375px (no horizontal
  scroll; the box fits).

The issue's last checkbox — GitHub Pages actually serving it for a missing
path on the deployed site, in both themes — can only be ticked after this
merges and deploys; verify with any bogus URL on the live domain.

🤖 Generated with Claude Code

[williamdemeo]

Round 2, from review: the goal now names the missing page itself (_ : ∃ cv/index.html.bak for a request to /cv/index.html.bak), substituted at runtime from location.pathname — textContent-only, whitespace flattened, long paths keep their tail, static ThisPage without JS. And the block now sits in a terminal window (sunken bar, three monochrome dots, 404.agda), tokens only. All gates re-run green: strict build, font/offline/contrast — 16,388 elements per theme, 0 below AA. PR body updated to match.

[williamdemeo]

Round 3, from review: terminal chrome and heading-size type reverted — the goal (still naming the visitor's path) now sits in the same hairline .highlight box every real Agda block wears, at the same --type-code size, with only the padding more generous. Authentic over ornamental. Gates re-run green: strict build; font/offline/contrast, 0 below AA both themes. PR body updated.

[williamdemeo]

Round 4, from review: the hint sentence moved into the box as an Agda comment (--, reworded "The hole"), typing itself out in editor green a beat after first paint. CSS-only: full sentence in the DOM from the first byte, steps(56) clip-path reveal (no layout shift, screen readers never wait), prefers-reduced-motion shows it whole (verified by emulation — zero animation objects), below 45em it wraps and skips the animation. Timeline verified over a cold load: plays exactly once, no restart. Greens pinned per scheme (dark: the palette's string green, 12.5:1; light: a deeper leaf at 6.0:1 — the string token itself is only 4.59:1 on the raised surface). Gates re-run green. PR body updated.

[Copilot]

Pull request overview

This PR implements a custom MkDocs Material 404 page override that presents missing URLs as an “unfillable Agda goal” (including runtime substitution of the requested path), and updates the contrast audit script to correctly parse Chromium’s color(srgb …) serialization produced by color-mix().

Changes:

• Add overrides/404.html to replace Material’s default not-found page with the new goal-themed design and navigation exits (index/projects/search).
• Fix scripts/js/audit_contrast.mjs color parsing to correctly handle CSS Color 4 color(srgb …) output (including scientific notation).
• Update mkdocs.yml comment to reflect the presence of two template overrides.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
scripts/js/audit_contrast.mjs	Corrects contrast-audit parsing for color(srgb …) values emitted by Chromium.
overrides/404.html	Adds a full custom 404 template with scoped styling and runtime path injection.
mkdocs.yml	Updates theme override commentary to mention the new 404 override.

Suppressed comments (1)

overrides/404.html:197

• This hard-codes a raw hex color for the typed comment. Since the dark-scheme string highlight is already defined as --md-code-hl-string-color (see docs/stylesheets/extra.css), you can reference that variable directly and avoid duplicating palette literals here.

    [data-md-color-scheme="slate"] .goal-404__typed {
      color: #86efac;
    }

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[williamdemeo]

Fair catch — fixed in 8282f9b. The affordance is now a real <button type="button"> dressed in the same link clothes (baseline-identical to its link siblings — measured, 0px delta), wired to click() the same __search checkbox the header's magnifier toggles and then focus the query field explicitly. That last part matters: Material only auto-focuses the field from its own s shortcut, not from a toggle change — measured on both layouts. Verified with trusted CDP input: Tab reaches the button, and both mouse click and Enter open the overlay with the caret in the query field. Two deliberate corners: with scripts off the button is inert, which gives up nothing because Material search is a JS feature end to end (index fetch, worker, results); and if the search plugin is ever removed, the script hides the dead control rather than leaving it.

[williamdemeo]

Half agreed, and the half that stands is fixed in 8282f9b: the extrahead comment's "tokens only" claim did overstate, and it now names its exceptions (two structural values, one per-scheme colour pair) instead. But deriving these from --md-code-hl-string-color is the one thing this file must not do. That token measures 4.59:1 on the raised code surface in light — below everything else on the site (the current floor is 4.83:1) — and adopting a value that fails the margin is exactly what ADR-005 exists to refuse; it adjusted three upstream agda-algebras values for the same reason rather than shipping them broken. Dark's #86efac does coincide with the dark string token today, but the coincidence is not the meaning: this green is the editor-comment green the page speaks in, pinned per scheme the same way extra.css pins its syntax colours, so it stays green — and stays at 6.0:1 / 12.5:1 — even if the string token is ever retuned. The comment above the pair carries the measured ratios. (Same answer for the suppressed duplicate on the slate value.)