site: build the generated views into a static site in CI (WO 4.3, build only)

Justfile

@@ -131,7 +131,7 @@ clean-all: clean
 
 # Run every detected language's tests. It runs `check` first (re-anchoring plan WO 2.5), so a stale view or a
 # failing proof fails it.
-test: check provision::test
+test: check site-test provision::test
 
 # Run tests with verbose output
 test-verbose: provision::test
@@ -707,7 +707,7 @@ uncloak:
 # The Mathesis golden path (re-anchoring plan WO 2.5). CI runs it in the pinned
 # Guix (agda-proof-policy.yml). A stale view or a failing proof fails.
 # Golden path: every generated view matches its data, every gated proof checks
-check: check-views check-proofs
+check: check-views site-check check-proofs
 
 # Needs bun, network for the receipts, and MATHESIS_STANDARDS (see `registry`).
 # Views current: catalogue, census tests, atlas, claims registry, bridges and
@@ -788,3 +788,24 @@ applied-build:
 applied-check:
     bun scripts/applied/cohort.mjs check
     bun test tests/applied/
+
+# ── mathesis: static site of the generated views (re-anchoring plan WO 4.3) ──
+
+# Build the site into OUT (default: a fresh temp dir; never a tracked path).
+# BUILD ONLY: nothing deploys. Needs asciidoctor (in the pinned Guix shell) and
+# bun. It fails on any Asciidoctor warning and on any broken relative link.
+site out="":
+    bun scripts/site/site.mjs build {{out}}
+
+# Build the site into a temp dir, then discard it. `check` runs this, so CI
+# builds the site on every pull request and push to main.
+site-check:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    out="$(mktemp -d)"
+    trap 'rm -rf "$out"' EXIT
+    bun scripts/site/site.mjs build "$out"
+
+# Test the front-page generator and the link check (no asciidoctor needed)
+site-test:
+    bun test tests/site/

build/manifest.scm

@@ -16,4 +16,6 @@
        ;; Provers for the proof lanes (re-anchoring plan WO 1.4, ruling D-8 (a)).
        ;; No agda-stdlib: its Guix package does not build, and no proof here
        ;; imports it (owner ruling 2026-11-10).
-       "agda" "coq" "lean4"))
+       "agda" "coq" "lean4"
+       ;; Static site of the generated views (re-anchoring plan WO 4.3).
+       "ruby-asciidoctor"))

docs/status/ROADMAP.adoc

