wcook04 · Oct 31, 2026 · Oct 31, 2026 · Oct 31, 2026 · Oct 31, 2026 · Oct 31, 2026
diff --git 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
@@ -38,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/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
@@ -20,7 +20,15 @@ Data flows one way: `papers/<slug>/` 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.
+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`.
+
 Look at any visual change in a browser at laptop and monitor widths.
diff --git a/README.md b/README.md
@@ -1,37 +1,82 @@
 # 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.
+[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
+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)
 
-- 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.
+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.
+
+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
 Lean's own output. The only added words are a short plain title for each declaration, and short
 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.
 
+## 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 run dev
+```
+
+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`.
+`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 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 ..
+python3 tests/journey.py --shots /tmp/journey
+```
+
+`tests/speed.py` measures a paper's first screen on a home connection.
+
+`tools/capture_images.py` retakes the social card and the picture above from a running site.
+
 ## Add a paper
 
-A paper is a folder. Everything else is generated from it.
+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/<slug>/
@@ -43,46 +88,23 @@ papers/<slug>/
   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:
+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     # every word, quote and name must hold
+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) and runs the authors' Lean
-on the toolchain they pinned. `check` and `build` need Python 3.11 and Poppler, and, for
+`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.
 
-## Run the site
-
-```sh
-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.
-
-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
-```
-
-`tests/speed.py` measures a paper's first screen on a home connection.
-
-`tools/capture_images.py` retakes the social card and the picture above from a running site.
-
 ## What `paper.py check` establishes
 
 The command compares every word of the reading copy with the PDF, and one changed word stops
@@ -101,25 +123,41 @@ 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/`. 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 |
 | --- | --- |
-| `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) | 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) 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.
 
 ## 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
+[Will's home page](https://wcook04.github.io/), and the [project videos](https://wcook04.github.io/#videos).
diff --git 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/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/" }
   ]
 }
diff --git 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";