← Command reference · CLI overview

lean-pkg page

render the README verification section from coverage.yaml, claims, the ledger and the receipts; stdout unless –write/–check/–out/–site/–html.

Usage

lean-pkg page [--write] [--check] [--out PATH] [--site DIR] [--html PATH] [--repo DIR]
              [--allow-private-manuscript] [--agent AGENT] [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag	Description
NAME
--write	replace the marked block in the package README.md (append it when absent); prose outside the markers is untouched. For a gated package whose record says nothing about the docs-only exception, it then turns it on (update NAME --accept-docs-descendants, its own registry write), so committing the README keeps the receipts bound
--check	exit 1 when the README block is missing or stale, the lean-pkg credit is missing, or the Easley sentence has no backing Slurm receipt; with –site/–html also when those files are missing or stale; writes nothing
--out PATH	write the block here instead; README untouched
--site DIR	also write DIR/verification.md (the full page) and DIR/coverage.md (every row, its claims, inputs and notes) for MkDocs; with –check, compare them instead
--html PATH	also write one static HTML file (no script, no external asset) from the same data; with –check, compare it instead
--repo DIR	read the checkout DIR instead of the registered local_path, for this call only (never saved; for CI): DIR must be a git work tree, and when it has remotes one must be the package’s repo; not with –write
--allow-private-manuscript	render against manuscript.version ‘unposted’; the page then says so
--agent AGENT	with –write: the lease holder, when the package is leased

Details

Form	What it does	Key flags
page NAME	render the README verification section (status capsule, paper-to-Lean map, Not formalized, trust boundary, reproduce, evidence, citation, license, acknowledgments) between <!-- lean-pkg:page:begin --> and <!-- lean-pkg:page:end --> from coverage.yaml, claims.yaml, the claims ledger (a row is verified only when the ledger closes it) and the receipts committed under .lean-receipts/ (allow-listed fields only); deterministic; the public-safety scanner runs over the block and a blocking hit refuses; stdout by default; --write replaces only the marked block in the package README.md (appends it when absent), never commits and never writes the registry; --check exits 1 when the block is missing or stale, the lean-pkg credit is missing, or the README mentions the Easley Cluster without a backing Slurm receipt; toolchain advisory lines (- Toolchain advisory: ..., one per entry of lean-pkg’s toolchain advisories list naming the gate receipt’s toolchain) are left out of that comparison, so a new advisory never makes a page stale: --check prints a non-failing NOTE: toolchain advisory ID applies; the next page --write will show it instead, and --json lists toolchain_advisories[]; --out PATH writes the block elsewhere; --site DIR also writes DIR/verification.md (the full page) and DIR/coverage.md (every row with its claims, declarations, ledger statuses, inputs and notes) for MkDocs, and --html PATH one static HTML file of both (no script, no external asset); with --check those files are compared instead (missing or stale: exit 1); user text is escaped in every output; --repo DIR reads that checkout instead of local_path for this call (CI; not with --write); --json gains site_files[] {path, status} and repo_override (The verification page)	[--write \| --check \| --out PATH] [--site DIR] [--html PATH] [--repo DIR] [--allow-private-manuscript] [--agent A]

Exit codes

0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.

JSON output

Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):

• page (exit 0): counts, current, easley, kind, ledger_digest, ledger_status, manuscript, markdown, name, ok, private_manuscript, problems, readme, receipts, repo_override, rows, site_files, sites, toolchain_advisories, unchanged, verified_rows, warnings, written

Examples

Print the README verification section rendered from coverage.yaml, the claims, the ledger and the receipts.

lean-pkg page my-proof

Replace the marked block in the package README.md (append it when absent).

lean-pkg page my-proof --write

Exit 1 when the README block is missing or stale; a CI step for the package.

lean-pkg page my-proof --check

Also write the docs pages and one self-contained HTML file.

lean-pkg page my-proof --site docs --html docs/verification.html