Skip to content

Maintaining this site

This page explains how the documentation site is built and how to change the settings that are most likely to need adjusting.

How it works

The site is a MkDocs + Material build, generated directly from the literate .lagda.md sources β€” there is no separate copy of the documentation. The decision record is ADR-007; the moving parts are:

  • mkdocs.yml (repo root) β€” the site configuration: theme, colours toggle, plugins, Markdown extensions, navigation behaviour. Most settings live here.
  • scripts/python/mkdocs_gen_library.py β€” runs during every build and mounts the library: for each src/**/*.lagda.md it writes a site page at a clean URL (src/Setoid/Algebras/Basic.lagda.md β†’ /Setoid/Algebras/Basic/), and it generates SUMMARY.md, the file that becomes the whole navigation.
  • agda --html β€” when the highlighted build is requested, Agda renders each module's code blocks to classed, hyperlinked HTML. mkdocs_gen_library.py embeds that; if it is absent, code blocks fall back to plain monospace.
  • scripts/python/mkdocs_hooks.py β€” rewrites repo-relative prose links (src/…, docs/adr/…, CONTRIBUTING.md) into site URLs, and prints the per-page build log.
  • docs/_links.md β€” a library of reference-style links ([Setoid.Algebras.Basic][]) appended to every page so cross-references resolve. Its module half is generated by scripts/python/gen_links.py; re-run that after adding modules.
  • docs/stylesheets/custom.css β€” all the bespoke styling: the Agda token colours, the modern "Aurora" theme, and the landing-page components.
  • docs/assets/js/agda-copy.js β€” adds a copy button to the highlighted <pre class="Agda"> blocks (Material's own copy button only covers its .highlight blocks, which the agda --html output is not).
  • docs/assets/js/agda-toggle.js β€” the header's "Show more Agda" control (#431). Module sources wrap their leading OPTIONS/module/import scaffolding in <!-- … --> comments; mkdocs_gen_library.py re-surfaces those blocks tagged hidden-source, and this control shows or re-hides them all at once, with the choice persisted in localStorage like the palette toggle.

Hiding a module's import scaffolding

Every module's leading scaffolding block β€” the OPTIONS pragma, the module … where header, the imports, and the private variable declarations β€” is wrapped in an HTML comment in the .lagda.md source:

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Homomorphisms.Noether where

open import Level using ( Level )
-- … the rest of the imports …
```
-->

Agda still type-checks the block (fenced agda code inside an HTML comment is still code), GitHub's Markdown renderer collapses it, and on the site it becomes a toggleable hidden-source block, revealed either by the header's "Show more Agda" control (all blocks, persisted) or by the small β–Έ hidden code (n lines) note that agda-toggle.js places in front of each hidden block (that block only). When the scaffolding shares its fence with real definitions, split the fence and wrap only the scaffolding part. New modules should follow the same convention.

The wrapper must be an HTML comment rather than any indenting construct: Agda requires its code at column 0, so a block can never be indented into a ??? note admonition or a Markdown-nested <details> β€” indenting the fence breaks type-checking. The comment wrapper adds no indentation, which is exactly why issue #431 settled on this mechanism.

Two kinds of module are deliberate exceptions:

  • Pedagogical modules whose scaffolding is the subject of the surrounding prose stay fully unwrapped: Overture.Basic (which explains the OPTIONS pragma, modules, and imports) and Demos.HSP (the TYPES 2021 paper, which discusses its imports in the text).
  • Barrel modules stay unwrapped too: a barrel's annotated open import … public list is the page's content, and hiding its only block would leave a blank page that reads as unfinished.

As a tripwire against accidentally wrapping a barrel, the build logs a ⚠ <Module>: every code block on this page is hidden line for any page that would render code-free. Three prose-first pages hide their lone OPTIONS/module block by design and are exempt from that check: Overture.Preface, Demos.GeneralOperationsAndRelations, and Setoid.Complexity.Basic (PROSE_ONLY_MODULES in mkdocs_gen_library.py).

Build commands

Run these inside nix develop (the MkDocs toolchain is pinned in flake.nix):

Command What it does
make site Fast build to ./site. Code blocks are plain (no Agda pass).
make serve Fast live preview at http://127.0.0.1:8000.
make site-full make html + make agda-md + make site β€” the published site, with token highlighting + the /classic/ site. This is what CI builds.
make serve-full The full preview (highlighting + /classic/), live-reloading.
make html Just the classic clickable-HTML site (Everything.html index) into ./html.
make agda-md Just the highlighted-Markdown pass into .agda-html/md.

Seeing the real thing locally

make serve is fast but renders plain code blocks (and /classic/ 404s), because the agda --html passes are skipped. Use make serve-full to preview exactly what gets deployed.

Recovering a stuck Pages deployment

Publishing is a two-repository chain: the Docs workflow here builds ./site and pushes it to the gh-pages branch of universalalgebra/agda-algebras, and GitHub's auto-generated pages-build-deployment workflow in that repository publishes the branch to the live site. The last hop occasionally fails with a transient Deployment failed, try again later, and a failed run can wedge in queued when re-run. Recovery steps, in escalating order:

  • Check for a platform incident at githubstatus.com; this error is almost always GitHub-side, and waiting often suffices.
  • Re-run the failed pages-build-deployment run from the Actions tab of universalalgebra/agda-algebras.
  • Re-run the Docs workflow here (Actions β†’ Docs β†’ Run workflow). Note this re-triggers publication only when the rebuilt site differs from what is already on gh-pages β€” the publish action skips the push when nothing changed, so an unchanged same-day rebuild is a no-op.

  • Force a fresh deployment with an empty commit, which always re-triggers the publisher:

    git clone --branch gh-pages --depth 1 [email protected]:universalalgebra/agda-algebras.git ua-pages
cd ua-pages
git commit --allow-empty -m "retrigger Pages deployment"
git push

Merging any content change to master also re-pushes gh-pages and re-triggers publication as a side effect. When checking what is actually live, remember the Pages CDN caches responses for up to ten minutes and your browser caches the HTML and CSS on top of that β€” hard-refresh, or probe a file headers-only with curl -sI https://agda-algebras.universalalgebra.org/assets/js/agda-copy.js.

The site's own CSS/JS are content-hashed so that a returning visitor never renders fresh HTML against a stale-cached stylesheet or script (the assets carry a multi-hour max-age, far longer than the HTML's ten minutes). on_config in scripts/python/mkdocs_hooks.py appends an eight-character hash of each extra_css / extra_javascript file to its URL (custom.css?h=…); a changed asset therefore gets a fresh URL, which the short-lived HTML picks up within minutes (#429). The copied file keeps its plain name β€” only the reference carries the query β€” so the headers-only probe above is unaffected.

Resist the temptation to add a deployment workflow to the gh-pages branch itself: that branch is disposable build output which the publish action overwrites, and keeping such a file alive would require keep_files: true, which never deletes anything and so leaks renamed or removed pages onto the live site forever.

Changing the settings

Colours and the theme

The active palette is Aurora (indigoβ†’violet chrome, orange accent), a set of CSS variables in docs/stylesheets/custom.css under Β§6. Each colour scheme (light default, dark slate) has its own block; the --ualib-* aliases below the Material variables drive the bespoke components (hero gradient, stat numbers, matrix header, the βœ“ marks). To shift the accent, for example, edit:

[data-md-color-scheme="default"] {
  --md-primary-fg-color: #4f46e5; /* header / chrome (indigo-violet)    */
  --md-accent-fg-color:  #fb6a00; /* hover / accent  (vivid orange)     */
  --md-typeset-a-color:  #5b54e6; /* links                              */
  --ualib-board:   #201f4d;       /* hero gradient, indigo base         */
  --ualib-board-2: #4a2f86;       /* hero gradient, violet top          */
}

Two alternate palettes ship ready to drop in β€” replace both scheme blocks in Β§6 with one of these to retheme the whole site:

  • Cobalt (blue-led, the calmest): light --md-primary-fg-color: #2f37c9, --ualib-board: #1c2348 / --ualib-board-2: #2b3470, accent #f97316, links #3055e6; dark navy surfaces #0e1322.
  • Ultraviolet (violet-led, the boldest): light --md-primary-fg-color: #6d28d9, --ualib-board: #241a45 / --ualib-board-2: #3a2570, accent #f97316, links #7c3aed; dark purple-black surfaces #120e1f.

The code-block palette

The Agda token colours (used by both code blocks and inline prose terms) are in Β§2 of custom.css, with one block per scheme; the code-block background is in Β§4. These are independent of the chrome palette above, so changing one never disturbs the other.

  • Light is the classic-vivid (formal-ledger) palette β€” it already matches Aurora's blue/purple/orange, so it is usually left alone.
  • Dark is the bespoke Aurora Deep palette: a deep-indigo ground with orange keywords (echoing the hero accent) and indigo functions/modules (matching the links), so code reads as part of the theme.

To swap the dark palette, replace the [data-md-color-scheme="slate"] block in Β§2 and the slate --md-code-bg-color in Β§4. Two cooler alternates are ready to paste in (a user-facing in-page palette switcher would be possible but is intentionally not built β€” it competes with the light/dark toggle for little gain; a one-block edit here is the supported way to retheme):

/* TOKYO NIGHT β€” cool navy, violet keywords, cyan types. */
[data-md-color-scheme="slate"] { --md-code-bg-color: #1a1b2e; --code-accent: #7aa2f7;
  .AgdaKeyword, pre.Agda .Keyword { color: #bb9af7; }
  .AgdaComment, pre.Agda .Comment { color: #565f89; font-style: italic; }
  .AgdaString, pre.Agda .String { color: #9ece6a; }
  .AgdaNumber, pre.Agda .Number { color: #ff9e64; }
  .AgdaSymbol, pre.Agda .Symbol { color: #89ddff; }
  .AgdaArgument, pre.Agda .Argument, .AgdaMarkup, pre.Agda .Markup,
  .AgdaBound, pre.Agda .Bound, .AgdaGeneralizable, pre.Agda .Generalizable { color: #c0caf5; }
  .AgdaPrimitiveType, pre.Agda .PrimitiveType, .AgdaPrimitive, pre.Agda .Primitive,
  .AgdaDatatype, pre.Agda .Datatype, .AgdaRecord, pre.Agda .Record { color: #2ac3de; }
  .AgdaInductiveConstructor, pre.Agda .InductiveConstructor,
  .AgdaCoinductiveConstructor, pre.Agda .CoinductiveConstructor { color: #ff9e64; }
  .AgdaField, pre.Agda .Field { color: #73daca; }
  .AgdaFunction, pre.Agda .Function, .AgdaMacro, pre.Agda .Macro,
  .AgdaPostulate, pre.Agda .Postulate { color: #7aa2f7; }
  .AgdaModule, pre.Agda .Module { color: #7dcfff; }
}

/* NORD β€” desaturated frost; the calmest. */
[data-md-color-scheme="slate"] { --md-code-bg-color: #242a3d; --code-accent: #88c0d0;
  .AgdaKeyword, pre.Agda .Keyword { color: #81a1c1; }
  .AgdaComment, pre.Agda .Comment { color: #667089; font-style: italic; }
  .AgdaString, pre.Agda .String { color: #a3be8c; }
  .AgdaNumber, pre.Agda .Number, .AgdaField, pre.Agda .Field { color: #b48ead; }
  .AgdaSymbol, pre.Agda .Symbol { color: #9aa6c4; }
  .AgdaArgument, pre.Agda .Argument, .AgdaMarkup, pre.Agda .Markup,
  .AgdaBound, pre.Agda .Bound, .AgdaGeneralizable, pre.Agda .Generalizable { color: #d8dee9; }
  .AgdaPrimitiveType, pre.Agda .PrimitiveType, .AgdaPrimitive, pre.Agda .Primitive,
  .AgdaDatatype, pre.Agda .Datatype, .AgdaRecord, pre.Agda .Record { color: #8fbcbb; }
  .AgdaInductiveConstructor, pre.Agda .InductiveConstructor,
  .AgdaCoinductiveConstructor, pre.Agda .CoinductiveConstructor { color: #d08770; }
  .AgdaFunction, pre.Agda .Function, .AgdaMacro, pre.Agda .Macro,
  .AgdaPostulate, pre.Agda .Postulate, .AgdaModule, pre.Agda .Module { color: #88c0d0; }
}

Fonts

All three families are self-hosted under docs/assets/fonts/ (no font CDN), declared as @font-face at the top of custom.css:

  • headings β€” Space Grotesk (a geometric grotesque), via the single --ualib-display variable in :root. Change every heading, the hero title, the stat numbers, and the matrix header in one line by setting --ualib-display to "Geist" or "Sora" (both already self-hosted) β€” or add a new @font-face and name it there.
  • body β€” Inter (--md-text-font).
  • code β€” JuliaMono (--md-code-font), the one font still CDN-loaded, for its complete mathematical-Unicode coverage.

The logo and favicon

Both point at docs/assets/lambda.png via theme.logo and theme.favicon in mkdocs.yml. Drop a replacement PNG at that path (a transparent background looks best on the coloured header).

The nav is generated, not hand-written. The library tree comes from the module hierarchy automatically. The fixed top-level entries (Home, the Project section) are defined in scripts/python/mkdocs_gen_library.py in the SUMMARY.md assembly near the bottom β€” add or reorder lines there.

The landing page

docs/index.md is plain Markdown plus a few HTML blocks whose styling lives in custom.css (Β§8–§11):

  • the hero (.ualib-hero) β€” title, tagline, the formula, the buttons;
  • the stat strip (.ualib-stats) β€” edit the four numbers inline;
  • the Featured results gallery (.ualib-figures) β€” each card is one <a class="ualib-figure">; swap a monogram for a photo by replacing the <span class="ualib-portrait">GB</span> with <span class="ualib-portrait"><img src="/assets/portraits/birkhoff.jpg" alt="…"></span>;
  • the coverage matrix (table.ualib-matrix) β€” a plain HTML table; add a row for a new structure, or a <td class="yes">βœ“</td> for a new axiom.

Adding a prose page

Drop a Markdown file under docs/ and add a line to the SUMMARY.md assembly in mkdocs_gen_library.py so it appears in the nav. Repo-relative links in the prose (src/…, docs/…) are rewritten to site URLs automatically by the hook.

To make [Some Name][] resolve everywhere, add a definition to the External links section of docs/_links.md (or, for module links, just re-run python3 scripts/python/gen_links.py).

Where things live

mkdocs.yml                              site config (theme, plugins, nav behaviour)
docs/
  index.md                              the landing page
  site-guide.md                         this page
  _links.md                             shared reference-link library (generated + external)
  stylesheets/custom.css                all bespoke styling
  assets/                               logo, favicon, portraits, vendored JS
  adr/                                  architecture decision records
scripts/python/
  mkdocs_gen_library.py                 mounts src/ as pages + builds the nav
  mkdocs_hooks.py                       link rewriting + per-page build log
  gen_links.py                          regenerates the module half of _links.md
.github/workflows/docs.yml              build (make site-full) + deploy to gh-pages