diff --git a/Justfile b/Justfile index 68f23be..141e7d1 100644 --- a/Justfile +++ b/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/ diff --git a/build/manifest.scm b/build/manifest.scm index bddd657..34259e6 100644 --- a/build/manifest.scm +++ b/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")) diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index f2dfaff..c6f9c5d 100644 --- a/docs/status/ROADMAP.adoc +++ b/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 diff --git a/scripts/site/site.mjs b/scripts/site/site.mjs new file mode 100644 index 0000000..e1bbdb1 --- /dev/null +++ b/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); } +} diff --git a/tests/site/site.test.mjs b/tests/site/site.test.mjs new file mode 100644 index 0000000..2570e72 --- /dev/null +++ b/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('y', ['docs/a/y.html'], []); + expect(r.errors).toEqual([]); + expect(r.html).toBe('y'); +}); + +test('a link to a repository file outside the site becomes a GitHub link at main', () => { + const r = run('r', [], ['docs/README.adoc']); + expect(r.errors).toEqual([]); + expect(r.html).toBe(`r`); +}); + +test('a link to a file that exists nowhere fails', () => { + expect(run('g', [], []).errors[0]).toMatch(/broken relative link/); +}); + +test('a link that leaves the repository fails', () => { + expect(run('g', [], [], 'a/x.html').errors[0]).toMatch(/leaves the repository/); +}); + +test('a missing anchor fails, and absolute and in-page links pass', () => { + expect(run('y', ['docs/a/y.html'], []).errors[0]).toMatch(/no anchor/); + const ids = () => new Set(['top']); + expect(run('te', [], [], '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/); +});