Build static inspection pages

Write plain HTML, Markdown and JSON pages of chosen references, releases and pending reviews from a store.

lema site build reads a store and writes a directory of pages that you can read locally or serve yourself. It is not a hosted service: hosting, search and login are not built (Project status).

Before you start

• A store with at least one project reference or release. In the commands, $STORE is the store directory and $SOCK the server’s socket.
• The server stopped. lema site build opens the store directly, so with the server running it fails with the store at DIR is in use.

1. Build the pages

lema site build --store $STORE --out site --ref main --llms

A site selects at least one reference, release or review. The command prints a JSON summary: the output directory, the file and byte counts, and what it selected. A site over a limit is refused, never cut short.

2. Check what it wrote

Each page is X.html, with X.md and X.json beside it:

site.json lists every file with its SHA-256. With --llms, llms.txt indexes the references’ exports with their statements and links to the Markdown pages.

Each declaration page keeps three kinds of evidence apart: proof acceptance (the receipt from the pinned Lean 4.34.1 kernel, with its axiom footprint), specification review (review records), and execution and IR evidence (guarantee records and releases). Labels say checked, tested, assumed or reviewed. There is no single badge. The pages show what the store recorded, and building them is not a kernel check.

3. Serve the directory

The pages are plain HTML with an inline style and a content security policy of default-src 'none': no script, no forms, nothing loaded from elsewhere. Links are relative, so the directory works from any path. Serve the .txt, .md and .lema files as text.

The directory holds only the selection’s closure. No other reference, release, bundle or alias is listed, and knowing an object’s ID gives no page for it. Who may read the directory is up to you.

To rebuild, run the same command again. The same store state and selection give the same bytes, in any flag order. --out must be new, empty, or a site this command wrote (one that holds site.json). Any other directory is refused with is not empty and holds no site.json. Files that the previous site’s site.json does not list are left in place.

4. Review from an approval view

Name the pending move when you build:

lema site build --store $STORE --out site --ref main --review main=revision:$REV

The page under approval/main/ shows what a review of that move would bind: the move from the reference’s revision to $REV, the active policy and its version, the closure digest, and each declaration the review binds. Each declaration is shown with its view, its name map, the arguments its text leaves to Lean, and the whole declaration with nothing hidden. The declarations are the move’s exports that the policy’s protect gates cover, so under a policy without gates the page shows none and offers no display digest.

When every view gives back its declaration’s identity, the page prints the review command with its display digest. Start the server and run it as a reviewer that the active policy lists:

lema --socket $SOCK review --ref main --revision $REV --decision approve \
  --display $DIGEST --actor steward --token-file steward.token

The review then binds what the page displayed, including the renderer version. If the reference moved or another policy was adopted after you built the page, the digest is refused (is not what its subject displays now): rebuild the page and read it again. A view that does not round-trip, or a declaration the syntax cannot show, offers only a rejection.