[M3-2a] Rebuild the landing page as a stage (#93) - #106
Conversation
The home page drops the docs frame -- `hide: navigation, toc` in front matter, this page only -- and opens with a hero grid: eyebrow, the claim as the h1 (the name is in the header bar, the eyebrow, and <title>), a one-paragraph sub-claim, and two actions. The portrait moves from a float into the grid's second column, which retires #88's failure modes here: no rule can draw behind the photo and no line box gets squeezed, because nothing is in flow around it. That column is component-agnostic on purpose -- M3-2d (#96) swaps the figure for the typed-proof terminal without touching the grid. All hero styles are tokens; no raw colours or sizes. Verified in a browser at 1440px and 390px, both themes. Part of #93. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR rebuilds the MkDocs home page into a dedicated “landing stage” by removing the docs frame (nav + TOC) on only docs/index.md and introducing a two-column hero grid (copy + portrait) that can later host the typed-proof terminal.
Changes:
- Add a new
.herogrid component (and related utility classes) todocs/stylesheets/extra.css. - Update
docs/index.mdto hide navigation/TOC on the home page and replace the prior floated portrait layout with the new hero markup.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| docs/stylesheets/extra.css | Adds the new home-page hero grid styles (layout, typography, responsive behavior). |
| docs/index.md | Applies hide: [navigation, toc] on the home page and restructures the top section into the new hero grid markup. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| [Explore the projects](projects/index.md){ .md-button .md-button--primary } | ||
| [About me](about.md){ .md-button } | ||
| { .hero-actions } |
There was a problem hiding this comment.
Accurate about #93's task list, but this is sequencing, not drift. The first action is already the proofs ("Explore the projects"). The second — "watch an agent prove a theorem" — needs M4-3's page to exist, and that page (#99, an asciinema of a real agda-native-air session) is deliberately the long-lead item: a CTA pointing at a page that isn't there fails --strict, and pointing it anywhere else would break ADR-009's evidence-honesty rule before the evidence exists. "About me" holds the slot; the swap happens when #99 lands, and #93 stays open until its criteria are checked against the deployed page, so the gap stays tracked. No change here.
| } | ||
|
|
||
| .md-typeset .hero-side { | ||
| max-width: 24rem; |
There was a problem hiding this comment.
Taken, one commit late and one value later. The flagged 24rem left with .hero-side when the portrait was dropped (ccbd2c5) — but the follow-up's min-block-size: 20rem was the same violation reintroduced, and "no raw sizes" is this issue's own acceptance criterion. It is now --hero-stage in tokens.css, with the derivation recorded at the token (098abb7).
The photograph is out of the hero: it was decoration on a page whose argument is evidence, and the page argues better without it. The grid keeps both columns -- the second is reserved for M3-2d's typed-proof terminal (#96), and until that ships it is clear sky for the constellation backdrop (M3-2b, #94) instead of a picture covering it. A min-block-size holds the stage at the height the portrait used to establish, so the column reads as canvas rather than collapse and the copy centres in the kept height; below the breakpoint it returns to auto, because a stacked phone layout has no second column to keep clear. The bus photograph had no other reference anywhere in the tree, so the file goes too -- git keeps it if it is ever wanted, and About's Nara photograph stays where it is. Part of #93. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Copilot flagged a raw 24rem in the hero's mobile rules. That literal left with .hero-side when the portrait did, but the point outlives it: "no raw sizes" is this issue's own acceptance criterion, and the follow-up's min-block-size reintroduced one. The held-open stage height is now --hero-stage in tokens.css, with its derivation recorded where the value lives. Part of #93. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
What
The home page — and only the home page — drops the docs frame (
hide: navigation, toc) and opens with a hero grid: eyebrow line, the claim as the h1 ("Mathematics, machine-checked." — the name stays in the header bar, the eyebrow, and<title>), a one-paragraph sub-claim, and two.md-buttonactions. The grid's second column is deliberately empty: it is clear sky for #94's constellation backdrop until M3-2d (#96) puts the typed-proof terminal there.(The first cut of this PR moved the portrait into that column; the follow-up commit drops the photograph altogether — decoration on a page whose argument is evidence — and deletes the now-unreferenced file. About's Nara photograph is untouched.)
First of the three stacked landing PRs from the 2026-08-03 design review; #94 (constellation) and #95 (evidence strip) build on this canvas.
Notes for review
min-block-size: 20rem(the height the 440×370 portrait used to establish at full content width) holds the stage open, so the empty column reads as canvas rather than collapse and the copy centres in it. It returns toautobelow Material's mobile breakpoint, where there is no second column to keep clear.tokens.cssvalues — no raw colours or sizes; the front-matter comment block documents the load-bearing decisions.Verified
mkdocs build --strictgreen at this branch's tip.make design-audit(font + offline + contrast) green at the stack tip that contains this change: 50 pages × 2 themes, every text element AA, no cross-origin request, no font substitution.hero-sidemarkup and no reference to the deleted image.Part of #93 (the issue closes when the acceptance criteria are checked against the deployed page).
🤖 Generated with Claude Code