refactor(docs): design v1 — research-aesthetic polish for veritylang.com#1902
Merged
Conversation
- Drop the global `nav a` background/color override that was making the hero's "Start with a contract" CTA render with a transparent background. Sidebar/TOC/mobile-nav rules remain scoped. - Promote hero link styles to `!important` so Nextra utility classes can no longer leak through. - Replace `'->'` arrows in the proof-surface brief with `→`. - Add focus-visible + hover states for the hero CTAs.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
The Verity/Solidity comparison panels previously rendered as plain unhighlighted text — the client component shipped raw `<pre>` and the Shiki rehype pipeline never saw them. Move the component to a server component that calls Shiki directly with both project themes (cream + verity-dark) using CSS-variable dual-theme mode, then a tiny client child handles mobile tab switching. Result: full Verity and Solidity syntax highlighting on the homepage, matching the rest of the docs.
The hero was a 92vh column with an overweighted "A Lean-native language for verified smart contracts." dek (clamp up to 3.2rem) and a brief panel anchored to the bottom-right, leaving lots of empty space above and below it. Three equally-weighted button-style CTAs wrapped onto three rows in the narrow column. Restructured into: - A tighter `__head` block with kicker → logotype "Verity." (the period carries the accent color, like a small mark) → italic-emphasized dek. - A two-column `__body`: the left column carries the claim list and one filled primary CTA plus secondary text links with arrow glyphs; the right column becomes an "Abstract" definition list with the proof surface / contract shape / audit posture facts. - Reduced hero vertical padding; the page now lets the homepage comparison breathe instead of forcing a near-fullscreen hero. The CTA pattern follows research-paper landings: one strong call to action, then quieter "↗" text links to deeper sections.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
Replace the pure-black dark background with a warm near-black "deep ink" (#0B0908) and give the sidebar a slightly different tint so dark mode reads as deliberately preprint-y rather than blank. Bump the gold accent slightly (#CFA968) and use the same warm ink for the on-accent foreground so CTAs sit cleanly on the background.
Nextra 4 dropped the `nextra-body-typesetting-article` class, so every previous rule scoped to it had silently been dead code; the article body still looked passable only because Nextra's defaults are tame. Also discovered the DOM is `<article><main>...</main></article>` (the opposite of what the old code assumed), so `main article h2` matches nothing. Rescope all body-typography rules to `article main` (the article element gets no specific class on its own), bump specificity on each declaration with `!important` so the rules win over Tailwind utility classes added to every heading by Nextra (`x:text-3xl`, etc.). While there, give h2s a discreet preprint touch: a top rule and a small "§ N" marker on the right margin (CSS counter, suppressed on the CodeCompare heading so its inline kicker stays clean).
- Tighten the inline `code` chip: smaller font, monospace family, rounded corner, lighter border, slightly more padding inside. - Dark mode gets its own background mix so chips read as warm-ink surfaces rather than too-bright cards. - When an inline chip lands inside a heading (e.g. `solc` in a section title), drop the chip chrome entirely so the serif heading rhythm is preserved.
- Use `--verity-page` (warm cream) for the mobile body background to match the desktop content area instead of the darker `--verity-bg`. - Make the mobile hero CTA full-width and stack the secondary "↗" text links vertically. - Slightly shrink the mobile dek and hero h1 so the title doesn't run off-screen.
- Style the first paragraph after an h1 as a lead/abstract opener: slightly larger, lighter weight, more line-height. Mirrors how a preprint reads under the title. - Quiet the breadcrumb (smaller, UI font, muted color, no underlines) so it sits as a navigation marker rather than competing with the title. - Italicize the "Last updated on …" footer line and shrink it to a research-footer caption.
- Switch the navbar wordmark to Source Serif so it matches the page titles (research paper feel). - Slightly larger search input, rounded corner, accent-color focus outline, muted-color placeholder.
Two fixes asked for on the live site.
1. **Sidebar left-margin bug.** On viewports wider than the
`--nextra-content-width` (82rem), the layout centers the
sidebar+content flex row, leaving the page background visible in a
strip to the left of the sidebar. Fixed by giving
`aside.nextra-sidebar` a `::before` that absolutely positions a
100vw wide block of the sidebar tint to the left, plus
`overflow-x: clip` on `html, body` to prevent any horizontal
scrollbar. The aside's own children get `z-index: 1` so they paint
above the faux background.
2. **CodeCompare single-panel switcher.** Replace the side-by-side
Verity / Solidity grid with one panel and a pill-shaped tab
switcher. Land on Solidity (familiar surface), then after 3.2s
auto-switch once to Verity to *demonstrate the lift* — the caption
("Solidity ▸ runtime implementation surface" → "Verity ▸ typed
contract, proof-visible behavior") and a subtle accent wash come
along with it. Any user click cancels the timer and pins the choice.
Auto-switch is suppressed under `prefers-reduced-motion: reduce`.
The mobile bespoke tab strip is gone — same pill control works at
every width.
The CTA, hero brief panel, callouts, and code blocks all had sharp corners, but a few elements still kept Nextra's 4px / Tailwind rounded defaults — most visibly the sidebar item highlights and the code switcher tab pill. Zero out every border-radius in our stylesheet (search input, hero CTA, callouts, inline code chips, code switcher container, tabs, and the sidebar/TOC/mobile-nav active states) and add sweeping `border-radius: 0 !important` overrides for the sidebar a / button / li that Nextra rounds by default. The active sidebar item now reads as a flush warm-cream rectangle with a 2px inset accent bar on the left, matching the rest of the LaTeX-preprint feel. The code-switcher tab pill becomes a flat two-segment control divided by a vertical rule, consistent with the rest of the surfaces.
The previous wide-screen background fix put `position: relative` on `aside.nextra-sidebar`, which clobbered Nextra's `position: sticky` and let the aside fall back into normal document flow — at narrow widths the layout flex placed it *below* the navbar by another navbar height, leaving a ~68px empty strip above the first menu item. Switch the wide-screen left strip from an aside `::before` to a fixed `body::before` that paints the sidebar color from the navbar bottom to the viewport bottom, with `width: max(0, (100vw - content-width) / 2)` so it disappears on narrow viewports. The aside keeps its untouched sticky positioning, the sidebar sits flush under the navbar again, and on >1440px viewports the tan/ink fills the left strip seamlessly.
Cut redundancy and dense jargon to make the home page faster to read. - **Hero**: drop the three-item claim list (it duplicated what the brief panel already said). Replace the dek with a three-beat sentence that names the actual loop — "Write smart contracts in Lean. Compile to EVM. Prove them correct." Rename the brief panel from "Abstract" to "At a glance" and shorten its row labels (Proof surface → Pipeline, Contract shape → Surface, Audit posture → Assurance). - **Code compare**: shorter intro line and a switch from boxed body prose to a 3-column key-value note (label + short sentence). - **Report callout**: rewrite the dense Lean-path paragraph in plain English; keep the manual-reading guidance. - **Three-Layer Structure**: opening line names the three things in bold instead of restating them. - **Read next table**: trimmed cell copy.
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
With the claim list gone, the left CTA column was shorter than the right "At a glance" panel and the page leaked empty space below the CTA. Switch the hero body grid to align-items: end so the CTA + ↗ links sit at the same baseline as the bottom of the brief panel, and the empty space lives above (where it reads as intentional white). Also nudges the hero's top/bottom padding down a touch.
Replace the uniform flex gap on the hero head with per-element margins so the kicker hugs the title (0.6rem) while the dek and CTA cluster get more space. Reads as kicker+title together, dek as a beat, CTA as a beat.
The intro for the comparison section used a two-column grid (kicker + intro on the left, h2 on the right). Read as a paper-figure caption, but it was easy to miss the headline and the layout fought the otherwise top-to-bottom homepage rhythm. Collapse to a normal stacked intro: kicker → h2 → one-line prose. "The same contract, lifted into Lean." now sits on its own line on desktop, sized to match the page hierarchy.
The report-callout carried a 1 px bottom border, and the next h2 carries its own top rule via the article heading styles — they read as two close-together lines. Remove the callout's bottom border so section breaks have exactly one rule. Trim the callout's vertical margins a touch while there.
Nextra's auto pagination ("Getting Started →" at the bottom of the
homepage) rendered in display-text size and competed with the headings
on the page. Restyle it to the UI font, accent color, and a small
arrow that nudges right on hover — a footer navigator instead of a
section heading.
The CTRL+K hint inside the search input and the Pagefind results popover still rendered Nextra's default rounded corners. Match the rest of the UI by zeroing border-radius and re-coloring the chip to warm-tan ink-on-cream.
The "Copy page" / dropdown widget at the top of each article still rendered with Nextra's rounded-md wrapper. Zero the radius and use the warm-cream surface so it matches the rest of the UI.
Match the rest of the site's small-caps kicker convention: smaller size, accent color, letter-tracked uppercase. Reads as a label for the TOC list rather than a competing heading.
The article-body code blocks (`<pre>` rendered by Nextra) still carried a 6px border-radius. Match the square-corners convention by setting border-radius: 0 on the same selectors that already restyled the background/border.
The Pagefind search result links inside the popover still kept rounded-md from Nextra. Square them so the search panel matches the rest of the UI.
Four feedback items: 1. **Navbar too bright.** The old navbar was 94% of the lightest cream (--verity-page) with a 10px backdrop blur — read as a stark white slab above the tan sidebar. Switched to a warm mid-tone between sidebar and page (`color-mix(in srgb, --verity-sidebar 55%, --verity-page)`) and dropped the blur. The dark mode navbar now uses --verity-surface directly. Also fixed the selector — Nextra renamed the class to `.nextra-navbar-blur`, so the old rule was silently no-op. 2. **"White square at the top of the sidebar" while scrolling.** Same root cause: the translucent + backdrop-blur navbar was painting a bright rectangle over the top of the sidebar as page content scrolled past it. Removing the blur and giving the navbar an opaque mid-tone bg makes that artifact go away. 3. **Em dashes.** Replaced in user-facing copy: the side-by-side intro now uses ":", three-layer h3 captions use " · ", the trust callout uses ":". 4. **Solidity syntax highlighting.** The theme only defined Verity scopes (e.g. `keyword.declaration.contract.verity`), so Solidity tokens fell back to the editor foreground. Audited the actual scopes emitted by Shiki's Solidity grammar (`source.solidity`) and added matching colors for: contract/event/function/modifier keywords, type modifiers (public/external/payable/indexed/etc.), primitive types (address, uint256, …), contract/struct/event names, function names and modifier names, exception controls (require/assert/revert) in accent red, language transaction vars (msg.sender, msg.value, this), numerics, strings, and operators. Both light and dark themes updated with their respective palettes.
Adds a secondary "Read the paper" outlined CTA next to the primary "Start with a contract" button, before the Compiler/Verification/Research links. Opens lfglabs.dev/papers/verity.pdf in a new tab.
- index.mdx: re-add the `Compiler/Proofs/IRGeneration/Contract.lean` Layer 2 boundary sentence the sync checker requires. - verity-site.css: `.dark body::before` uses `--verity-sidebar` so the extended sidebar strip matches the actual sidebar color in dark mode. - verity-site.css: drop dead `.verity-claim-list` rules (no consumer). - verity-site.css: hoist Verity panel gradient onto the visible `.code-panel__pre > pre` so the upstream `!important` background no longer hides it. - verity-site.css: `.code-compare__notes > div` now carries the mobile separator (markup is a <dl> of <div>, not a <ul> of <li>). - verity-site.css: remove the redundant `.report-callout:has(+ h2)` rule (was unconditional and a no-op). - CodeCompare.tsx: read grammar/theme JSONs once and pass them into `highlight` instead of re-reading per call.
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 32981c8. Configure here.
| numbered sections feel formal there. Keep them on doc pages. */ | ||
| article:has(.verity-hero) main h2::after { | ||
| content: none !important; | ||
| } |
There was a problem hiding this comment.
Homepage h2 top-rule not suppressed as described
Low Severity
The PR description states "Section h2s carry a top rule + § N paper-section marker on doc pages (homepage suppresses both — the page is short)." However, article:has(.verity-hero) main h2::after only suppresses the § N marker (content: none). There is no corresponding rule to suppress border-top on homepage h2 elements. The "The Three-Layer Structure" and "Read next" headings in index.mdx still render the top hairline rule, contradicting the stated design intent.
Reviewed by Cursor Bugbot for commit 32981c8. Configure here.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Goal
Refresh veritylang.com toward a clean, elegant, research / LaTeX-preprint aesthetic with subtle warmth, careful typography, first-class syntax highlighting for Verity / Lean / Solidity, and a homepage that's fast to read and easy to act on.
Live at: https://veritylang.com
Working principles
#0B0908), restrained brown/gold accent.prefers-reduced-motionrespected.Approach
Every commit is screenshot-reviewed with Playwright (light + dark + mobile + 1920px wide) and deployed straight to Vercel prod (~30 commits, ~30 deploys).
Highlights
Hero
Lean 4 · Formal verification · EVM) →Verity.(period in accent color, 1.08× optical bump) → italic-emphasized one-line dek → CTA + ↗ secondary links.Write smart contracts in Lean. Compile to EVM. Prove them correct..Code comparison
Solidity/Verity).IntersectionObserver, suppressed underprefers-reduced-motion, cancelled by any user click).<pre>).Article typography
<article><main>...</main></article>); the oldnextra-body-typesetting-articleselectors were silently dead code.§ Npaper-section marker on doc pages (homepage suppresses both — the page is short).Specification — what should be true,Implementation — what runs on chain,Proof — they agree.Information density
Read nexttable →<ReadingList>component: bold title + one-line note + → arrow, hairline dividers.article:has(.verity-hero).Theme & polish
#0B0908) instead of pure black; gold accent dot, soft brown-gold CTAs.max-w-(--nextra-content-width)on wide screens via a fixedbody::beforestrip — no horizontal scroll.position: relativeoverrode Nextra'sstickyand dropped the aside; reverted).lfglabs-dev/verityrepo.How it was reviewed
Playwright screenshot loop at 1440×900, 1920×900, 1024×900, and 390×844, light + dark, both via
colorSchemeand a.darkclass fallback. Real-pixel sampling via pngjs to confirm bg colors at boundaries. Live verification onhttps://veritylang.comafter each Vercel prod deploy.Selected commits (most recent first)
single-column side-by-side introfiner rhythm in the hero headsubtler CTA hovertighten side-by-side intro linesplit hero kicker into three tagsLean 4 · Formal verification · EVM.point navbar GitHub link at new repolfglabs-dev/verity.respect prefers-reduced-motion on panel fadenudge the Verity. terminal dot up to 1.08emonly auto-switch when in viewhero as single column + facts stripdrop § N markers on home pagereading list replaces table<ReadingList>.inline captions on three-layer h3ssimplify homepage copy and structuresidebar no longer pushed down by navbar heightbody::beforestrip.square every rounded cornersidebar bg extends to viewport edge + switcherarticle typography rules now actually matcharticle main, added§ Nmarkers.warm the dark theme#0B0908deep ink.real syntax highlighting on landing CodeCompareprimary CTA, hero arrowsnav aglobal override was eating the CTA.Note
Medium Risk
Moderate risk: large CSS/markup retheme and new client-side switcher behavior may cause visual regressions or hydration/perf issues, but changes are isolated to the docs site UI.
Overview
Refreshes the docs-site design toward a warmer, research/preprint aesthetic: updates global tokens and extensive Nextra overrides (navbar/sidebar/search, square corners, typography/section styling, breadcrumbs/pagination, and dark-mode palette tweaks).
Reworks the homepage hero and navigation into a single-column CTA-focused layout with a new “facts” strip, updates homepage copy, and replaces the “Read next” table with a new
ReadingListcomponent.Overhauls the landing-page code comparison: switches from a static side-by-side grid to a tabbed single-panel
CodeCompareSwitcherthat auto-switches once when scrolled into view (respectingprefers-reduced-motion), and moves code rendering to server-side Shiki highlighting using the repo’s Verity grammar plus updated light/dark themes.Also updates docs navbar/repo links to
lfglabs-dev/verityand adds.verceland design-iteration scripts to.gitignore.Reviewed by Cursor Bugbot for commit 32981c8. Bugbot is set up for automated code reviews on this repo. Configure here.