From eb8ce3818cf3113f1854a25d860754ec4f7eda01 Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 22:21:33 +0000 Subject: [PATCH 1/6] Make the reader's fresh-run instructions and source map usable --- README.md | 69 ++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 50 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 38effc1..d186014 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,9 @@ You do not have to search the authors' files to find the Lean for a sentence. [![A paper on the left page with one sentence highlighted, and on the right the graph of its Lean proof above the exact Lean lines the sentence describes.](web/public/reader.webp)](https://wcook04.github.io/proof-reader/#/contextual-embeddings) +For a specific example, [open the paper at isoR's CLam case](https://wcook04.github.io/proof-reader/#/contextual-embeddings/@isoR-clam), +linked to Lean lines 217 to 221. + - As you scroll, the statement a third of the way down the page is highlighted, and its card on the graph is outlined. Cards carry plain titles, with the Lean name small beneath. - The right pane has two modes, Graph and Lean, with a toggle at its top. Click a statement or @@ -62,21 +65,35 @@ trust before extracting it. ## Run the site +Use Python 3.11 or later, Node 20.19 or later, and [Poppler](https://poppler.freedesktop.org/) +(`brew install poppler` on macOS; `sudo apt-get install poppler-utils` on Ubuntu). +From a fresh clone: + ```sh +git clone https://github.com/wcook04/proof-reader.git +cd proof-reader +cd web +npm ci +cd .. +python3 tools/paper.py build cd web -npm install npm run dev ``` -Open the address it prints. `npm run build` writes a static site to `web/dist`; set -`VITE_BASE_PATH` to the folder it will be served from. +Open the address it prints and choose *Contextual Embeddings*. The paper build creates +the data the site needs; it uses the checked-in Lean extraction, so running the existing +paper does not require Lean. After changing a paper's files, run `python3 tools/paper.py build` +again from the repository root. + +From `web/`, `npm run build` writes a static site to `web/dist`; set `VITE_BASE_PATH` +to the folder it will be served from. `npm run preview` serves that built site locally. To walk a reader's whole visit in a real browser, build for the public path and run the journey. It needs Playwright for Python, and takes `--browser firefox` or `webkit` as well: ```sh cd web && VITE_BASE_PATH=/proof-reader/ npm run build && cd .. -python tests/journey.py --shots /tmp/journey +python3 tests/journey.py --shots /tmp/journey ``` `tests/speed.py` measures a paper's first screen on a home connection. @@ -101,25 +118,39 @@ has reviewed them. ## Repository map -| Path | What it holds | +Authored paper files and the checked-in Lean extraction live under `papers/`. +`tools/paper.py build` turns them into `web/public/papers/`; Vite then packages those +files with the website in `web/dist/`. Both output directories are ignored by Git: +change their sources and rebuild them. + +| Source | What it holds | | --- | --- | -| `papers/` | One folder for each paper | -| `skills/add-paper/` | How to fill in a new paper | -| `tools/paper.py` | Extract the Lean, compare with the PDF and build the data | -| `tools/transcribe.py` | Draft a paper's reading text from its PDF | -| `tools/reading.py` | Compare the reading copy with the PDF and mark its linked statements | -| `web/tools/render-paper.mjs` | Typeset `paper.md` with Markdown and KaTeX | -| `tools/extract.lean.template` | The Lean program that lists a project's declarations | -| `web/` | The website | -| `web/src/map/` | The map, copied from [lean-exposition](https://github.com/wcook04/lean-exposition) | -| `web/src/app/history.ts` | What one history entry remembers | -| `web/src/proof/` | The right page: graph, Lean, handle | -| `tests/journey.py` | A reader's whole visit, in a real browser | +| [papers/](papers/) | One folder for each paper | +| [skills/add-paper/](skills/add-paper/) | How to fill in a new paper | +| [tools/paper.py](tools/paper.py) | Extract the Lean, compare with the PDF and build the data | +| [tools/transcribe.py](tools/transcribe.py) | Draft a paper's reading text from its PDF | +| [tools/reading.py](tools/reading.py) | Compare the reading copy with the PDF and mark its linked statements | +| [render-paper.mjs](web/tools/render-paper.mjs) | Typeset `paper.md` with Markdown and KaTeX | +| [extract.lean.template](tools/extract.lean.template) | The Lean program that lists a project's declarations | +| [web/](web/) | The website | +| [web/src/map/](web/src/map/) | The map, copied from [lean-exposition](https://github.com/wcook04/lean-exposition) | +| [history.ts](web/src/app/history.ts) | What one history entry remembers | +| [web/src/proof/](web/src/proof/) | The right page: graph, Lean, handle | +| [tests/](tests/) | Python unit tests and the browser [journey](tests/journey.py) | +| [Pages workflow](.github/workflows/pages.yml) | Check every paper, build the site and publish to GitHub Pages | + +## Related work and videos + +[Lean Exposition](https://github.com/wcook04/lean-exposition) provides a tool and writing +methods for preparing three explanations of a Lean result. Its +[reading website](https://wcook04.github.io/lean-exposition-site/) presents those draft +explanations beside the graph; [this video walks through that site](https://www.youtube.com/watch?v=sYMDcT7vyng). +Proof Reader's reading copy keeps the original paper's wording. ## Licence Code is Apache-2.0; see [LICENSE](LICENSE) and [NOTICE](NOTICE). Each paper and Lean project keeps its own licence and credit, named in its `paper.toml` and on its page. -Proof Reader is one of Will Cook's sites. All websites, code and videos are on -[my home page](https://wcook04.github.io/). +Proof Reader is one of Will Cook's sites. Find the other websites and code on +[my home page](https://wcook04.github.io/), and the [project videos](https://wcook04.github.io/#videos). From 166b376db6ec7258f635b85a586c218d720de6a1 Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 22:31:25 +0000 Subject: [PATCH 2/6] Remove retired reader paths and guard source ownership --- .github/workflows/pages.yml | 2 + AGENTS.md | 2 +- CONTRIBUTING.md | 8 +- README.md | 2 + web/package.json | 4 +- web/src/app/history.ts | 2 +- web/src/lean/LeanPane.tsx | 222 -------------------------------- web/src/map/MapView.tsx | 3 - web/src/map/scene.ts | 80 ------------ web/src/proof/MapPane.tsx | 2 +- web/tools/check-source.mjs | 80 ++++++++++++ web/tools/check-source.test.mjs | 98 ++++++++++++++ 12 files changed, 195 insertions(+), 310 deletions(-) delete mode 100644 web/src/lean/LeanPane.tsx delete mode 100644 web/src/map/MapView.tsx delete mode 100644 web/src/map/scene.ts create mode 100644 web/tools/check-source.mjs create mode 100644 web/tools/check-source.test.mjs diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index be607c3..3e99ecf 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -26,6 +26,8 @@ jobs: run: sudo apt-get update -qq && sudo apt-get install -y -qq poppler-utils - run: npm ci working-directory: web + - run: npm run test:source + working-directory: web - run: python -m unittest discover -s tests # Checks every link and every word of each reading copy against its PDF. - name: Check each paper and build its data diff --git a/AGENTS.md b/AGENTS.md index 0a98a75..5a67588 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -35,7 +35,7 @@ Before committing a change, run: ```sh python3 -m unittest discover -s tests python3 tools/paper.py check contextual-embeddings -cd web && VITE_BASE_PATH=/proof-reader/ npm run build && cd .. +cd web && npm run test:source && VITE_BASE_PATH=/proof-reader/ npm run build && cd .. python3 tests/journey.py ``` diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 808f7e1..76d2ca1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -20,7 +20,13 @@ Data flows one way: `papers//` to `tools/paper.py` to `web/public/papers/` python3 -m unittest discover -s tests python3 tools/paper.py check contextual-embeddings python3 tools/paper.py build -cd web && npm ci && npm run build +cd web && npm ci && npm run test:source && npm run build ``` +`npm run check:source` checks that each reader source file has an entry point. +The copied map engine's drawing diagnostics are a separate developer entry. +Use `npm run check:source -- --index` to check staged source before committing. +The check follows literal module imports and local CSS references; extend it with +a fixture before introducing computed imports or `import.meta.glob`. + Look at any visual change in a browser at laptop and monitor widths. diff --git a/README.md b/README.md index d186014..448eda8 100644 --- a/README.md +++ b/README.md @@ -135,7 +135,9 @@ change their sources and rebuild them. | [web/](web/) | The website | | [web/src/map/](web/src/map/) | The map, copied from [lean-exposition](https://github.com/wcook04/lean-exposition) | | [history.ts](web/src/app/history.ts) | What one history entry remembers | +| [web/src/lean/](web/src/lean/) | Shared Lean code rendering and tokens | | [web/src/proof/](web/src/proof/) | The right page: graph, Lean, handle | +| [check-source.mjs](web/tools/check-source.mjs) | Reject source files with no entry point; run with `npm run check:source` in `web/` | | [tests/](tests/) | Python unit tests and the browser [journey](tests/journey.py) | | [Pages workflow](.github/workflows/pages.yml) | Check every paper, build the site and publish to GitHub Pages | diff --git a/web/package.json b/web/package.json index 8a63475..91a5694 100644 --- a/web/package.json +++ b/web/package.json @@ -10,7 +10,9 @@ }, "scripts": { "dev": "vite", - "build": "tsc --noEmit && vite build", + "build": "npm run check:source && tsc --noEmit && vite build", + "check:source": "node tools/check-source.mjs", + "test:source": "node --test tools/check-source.test.mjs", "preview": "vite preview", "typecheck": "tsc --noEmit" }, diff --git a/web/src/app/history.ts b/web/src/app/history.ts index d13ca79..b7d27c1 100644 --- a/web/src/app/history.ts +++ b/web/src/app/history.ts @@ -4,7 +4,7 @@ // Opening something pushes an entry. Following and pointing only rewrite the // entry they are in. -import type { MapScene } from "../map/scene"; +import type { MapScene } from "../map/canvas/scene"; export type Copy = "reading" | "pdf"; export type Tab = "step" | "index" | "file"; diff --git a/web/src/lean/LeanPane.tsx b/web/src/lean/LeanPane.tsx deleted file mode 100644 index 1ec36f5..0000000 --- a/web/src/lean/LeanPane.tsx +++ /dev/null @@ -1,222 +0,0 @@ -// The right-hand page: the authors' Lean file, with the declaration being read -// lined up beside its sentence. Above it, what Lean reports about that -// declaration and any note, kept short so the file stays the subject. - -import { useEffect, useMemo, useRef, type CSSProperties } from "react"; -import type { Declaration, Edition } from "../app/edition"; -import { isType } from "../model/fromEdition"; -import { READING_LINE } from "../paper/reading-line"; -import { tokenizeLean } from "./leanTokens"; - -const KIND_WORDS: Record = { - theorem: "Theorem", - lemma: "Lemma", - def: "Definition", - abbrev: "Definition", - instance: "Instance", - axiom: "Axiom", - inductive: "Type", - structure: "Type", - class: "Type class", - opaque: "Definition", -}; - -interface Props { - edition: Edition; - selected: string | null; - /** Every declaration the passage being read is about. */ - reading: string[]; - onSelect(id: string): void; - onPassage(id: string): void; - /** The exact lines the sentence being read describes, when it names them. */ - exact: [number, number] | null; - /** A line for the reader above the Lean: how to begin, or that nothing here is tied. */ - notice: string | null; - /** Present when the reader came here from the map. */ - onBack?(): void; -} - -export function LeanPane({ edition, selected, reading, exact, notice, onSelect, onPassage, onBack }: Props) { - const declaration = edition.declarations.find((d) => d.id === selected) ?? edition.declarations.find((d) => reading.includes(d.id)) ?? null; - const file = declaration?.file ?? Object.keys(edition.lean.files)[0]; - const lit = useMemo(() => edition.declarations.filter((d) => reading.includes(d.id) && d.file === file), [edition, file, reading]); - return ( - - ); -} - -function Head({ edition, d, onSelect, onPassage }: { edition: Edition; d: Declaration; onSelect(id: string): void; onPassage(id: string): void }) { - const isProof = d.keyword === "theorem" || d.keyword === "lemma"; - const passages = d.passages.map((id) => edition.passages.find((p) => p.id === id)).filter((p) => !!p); - const pages = passages.filter((p, index) => passages.findIndex((other) => other.page === p.page) === index); - const severalFiles = Object.keys(edition.lean.files).length > 1; - return ( - <> -

- {d.id} - {KIND_WORDS[d.keyword] ?? d.keyword}, {severalFiles ? `${d.file.split("/").pop()}, ` : ""}lines {d.line} to {d.end_line} -

- {d.keyword === "axiom" &&

Assumed, not proved. Lean takes this as given.

} - {isProof && ( -

- {d.axioms.length ? ( - <> - Lean reports this rests on{" "} - {d.axioms.map((a) => ( - - ))} - - ) : ( - <>Lean reports this uses none of the authors’ axioms. - )} -

- )} - {d.note &&

{d.note.text}

} - {!isType(d) && d.used_by.length > 0 && ( -

- Used by{" "} - {d.used_by.map((name) => ( - - ))} -

- )} - {pages.length > 1 && ( -

- In the paper at{" "} - {pages.map((p) => ( - - ))} -

- )} - - ); -} - -interface Piece { - text: string; - kind: string; -} - -/** Split a file into lines of tokens, setting the authors' comments apart from code. */ -function lineTokens(text: string): Piece[][] { - let inBlock = false; - return text.split("\n").map((line) => { - const pieces: Piece[] = []; - let rest = line; - while (rest) { - if (inBlock) { - const close = rest.indexOf("-/"); - const end = close < 0 ? rest.length : close + 2; - pieces.push({ text: rest.slice(0, end), kind: "prose" }); - rest = rest.slice(end); - if (close >= 0) inBlock = false; - continue; - } - const block = rest.indexOf("/-"); - const dash = rest.indexOf("--"); - const start = block >= 0 && (dash < 0 || block < dash) ? block : dash; - const code = start < 0 ? rest : rest.slice(0, start); - if (code) for (const token of tokenizeLean(code)) pieces.push({ text: token.text, kind: token.kind }); - if (start < 0) break; - rest = rest.slice(start); - if (start === dash && (block < 0 || dash < block)) { - pieces.push({ text: rest, kind: "comment" }); - break; - } - inBlock = true; - pieces.push({ text: rest.slice(0, 2), kind: "prose" }); - rest = rest.slice(2); - } - return pieces; - }); -} - -interface SourceProps { - name: string; - text: string; - focus: Declaration | null; - lit: Declaration[]; - exact: [number, number] | null; - known: Declaration[]; - onSelect(id: string): void; -} - -function Source({ name, text, focus, lit, exact, known, onSelect }: SourceProps) { - const lines = useMemo(() => tokenLines(text), [text]); - const names = useMemo(() => new Set(known.map((d) => d.id)), [known]); - const body = useRef(null); - - // Bring the declaration level with the paper's reading line, so the sentence - // and its Lean sit side by side. - useEffect(() => { - if (!focus) return; - const el = body.current; - const row = el?.querySelector(`[data-line="${exact ? exact[0] : focus.line}"]`); - const paper = document.querySelector("[data-paper-pane]"); - if (!el || !row || !paper) return; - const align = (behavior: ScrollBehavior) => { - const line = paper.getBoundingClientRect().top + paper.clientHeight * READING_LINE; - // Level with the paper's reading line where that falls inside this pane; a tall - // head or a stacked phone layout can put it above, and the code must still show. - const room = Math.max(14, Math.min(line - el.getBoundingClientRect().top, el.clientHeight * 0.6)); - el.scrollTo({ top: row.offsetTop - room + 11, behavior }); - }; - const reduced = window.matchMedia("(prefers-reduced-motion: reduce)").matches; - align(reduced ? "auto" : "smooth"); - // The code font can arrive after this and rewrap the lines, so level up again. - let live = true; - void document.fonts.ready.then(() => live && align("auto")); - const observer = new ResizeObserver(() => align("auto")); - observer.observe(el); - return () => { - live = false; - observer.disconnect(); - }; - }, [exact, focus]); - - return ( -
- - {lines.map((pieces, index) => { - const line = index + 1; - const within = (d: Declaration) => line >= d.line && line <= d.end_line; - const on = lit.some(within) ? " is-on" : ""; - const isFocus = focus && within(focus) ? " is-on" : ""; - const isExact = exact && line >= exact[0] && line <= exact[1] ? " is-exact" : ""; - // A long line wraps under its own code, so nesting stays readable. - const indent = /^ */.exec(pieces.map((piece) => piece.text).join(""))?.[0].length ?? 0; - return ( - - - - {pieces.map((piece, i) => { - // Types take one colour on both pages, so the same name reads the same. - const typed = piece.kind === "ident" && /^[A-Z]/.test(piece.text); - if (names.has(piece.text)) { - return ( - - ); - } - if (piece.kind === "space" || piece.kind === "punct") return piece.text; - return {piece.text}; - })} - {"\n"} - - - ); - })} - -
- ); -} - -const tokenLines = lineTokens; diff --git a/web/src/map/MapView.tsx b/web/src/map/MapView.tsx deleted file mode 100644 index 60e87c8..0000000 --- a/web/src/map/MapView.tsx +++ /dev/null @@ -1,3 +0,0 @@ -// The map component used by other pages. It is the goal-first argument tree; -// see ArgumentTree.tsx. Kept under this name so pages can import "MapView". -export { ArgumentTree as MapView, type Insets, type MapViewHandle, type TreeProps as MapViewProps } from "./ArgumentTree"; diff --git a/web/src/map/scene.ts b/web/src/map/scene.ts deleted file mode 100644 index f869bad..0000000 --- a/web/src/map/scene.ts +++ /dev/null @@ -1,80 +0,0 @@ -// The map's remembered scene, kept per history entry so Back returns the reader -// to the camera, unfolded branches and representation they left. The URL holds -// what is selected; the history entry's state holds how it was being looked at. -// -// Pan and zoom only ever replace the current entry's state (never push), and -// other owners' keys in history.state (the reader keeps its own) are merged, -// never overwritten. - -import type { MapScene } from "./ArgumentTree"; - -export type { MapScene }; - -const KEY = "mapScene"; -const DELAY = 200; - -function stateObject(): Record { - const s = window.history.state as unknown; - return s && typeof s === "object" ? { ...(s as Record) } : {}; -} - -const finite = (v: unknown): v is number => typeof v === "number" && Number.isFinite(v); - -/** A scene as stored, if it is well formed and every record it names is in this edition. */ -export function validScene(value: unknown, has: (id: string) => boolean): MapScene | null { - if (!value || typeof value !== "object") return null; - const v = value as Partial; - const c = v.camera; - if (!c || !finite(c.x) || !finite(c.y) || !finite(c.k) || c.k <= 0) return null; - if (!Array.isArray(v.expanded) || !v.expanded.every((id) => typeof id === "string" && has(id))) return null; - if (v.mode !== "steps" && v.mode !== "overview") return null; - const a = v.anchor; - const anchor = a && typeof a.id === "string" && has(a.id) && finite(a.x) && finite(a.y) ? { id: a.id, x: a.x, y: a.y } : undefined; - return { camera: { x: c.x, y: c.y, k: c.k }, expanded: [...v.expanded], mode: v.mode, ...(anchor ? { anchor } : {}) }; -} - -/** The scene remembered for the current history entry, or null. */ -export function readScene(has: (id: string) => boolean): MapScene | null { - return validScene(stateObject()[KEY], has); -} - -function write(scene: MapScene, href: string) { - // The entry may have changed since the scene settled; never write into another page's entry. - if (window.location.href !== href) return; - try { - window.history.replaceState({ ...stateObject(), [KEY]: scene }, ""); - } catch { - /* history state unavailable (sandboxed frames) */ - } -} - -/** Debounced writes of the settled scene into the current entry. */ -export function sceneWriter() { - let timer: ReturnType | null = null; - let pending: { scene: MapScene; href: string } | null = null; - const cancel = () => { - if (timer) clearTimeout(timer); - timer = null; - pending = null; - }; - return { - /** Remember this scene for the current entry after a short quiet period. */ - save(scene: MapScene) { - if (timer) clearTimeout(timer); - pending = { scene, href: window.location.href }; - timer = setTimeout(() => { - const p = pending; - cancel(); - if (p) write(p.scene, p.href); - }, DELAY); - }, - /** Write now (before leaving the entry), preferring a fresh scene when one is given. */ - flush(scene?: MapScene | null) { - const p = pending; - cancel(); - if (scene) write(scene, window.location.href); - else if (p) write(p.scene, p.href); - }, - cancel, - }; -} diff --git a/web/src/proof/MapPane.tsx b/web/src/proof/MapPane.tsx index 1104d48..6bfa3bd 100644 --- a/web/src/proof/MapPane.tsx +++ b/web/src/proof/MapPane.tsx @@ -8,7 +8,7 @@ import { memo, useCallback, useEffect, useImperativeHandle, useLayoutEffect, useMemo, useRef, useState, type Ref } from "react"; import type { Edition } from "../app/edition"; import { ArgumentTree, type Insets, type MapViewHandle } from "../map/ArgumentTree"; -import type { MapScene } from "../map/scene"; +import type { MapScene } from "../map/canvas/scene"; import { isType } from "../model/fromEdition"; import type { ArgGraph } from "../model/graph"; diff --git a/web/tools/check-source.mjs b/web/tools/check-source.mjs new file mode 100644 index 0000000..2e72261 --- /dev/null +++ b/web/tools/check-source.mjs @@ -0,0 +1,80 @@ +// Keep retired UI implementations out of the maintained source tree. TypeScript +// checks imports, but does not report whole files that nothing imports. +// Follow literal module imports and local CSS references. Extend this check and +// its fixtures before introducing computed imports or import.meta.glob. +import { execFileSync } from "node:child_process"; +import { existsSync, readFileSync } from "node:fs"; +import { dirname, posix, resolve } from "node:path"; +import { fileURLToPath } from "node:url"; +import ts from "typescript"; + +const WEB = resolve(dirname(fileURLToPath(import.meta.url)), ".."); +const ENTRIES = [ + "src/main.tsx", + // Developer diagnostics for the copied map engine, not part of the reader bundle. + "src/map/engine/audit.ts", +]; + +/** Inspect Git candidates, or staged contents when checking the proposed commit. */ +export function checkSource(web = WEB, { index = false } = {}) { + const git = (...args) => execFileSync("git", args, { cwd: web, encoding: "utf8", stdio: ["ignore", "pipe", "pipe"] }); + const prefix = git("rev-parse", "--show-prefix").trim(); + const args = ["ls-files", "-z", "--cached"]; + if (!index) args.push("--others", "--exclude-standard"); + const candidates = new Set(git(...args, "--", "src/").split("\0").filter((file) => file.startsWith("src/"))); + const source = new Map(); + for (const file of candidates) { + // A tracked deletion is absent from the working tree but may still be in the index. + if (!index && !existsSync(resolve(web, file))) continue; + source.set(file, index ? git("show", `:${prefix}${file}`) : readFileSync(resolve(web, file), "utf8")); + } + const errors = []; + const edges = new Map(); + for (const [file, text] of source) { + const css = file.endsWith(".css"); + const imports = /\.[cm]?[jt]sx?$/.test(file) + ? ts.preProcessFile(text, true, true).importedFiles.map((item) => item.fileName) + : css ? [...text.matchAll(/@import\s+['"](\.[^'"]+)['"]|url\(\s*['"]?([^'"()]+?)['"]?\s*\)/g)].map((match) => match[1] ?? match[2]) : []; + const targets = []; + for (const name of imports.filter((name) => css ? !/^(?:[a-z]+:|\/|#)/i.test(name) : name.startsWith("."))) { + const base = posix.normalize(posix.join(posix.dirname(file), name.split(/[?#]/)[0])); + const target = ["", ".ts", ".tsx", ".js", ".jsx", ".css", ".json", "/index.ts", "/index.tsx"].map((suffix) => base + suffix).find((candidate) => source.has(candidate)); + if (target) targets.push(target); + else errors.push(`${file}: local import ${name} has no source file`); + } + edges.set(file, targets); + } + const reached = new Set(); + function visit(file) { + if (reached.has(file)) return; + reached.add(file); + for (const target of edges.get(file) ?? []) visit(target); + } + for (const entry of ENTRIES) { + if (!source.has(entry)) errors.push(`Missing source entry: ${entry}`); + else visit(entry); + } + for (const file of source.keys()) { + if (!reached.has(file)) errors.push(`Unused source file: ${file}`); + } + return errors; +} + +if (process.argv[1] && resolve(process.argv[1]) === fileURLToPath(import.meta.url)) { + const args = process.argv.slice(2); + if (args.some((arg) => arg !== "--index")) { + console.error("Usage: node tools/check-source.mjs [--index]"); + process.exitCode = 2; + } else { + try { + const errors = checkSource(WEB, { index: args.includes("--index") }); + if (errors.length) { + console.error(errors.join("\n")); + process.exitCode = 1; + } else console.log("Source tree: all reader files and map diagnostics have an entry point."); + } catch (error) { + console.error(`Cannot check source tree: ${error.message}`); + process.exitCode = 1; + } + } +} diff --git a/web/tools/check-source.test.mjs b/web/tools/check-source.test.mjs new file mode 100644 index 0000000..160a14b --- /dev/null +++ b/web/tools/check-source.test.mjs @@ -0,0 +1,98 @@ +import assert from "node:assert/strict"; +import { execFileSync } from "node:child_process"; +import { mkdtempSync, mkdirSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { dirname, join } from "node:path"; +import { test } from "node:test"; +import { checkSource } from "./check-source.mjs"; + +function fixture(t) { + const root = mkdtempSync(join(tmpdir(), "proof-reader-source-test-")); + t.after(() => rmSync(root, { recursive: true, force: true })); + const git = (...args) => execFileSync("git", args, { cwd: root, stdio: "pipe" }); + const write = (file, text = "export {};") => { + mkdirSync(dirname(join(root, file)), { recursive: true }); + writeFileSync(join(root, file), text); + }; + git("init", "-q"); + write("src/main.tsx"); + write("src/map/engine/audit.ts"); + return { root, git, write }; +} + +test("keeps the reader and explicit map diagnostic entries", (t) => { + const { root } = fixture(t); + assert.deepEqual(checkSource(root), []); +}); + +test("follows static, dynamic, type, CSS and JSON imports", (t) => { + const { root, write } = fixture(t); + write("src/main.tsx", 'import "./base.css"; import data from "./data.json"; import image from "./paper.svg?url"; import type { T } from "./types"; export { child } from "./child"; import("./lazy");'); + write("src/base.css", '@import "katex/dist/katex.min.css"; @import "./other.css"; body { background: url(paper.svg#layer); }'); + write("src/other.css", "body {}"); + write("src/paper.svg", ""); + write("src/data.json", "{}"); + write("src/types.ts", "export type T = string;"); + write("src/child/index.ts", "export const child = 1;"); + write("src/lazy.ts"); + assert.deepEqual(checkSource(root), []); +}); + +test("rejects an unreferenced UI implementation and a stale import", (t) => { + const { root, write } = fixture(t); + write("src/old/LeanPane.tsx"); + write("src/main.tsx", 'import "./missing";'); + assert.deepEqual(checkSource(root), [ + "src/main.tsx: local import ./missing has no source file", + "Unused source file: src/old/LeanPane.tsx", + ]); +}); + +test("does not descend into ignored outputs or unrelated tools", (t) => { + const { root, write } = fixture(t); + write(".gitignore", "/src/generated/\n/dist/\n"); + write("src/generated/cache.ts"); + write("dist/chunk.ts"); + write("tools/helper.ts"); + assert.deepEqual(checkSource(root), []); +}); + +test("uses staged source even when the working tree was repaired", (t) => { + const { root, git, write } = fixture(t); + write("src/main.tsx", 'import "./missing";'); + git("add", "."); + write("src/main.tsx"); + assert.deepEqual(checkSource(root), []); + assert.deepEqual(checkSource(root, { index: true }), ["src/main.tsx: local import ./missing has no source file"]); +}); + +test("distinguishes staged additions, working deletions and staged deletions", (t) => { + const { root, git, write } = fixture(t); + write("src/retired.ts"); + git("add", "."); + rmSync(join(root, "src/retired.ts")); + assert.deepEqual(checkSource(root), []); + assert.deepEqual(checkSource(root, { index: true }), ["Unused source file: src/retired.ts"]); + git("rm", "--cached", "src/retired.ts"); + assert.deepEqual(checkSource(root, { index: true }), []); +}); + +test("reads the right index paths when web is nested below the Git root", (t) => { + const { root, git, write } = fixture(t); + write("web/src/main.tsx"); + write("web/src/map/engine/audit.ts"); + git("add", "."); + assert.deepEqual(checkSource(join(root, "web"), { index: true }), []); +}); + +test("rejects removal of the reader entry", (t) => { + const { root } = fixture(t); + rmSync(join(root, "src/main.tsx")); + assert.deepEqual(checkSource(root), ["Missing source entry: src/main.tsx"]); +}); + +test("fails clearly without Git", (t) => { + const { root } = fixture(t); + rmSync(join(root, ".git"), { recursive: true }); + assert.throws(() => checkSource(root), /git rev-parse/); +}); From d2ec95d37f219827bed5d5a43fe4330a045714dc Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 22:45:01 +0000 Subject: [PATCH 3/6] Keep source archive builds independent of Git --- .github/workflows/pages.yml | 12 ++++++++++++ CONTRIBUTING.md | 2 ++ web/tools/check-source.mjs | 28 +++++++++++++++++++++++---- web/tools/check-source.test.mjs | 34 +++++++++++++++++++++++++++++---- 4 files changed, 68 insertions(+), 8 deletions(-) diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 3e99ecf..278bd7f 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -40,6 +40,18 @@ jobs: working-directory: web env: VITE_BASE_PATH: /proof-reader/ + - name: Build the same site from a source archive + env: + VITE_BASE_PATH: /proof-reader/ + run: | + archive="$RUNNER_TEMP/proof-reader-source" + mkdir -p "$archive" + git archive HEAD | tar -x -C "$archive" + test ! -e "$archive/.git" + npm ci --prefix "$archive/web" + python "$archive/tools/paper.py" build + npm run build --prefix "$archive/web" + diff -qr web/dist "$archive/web/dist" - uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 with: path: web/dist diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 76d2ca1..daeecc8 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -26,6 +26,8 @@ cd web && npm ci && npm run test:source && npm run build `npm run check:source` checks that each reader source file has an entry point. The copied map engine's drawing diagnostics are a separate developer entry. Use `npm run check:source -- --index` to check staged source before committing. +Ordinary checks also work in a source ZIP or archive: without Git, they inspect +only `web/src/`. The `--index` option requires a Git checkout. The check follows literal module imports and local CSS references; extend it with a fixture before introducing computed imports or `import.meta.glob`. diff --git a/web/tools/check-source.mjs b/web/tools/check-source.mjs index 2e72261..7855d22 100644 --- a/web/tools/check-source.mjs +++ b/web/tools/check-source.mjs @@ -3,7 +3,7 @@ // Follow literal module imports and local CSS references. Extend this check and // its fixtures before introducing computed imports or import.meta.glob. import { execFileSync } from "node:child_process"; -import { existsSync, readFileSync } from "node:fs"; +import { existsSync, readdirSync, readFileSync } from "node:fs"; import { dirname, posix, resolve } from "node:path"; import { fileURLToPath } from "node:url"; import ts from "typescript"; @@ -15,13 +15,33 @@ const ENTRIES = [ "src/map/engine/audit.ts", ]; -/** Inspect Git candidates, or staged contents when checking the proposed commit. */ +// Source archives have no Git inventory. The maintained source lives entirely +// under src/; generated papers, bundles and dependencies are outside that tree. +function sourceFiles(web, folder = "src") { + if (!existsSync(resolve(web, folder))) return []; + return readdirSync(resolve(web, folder), { withFileTypes: true }).flatMap((entry) => { + const file = posix.join(folder, entry.name); + if (entry.isDirectory()) return sourceFiles(web, file); + return entry.isFile() ? [file] : []; + }); +} + +/** Inspect source files; use Git's exact staged contents only with --index. */ export function checkSource(web = WEB, { index = false } = {}) { const git = (...args) => execFileSync("git", args, { cwd: web, encoding: "utf8", stdio: ["ignore", "pipe", "pipe"] }); - const prefix = git("rev-parse", "--show-prefix").trim(); + let prefix; + // Do not borrow an unrelated ancestor's index when an archive is unpacked + // inside another checkout. This project's .git is beside web/, or at a test root. + const checkout = existsSync(resolve(web, "..", ".git")) || existsSync(resolve(web, ".git")); + try { + if (!checkout) throw new Error("No project Git metadata"); + prefix = git("rev-parse", "--show-prefix").trim(); + } catch (error) { + if (index) throw new Error("Staged source checking requires a Git checkout and Git.", { cause: error }); + } const args = ["ls-files", "-z", "--cached"]; if (!index) args.push("--others", "--exclude-standard"); - const candidates = new Set(git(...args, "--", "src/").split("\0").filter((file) => file.startsWith("src/"))); + const candidates = new Set(prefix === undefined ? sourceFiles(web) : git(...args, "--", "src/").split("\0").filter((file) => file.startsWith("src/"))); const source = new Map(); for (const file of candidates) { // A tracked deletion is absent from the working tree but may still be in the index. diff --git a/web/tools/check-source.test.mjs b/web/tools/check-source.test.mjs index 160a14b..0c33996 100644 --- a/web/tools/check-source.test.mjs +++ b/web/tools/check-source.test.mjs @@ -1,6 +1,6 @@ import assert from "node:assert/strict"; import { execFileSync } from "node:child_process"; -import { mkdtempSync, mkdirSync, rmSync, writeFileSync } from "node:fs"; +import { mkdtempSync, mkdirSync, rmSync, symlinkSync, writeFileSync } from "node:fs"; import { tmpdir } from "node:os"; import { dirname, join } from "node:path"; import { test } from "node:test"; @@ -91,8 +91,34 @@ test("rejects removal of the reader entry", (t) => { assert.deepEqual(checkSource(root), ["Missing source entry: src/main.tsx"]); }); -test("fails clearly without Git", (t) => { - const { root } = fixture(t); +test("checks a source archive without Git while keeping --index Git-only", (t) => { + const { root, write } = fixture(t); rmSync(join(root, ".git"), { recursive: true }); - assert.throws(() => checkSource(root), /git rev-parse/); + write("src/main.tsx", 'import "./active";'); + write("src/active.ts"); + write("dist/unused.ts"); + write("node_modules/package/unused.ts"); + assert.deepEqual(checkSource(root), []); + assert.throws(() => checkSource(root, { index: true }), /requires a Git checkout and Git/); + write("src/retired.ts"); + assert.deepEqual(checkSource(root), ["Unused source file: src/retired.ts"]); +}); + +test("does not follow directory links out of an archive's maintained source", (t) => { + const { root, write } = fixture(t); + rmSync(join(root, ".git"), { recursive: true }); + write("outside/unused.ts"); + symlinkSync(join(root, "outside"), join(root, "src", "external"), "dir"); + assert.deepEqual(checkSource(root), []); +}); + + +test("an archive nested in an unrelated Git checkout does not inherit its ignores or index", (t) => { + const { root, write } = fixture(t); + write(".gitignore", "/archive/\n"); + write("archive/web/src/main.tsx"); + write("archive/web/src/map/engine/audit.ts"); + const web = join(root, "archive", "web"); + assert.deepEqual(checkSource(web), []); + assert.throws(() => checkSource(web, { index: true }), /requires a Git checkout and Git/); }); From c677bfad7ffac74cec75e6f84ce8608e1b236b5e Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 22:48:53 +0000 Subject: [PATCH 4/6] Keep the site list in the central registry's order --- web/src/app/family.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/web/src/app/family.json b/web/src/app/family.json index c4829f5..ff7123d 100644 --- a/web/src/app/family.json +++ b/web/src/app/family.json @@ -4,9 +4,9 @@ "sites": [ { "id": "maths", "name": "Plectis Mathematics", "url": "https://wcook04.github.io/practical-formal-verification/map/" }, { "id": "lean-exposition", "name": "Lean Exposition", "url": "https://wcook04.github.io/lean-exposition-site/" }, + { "id": "proof-reader", "name": "Proof Reader", "url": "https://wcook04.github.io/proof-reader/" }, { "id": "atlas", "name": "Plectis Atlas", "url": "https://wcook04.github.io/plectis-atlas/" }, { "id": "formal-verification", "name": "Practical Formal Verification", "url": "https://wcook04.github.io/practical-formal-verification/explorer/" }, - { "id": "zenith", "name": "Zenith", "url": "https://wcook04.github.io/plectis-zenith/" }, - { "id": "proof-reader", "name": "Proof Reader", "url": "https://wcook04.github.io/proof-reader/" } + { "id": "zenith", "name": "Zenith", "url": "https://wcook04.github.io/plectis-zenith/" } ] } From 7cb42935d4e4a3badeab1470b602bf5a336194d7 Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 22:59:17 +0000 Subject: [PATCH 5/6] Explain the reader to newcomers --- README.md | 127 ++++++++++++++++++++++++++++-------------------------- 1 file changed, 65 insertions(+), 62 deletions(-) diff --git a/README.md b/README.md index 448eda8..52b14d2 100644 --- a/README.md +++ b/README.md @@ -1,30 +1,28 @@ # Proof Reader -Proof Reader shows a research paper beside its proof in [Lean](https://lean-lang.org), a -programming language whose compiler rejects a proof with a wrong step. You read the paper on the -left page as you read any paper. The right page holds a graph of the Lean proof, which moves to -the statement you are reading, and a click on a statement shows the authors' exact Lean lines. -You do not have to search the authors' files to find the Lean for a sentence. +Proof Reader displays a research paper beside its proof in +[Lean](https://lean-lang.org), a language for writing mathematical statements +and proofs that a computer can check. Click a linked statement in the paper to +open the authors' corresponding Lean code. You can also explore a diagram of +the proof steps and the connections between them. **[Read a paper in it](https://wcook04.github.io/proof-reader/#/contextual-embeddings)**: *Contextual Embeddings* by Frohlich, Foster, Kavvos and Wang (PLDI 2026), shown with the authors' Lean under CC BY 4.0. The links between the paper and the Lean were made with AI and have not been reviewed by the authors. [![A paper on the left page with one sentence highlighted, and on the right the graph of its Lean proof above the exact Lean lines the sentence describes.](web/public/reader.webp)](https://wcook04.github.io/proof-reader/#/contextual-embeddings) -For a specific example, [open the paper at isoR's CLam case](https://wcook04.github.io/proof-reader/#/contextual-embeddings/@isoR-clam), +For a specific example, [open a paragraph and its five linked lines of Lean](https://wcook04.github.io/proof-reader/#/contextual-embeddings/@isoR-clam), linked to Lean lines 217 to 221. -- As you scroll, the statement a third of the way down the page is highlighted, and its card - on the graph is outlined. Cards carry plain titles, with the Lean name small beneath. -- The right pane has two modes, Graph and Lean, with a toggle at its top. Click a statement or - a card and the pane changes to Lean at the exact lines: "isoR's CLam case" opens `CLam`'s five - lines, not the top of `isoR`. Any Back returns you to the graph at the same place. -- Choose Lean on the toggle and the Lean moves with the text, level with the sentence you are - reading, with a short line across the gutter between them. Drag the handle to see the graph - as well. -- Citations and figures open under the paragraph that mentions them, so you keep your place. -- Back returns the same pixel of the paper, the same open statement and the same graph, also - after a reload. Every statement and declaration has an address you can send to someone. -- An index at the end of the contents lists every declaration and the axioms Lean reports. +On a desktop, the paper is on the left and the proof diagram is on the right. +As you scroll, the diagram highlights the step linked to the passage you are +reading. Click a statement or diagram card to see its Lean code. Use **Back** +to return to the diagram without losing your place, or the **Graph / Lean** +toggle to choose what stays beside the paper. + +Citations and figures open beneath the paragraph that mentions them. Each +linked statement has its own address, so you can send someone directly to it. +The contents also include an index of named Lean definitions and theorems +(called **declarations**), with the assumptions each proof uses (**axioms**). The site adds no explanation of the mathematics. A program compares the reading copy with the PDF word for word, and the PDF is one click away. The graph and the axiom lists are built from @@ -32,37 +30,6 @@ Lean's own output. The only added words are a short plain title for each declara notes where the paper and the Lean differ, each linked to the sentence it is about. These links, notes and titles were made with AI and have not been reviewed by the authors. -## Add a paper - -A paper is a folder. Everything else is generated from it. - -``` -papers// - paper.pdf the authors' PDF, unchanged - paper.md the paper's text, compared with the PDF word for word - paper.toml title, authors, licences and the Lean modules to read - lean/ the authors' Lean project, unchanged - links.json which passage goes with which declaration, and each one's plain title - generated/ what Lean reports about the project -``` - -The [add-paper skill](skills/add-paper/SKILL.md) walks an agent or a person through -it. In short: - -```sh -python3 tools/paper.py new my-paper # then add the PDF, Lean and paper.toml -python3 tools/paper.py extract my-paper # build the Lean and list its declarations -python3 tools/transcribe.py my-paper # draft paper.md from the PDF's structure -python3 tools/paper.py check my-paper # every word, quote and name must hold -python3 tools/paper.py build # write the data the site reads -``` - -`extract` needs [elan](https://github.com/leanprover/elan) and runs the authors' Lean -on the toolchain they pinned. `check` and `build` need Python 3.11 and Poppler, and, for -a paper with a `paper.md`, Node with `npm install` run in `web/`. `transcribe.py` also -needs `pypdf`. The authors' code runs on your machine, so read a project you do not -trust before extracting it. - ## Run the site Use Python 3.11 or later, Node 20.19 or later, and [Poppler](https://poppler.freedesktop.org/) @@ -85,11 +52,14 @@ the data the site needs; it uses the checked-in Lean extraction, so running the paper does not require Lean. After changing a paper's files, run `python3 tools/paper.py build` again from the repository root. -From `web/`, `npm run build` writes a static site to `web/dist`; set `VITE_BASE_PATH` -to the folder it will be served from. `npm run preview` serves that built site locally. +From `web/`, `npm run build` writes a static site to `web/dist`. +`npm run preview` serves that build locally. If you set `VITE_BASE_PATH` for +the build, use the same setting for the preview. For example, a build made with +`VITE_BASE_PATH=/proof-reader/ npm run build` needs +`VITE_BASE_PATH=/proof-reader/ npm run preview`. -To walk a reader's whole visit in a real browser, build for the public path and run the -journey. It needs Playwright for Python, and takes `--browser firefox` or `webkit` as well: +To test the reading controls in a real browser, build the site and run the +browser test script. It needs Playwright for Python, and takes `--browser firefox` or `webkit` as well: ```sh cd web && VITE_BASE_PATH=/proof-reader/ npm run build && cd .. @@ -100,6 +70,39 @@ python3 tests/journey.py --shots /tmp/journey `tools/capture_images.py` retakes the social card and the picture above from a running site. +## Add a paper + +To add a paper, create a folder containing the original PDF and Lean project, +a reading copy of the text, and links between passages and Lean statements. +The build command turns those files into pages for the website. + +``` +papers// + paper.pdf the authors' PDF, unchanged + paper.md the paper's text, compared with the PDF word for word + paper.toml title, authors, licences and the Lean modules to read + lean/ the authors' Lean project, unchanged + links.json which passage goes with which declaration, and each one's plain title + generated/ what Lean reports about the project +``` + +The [add-paper guide](skills/add-paper/SKILL.md) gives the full procedure for a +person or an AI assistant. The commands are: + +```sh +python3 tools/paper.py new my-paper # then add the PDF, Lean and paper.toml +python3 tools/paper.py extract my-paper # build the Lean and list its declarations +python3 tools/transcribe.py my-paper # draft paper.md from the PDF's structure +python3 tools/paper.py check my-paper # compare the text and check the links +python3 tools/paper.py build # write the data the site reads +``` + +`extract` needs [elan](https://github.com/leanprover/elan), the Lean installer, +and uses the Lean version specified by the paper's authors. `check` and `build` need Python 3.11 and Poppler, and, for +a paper with a `paper.md`, Node with `npm install` run in `web/`. `transcribe.py` also +needs `pypdf`. The authors' code runs on your machine, so read a project you do not +trust before extracting it. + ## What `paper.py check` establishes The command compares every word of the reading copy with the PDF, and one changed word stops @@ -119,8 +122,8 @@ has reviewed them. ## Repository map Authored paper files and the checked-in Lean extraction live under `papers/`. -`tools/paper.py build` turns them into `web/public/papers/`; Vite then packages those -files with the website in `web/dist/`. Both output directories are ignored by Git: +`tools/paper.py build` turns them into `web/public/papers/`. The website build +command then packages them with the application in `web/dist/`. Both output directories are ignored by Git: change their sources and rebuild them. | Source | What it holds | @@ -134,17 +137,17 @@ change their sources and rebuild them. | [extract.lean.template](tools/extract.lean.template) | The Lean program that lists a project's declarations | | [web/](web/) | The website | | [web/src/map/](web/src/map/) | The map, copied from [lean-exposition](https://github.com/wcook04/lean-exposition) | -| [history.ts](web/src/app/history.ts) | What one history entry remembers | -| [web/src/lean/](web/src/lean/) | Shared Lean code rendering and tokens | -| [web/src/proof/](web/src/proof/) | The right page: graph, Lean, handle | -| [check-source.mjs](web/tools/check-source.mjs) | Reject source files with no entry point; run with `npm run check:source` in `web/` | +| [history.ts](web/src/app/history.ts) | Saved reading position and open statements for the Back button | +| [web/src/lean/](web/src/lean/) | Code for displaying and colouring Lean source | +| [web/src/proof/](web/src/proof/) | The proof diagram and Lean panel beside the paper | +| [check-source.mjs](web/tools/check-source.mjs) | Find source files that the application and tools do not use; run with `npm run check:source` in `web/` | | [tests/](tests/) | Python unit tests and the browser [journey](tests/journey.py) | | [Pages workflow](.github/workflows/pages.yml) | Check every paper, build the site and publish to GitHub Pages | ## Related work and videos -[Lean Exposition](https://github.com/wcook04/lean-exposition) provides a tool and writing -methods for preparing three explanations of a Lean result. Its +[Lean Exposition](https://github.com/wcook04/lean-exposition) contains writing guides and tools for explaining a Lean proof in three papers +with different levels of detail. Its [reading website](https://wcook04.github.io/lean-exposition-site/) presents those draft explanations beside the graph; [this video walks through that site](https://www.youtube.com/watch?v=sYMDcT7vyng). Proof Reader's reading copy keeps the original paper's wording. @@ -155,4 +158,4 @@ Code is Apache-2.0; see [LICENSE](LICENSE) and [NOTICE](NOTICE). Each paper and project keeps its own licence and credit, named in its `paper.toml` and on its page. Proof Reader is one of Will Cook's sites. Find the other websites and code on -[my home page](https://wcook04.github.io/), and the [project videos](https://wcook04.github.io/#videos). +[Will's home page](https://wcook04.github.io/), and the [project videos](https://wcook04.github.io/#videos). From d5f903ca698df1eed31fad00f578c6a54854de1d Mon Sep 17 00:00:00 2001 From: Will Cook <46428721+wcook04@users.noreply.github.com> Date: Sat, 31 Oct 2026 23:05:55 +0000 Subject: [PATCH 6/6] Link the central project page from the README opening --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 52b14d2..23576dc 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,7 @@ # Proof Reader +[Will Cook’s home page: all projects and videos](https://wcook04.github.io/) + Proof Reader displays a research paper beside its proof in [Lean](https://lean-lang.org), a language for writing mathematical statements and proofs that a computer can check. Click a linked statement in the paper to