@@ -199,6 +199,18 @@ One pull request that changes census rows is open at a time (atlas README,
   clause; `docs/status/PROOF-STATUS.adoc` records the comparison. WO 4.2 is
   then done. Next: receipts for APP-1 to APP-4, from a CI run on the merged
   commit, then WO 4.3 (needs a ruling).
+* WO 4.3, publish the atlas (owner rulings 2026-11-12): site built in CI;
+  deploy waits for the 2026-11-24 hold and an owner ruling.
+** `just site OUT` writes one generated front page, then renders it and the
+   seven generated views with Asciidoctor (pinned Guix shell,
+   `ruby-asciidoctor`). `just check` builds the site into a temp dir, so the
+   Guix job builds it on every pull request and push to main.
+** The build fails on any Asciidoctor warning and on any broken relative link.
+   A link to a repository file outside the site becomes a GitHub link at `main`.
+** Not done, by ruling: no deploy job and no Pages settings change. Stage 1
+   must hold two weeks, so deploy is possible on or after 2026-11-24, after a
+   fresh owner question. `.github/workflows/pages.yml` stays as it is; the
+   deploy pull request replaces it.
 * Open item for the owner (ruling 2026-11-12): none of the JSON Lines data
   files declares a licence; JSON has no comment syntax. The owner will write
   one `REUSE.toml` rule at the root that covers all of them (doctrine 6: a

scripts/site/site.mjs

@@ -0,0 +1,170 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+//
+// The static site of the generated views (re-anchoring plan WO 4.3). BUILD
+// ONLY: nothing here deploys or publishes.
+//
+//   bun scripts/site/site.mjs build OUT
+//
+// It writes one generated front page, then renders that page and each view
+// with Asciidoctor into OUT, at the same paths as the views. It fails closed:
+//   - Asciidoctor runs with --failure-level=WARN, so any warning fails.
+//   - A view header that no longer names its source fails the build.
+//   - A relative link to a file that is neither in the site nor in the
+//     repository fails. A relative link to a repository file that is not in
+//     the site becomes an absolute GitHub link at `main`.
+import {readFileSync, writeFileSync, existsSync, mkdirSync, mkdtempSync, readdirSync, statSync} from 'node:fs';
+import {spawnSync} from 'node:child_process'; // hypatia:ignore js_exec_sync -- argv array, no shell; the program is an absolute path and every argument is a constant or a repository path
+import {tmpdir} from 'node:os';
+import path from 'node:path';
+
+export const GITHUB = 'https://github.com/hyperpolymath/mathesis';
+
+// Each view, the text its header must contain (its generator or its source),
+// and one line on how it is derived. The check on `needs` keeps the line true.
+export const VIEWS = [
+  {file: 'docs/atlas/generated/az.adoc', needs: 'census/rows.jsonl',
+   how: 'Built by `scripts/atlas/census-atlas.mjs` from the census rows `docs/atlas/census/rows.jsonl`.'},
+  {file: 'docs/atlas/generated/catalogue.adoc', needs: 'scripts/census/render-catalogue.sh',
+   how: 'Rendered by `scripts/census/render-catalogue.sh` from the census rows.'},
+  {file: 'docs/atlas/generated/organisations.adoc', needs: 'census/rows.jsonl',
+   how: 'Built by `scripts/atlas/census-atlas.mjs` from the census rows `docs/atlas/census/rows.jsonl`.'},
+  {file: 'docs/atlas/generated/registry.adoc', needs: 'scripts/registry/claims-registry.mjs',
+   how: 'Built by `scripts/registry/claims-registry.mjs` from `docs/atlas/claims/claims.jsonl` and the receipts it pins. The grade is derived, not assigned.'},
+  {file: 'docs/atlas/generated/bridges.adoc', needs: 'scripts/registry/claims-registry.mjs',
+   how: 'Built by `scripts/registry/claims-registry.mjs` from `docs/atlas/claims/bridges.jsonl`. Each row is a candidate, not evidence.'},
+  {file: 'docs/theory/generated/index.adoc', needs: 'scripts/registry/claims-registry.mjs',
+   how: 'Built by `scripts/registry/claims-registry.mjs` from `docs/theory/admissions.jsonl`, the claims and the receipt they pin.'},
+  {file: 'applied-systems/finance/cohort-economics/generated/examples.adoc', needs: 'scripts/applied/cohort.mjs',
+   how: 'Built by `scripts/applied/cohort.mjs` from the files in `applied-systems/finance/cohort-economics/examples/`.'},
+];
+
+export const htmlPath = adoc => adoc.replace(/\.adoc$/, '.html');
+
+export function title(text) {
+  const m = /^= (.+)$/m.exec(text);
+  if (!m) throw new Error('view has no document title');
+  return m[1].trim();
+}
+
+// The header of a view is its leading `//` comment lines.
+export function header(text) {
+  return text.split('\n').filter((l, i, a) => a.slice(0, i + 1).every(x => x.startsWith('//'))).join(' ');
+}
+
+export function frontPage(read) {
+  const rows = VIEWS.map(v => {
+    const text = read(v.file);
+    const head = header(text) + ' ' + text.split('\n').slice(0, 40).join(' ');
+    if (!head.includes(v.needs)) throw new Error(`${v.file}: header does not name ${v.needs}`);
+    return `|link:${htmlPath(v.file)}[${title(text)}]\n|${v.how}`;
+  });
+  return [
+    '// SPDX-License-Identifier: CC-BY-SA-4.0',
+    '// GENERATED by scripts/site/site.mjs; do not hand-edit.',
+    '= Mathesis atlas',
+    '',
+    'Mathesis is the maths section of the estate. These pages are generated views',
+    'of public data. Each view says what it was built from. Mathesis derives status',
+    'from receipts and does not assert it.',
+    '',
+    '[cols="2,5",options="header"]',
+    '|===',
+    '|View |How it is derived',
+    '',
+    rows.join('\n\n'),
+    '|===',
+    '',
+    `The source is in ${GITHUB}[the repository].`,
+    '',
+  ].join('\n');
+}
+
+const attrRe = /\b(href|src)="([^"]*)"/g;
+
+// Check every relative link of one page. `siteHas(rel)` tells whether a path
+// is in the site; `repoHas(rel)` whether it is in the repository. Returns the
+// rewritten HTML and the list of failures.
+export function checkLinks(page, html, siteHas, repoHas, idsOf) {
+  const errors = [];
+  const dir = path.posix.dirname(page);
+  const out = html.replace(attrRe, (whole, attr, url) => {
+    if (url === '' || url.startsWith('#') && !url.slice(1)) return whole;
+    if (/^[a-z][a-z0-9+.-]*:/i.test(url) || url.startsWith('//')) return whole;
+    const frag = url.includes('#') ? url.slice(url.indexOf('#')) : '';
+    const cut = url.search(/[?#]/);
+    const rel = cut < 0 ? url : url.slice(0, cut);
+    if (rel === '') { // in-page anchor
+      if (frag.length > 1 && !idsOf(page).has(decodeURIComponent(frag.slice(1)))) errors.push(`${page}: no anchor ${frag}`);
+      return whole;
+    }
+    const target = path.posix.normalize(path.posix.join(dir, rel));
+    if (target.startsWith('..')) { errors.push(`${page}: link leaves the repository: ${url}`); return whole; }
+    const asHtml = htmlPath(target);
+    if (siteHas(asHtml)) {
+      if (frag.length > 1 && !idsOf(asHtml).has(decodeURIComponent(frag.slice(1)))) errors.push(`${page}: no anchor ${frag} in ${asHtml}`);
+      return `${attr}="${htmlPath(rel)}${frag}"`;
+    }
+    if (siteHas(target)) return whole;
+    if (repoHas(target)) return `${attr}="${GITHUB}/blob/main/${target.replace(/\/$/, '')}${frag}"`;
+    errors.push(`${page}: broken relative link ${url} (not in the site, not in the repository)`);
+    return whole;
+  });
+  return {html: out, errors};
+}
+
+const walk = (root, dir = '') => readdirSync(path.join(root, dir)).flatMap(n => {
+  const rel = path.posix.join(dir, n);
+  return statSync(path.join(root, rel)).isDirectory() ? walk(root, rel) : [rel];
+});
+
+// Find asciidoctor in the absolute directories of PATH (or take ASCIIDOCTOR), and
+// run it by its absolute path, so no relative PATH entry can pick the program.
+export function findAsciidoctor(env = process.env) {
+  if (env.ASCIIDOCTOR) return env.ASCIIDOCTOR;
+  for (const d of (env.PATH || '').split(path.delimiter)) {
+    if (path.isAbsolute(d) && existsSync(path.join(d, 'asciidoctor'))) return path.join(d, 'asciidoctor');
+  }
+  throw new Error('asciidoctor not found in an absolute directory of PATH (set ASCIIDOCTOR to its path)');
+}
+
+function asciidoctor(args) {
+  const r = spawnSync(findAsciidoctor(), ['-S', 'safe', '-B', '/', '--failure-level=WARN', '-a', 'nofooter', '-a', 'webfonts!', ...args], {encoding: 'utf8'});
+  if (r.error) throw new Error(`asciidoctor not runnable: ${r.error.message}`);
+  process.stderr.write(r.stderr || '');
+  if (r.status !== 0) throw new Error(`asciidoctor failed (status ${r.status})`);
+}
+
+export function build(root, out) {
+  const read = f => readFileSync(path.join(root, f), 'utf8');
+  mkdirSync(out, {recursive: true});
+  const stage = mkdtempSync(path.join(tmpdir(), 'mathesis-site-'));
+  writeFileSync(path.join(stage, 'index.adoc'), frontPage(read));
+  asciidoctor(['-D', out, path.join(stage, 'index.adoc')]);
+  asciidoctor(['-R', root, '-D', out, ...VIEWS.map(v => path.join(root, v.file))]);
+
+  const pages = walk(out).filter(f => f.endsWith('.html'));
+  const files = new Set(walk(out));
+  const ids = new Map();
+  const idsOf = p => ids.get(p) ?? ids.set(p, new Set([...readFileSync(path.join(out, p), 'utf8').matchAll(/\bid="([^"]+)"/g)].map(m => m[1]))).get(p);
+  const errors = [];
+  for (const p of pages) {
+    const r = checkLinks(p, readFileSync(path.join(out, p), 'utf8'), x => files.has(x), x => existsSync(path.join(root, x)), idsOf);
+    writeFileSync(path.join(out, p), r.html);
+    errors.push(...r.errors);
+  }
+  for (const v of VIEWS) if (!files.has(htmlPath(v.file))) errors.push(`missing page ${htmlPath(v.file)}`);
+  if (errors.length) throw new Error(errors.join('\n'));
+  return pages;
+}
+
+if (import.meta.main) {
+  const [cmd, outArg] = process.argv.slice(2);
+  if (cmd !== 'build') { console.error('usage: site.mjs build OUT'); process.exit(2); }
+  const root = path.resolve(import.meta.dir, '../..');
+  const out = path.resolve(outArg || mkdtempSync(path.join(tmpdir(), 'mathesis-site-out-')));
+  try {
+    const pages = build(root, out);
+    console.log(`site: ${pages.length} pages in ${out}`);
+  } catch (e) { console.error(`site: FAIL\n${e.message}`); process.exit(1); }
+}

tests/site/site.test.mjs

@@ -0,0 +1,57 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+import {test, expect} from 'bun:test';
+import {readFileSync} from 'node:fs';
+import {VIEWS, frontPage, checkLinks, htmlPath, findAsciidoctor, GITHUB} from '../../scripts/site/site.mjs';
+
+const root = new URL('../../', import.meta.url).pathname;
+const read = f => readFileSync(root + f, 'utf8');
+
+test('the front page links every view and says how each is derived', () => {
+  const page = frontPage(read);
+  for (const v of VIEWS) {
+    expect(page).toContain(`link:${htmlPath(v.file)}[`);
+    expect(page).toContain(v.how);
+  }
+  expect(page).toContain('GENERATED by scripts/site/site.mjs');
+});
+
+test('the front page fails when a view header no longer names its source', () => {
+  const bad = f => read(f).replaceAll('claims-registry.mjs', 'x').replaceAll('census/rows.jsonl', 'x');
+  expect(() => frontPage(bad)).toThrow(/header does not name/);
+});
+
+const none = () => new Set();
+const run = (html, site, repo, page = 'docs/a/x.html', ids = none) =>
+  checkLinks(page, html, p => site.includes(p), p => repo.includes(p), ids);
+
+test('a link to another page of the site becomes an .html link', () => {
+  const r = run('<a href="y.adoc">y</a>', ['docs/a/y.html'], []);
+  expect(r.errors).toEqual([]);
+  expect(r.html).toBe('<a href="y.html">y</a>');
+});
+
+test('a link to a repository file outside the site becomes a GitHub link at main', () => {
+  const r = run('<a href="../README.adoc#top">r</a>', [], ['docs/README.adoc']);
+  expect(r.errors).toEqual([]);
+  expect(r.html).toBe(`<a href="${GITHUB}/blob/main/docs/README.adoc#top">r</a>`);
+});
+
+test('a link to a file that exists nowhere fails', () => {
+  expect(run('<a href="gone.adoc">g</a>', [], []).errors[0]).toMatch(/broken relative link/);
+});
+
+test('a link that leaves the repository fails', () => {
+  expect(run('<a href="../../../x">g</a>', [], [], 'a/x.html').errors[0]).toMatch(/leaves the repository/);
+});
+
+test('a missing anchor fails, and absolute and in-page links pass', () => {
+  expect(run('<a href="y.html#nope">y</a>', ['docs/a/y.html'], []).errors[0]).toMatch(/no anchor/);
+  const ids = () => new Set(['top']);
+  expect(run('<a href="#top">t</a><a href="https://example.org/x">e</a>', [], [], 'docs/a/x.html', ids).errors).toEqual([]);
+});
+
+test('asciidoctor is found only in an absolute directory of PATH', () => {
+  expect(findAsciidoctor({ASCIIDOCTOR: '/x/asciidoctor'})).toBe('/x/asciidoctor');
+  expect(() => findAsciidoctor({PATH: 'relative/dir'})).toThrow(/not found/);
+});