← Command reference · lean-pkg receipt · CLI overview
lean-pkg receipt check
validate a published package’s receipts from git alone: no registry, no network, never runs Lean (an outside referee’s check; exit 0 only when every check passes).
Also spelled: lean-pkg verify-receipts (all aliases).
Usage
lean-pkg receipt check --repo DIR --commit SHA [--at REF] [--docs-descendants]
[--name NAME] [common flags]
[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.
Arguments and flags
| Argument or flag | Description |
|---|---|
--repo DIR |
a local clone of the package (the package directory; cloned privately, never modified). Required. |
--commit SHA |
the commit the receipts bind (the page’s git checkout <commit> line). Required. |
--at REF |
the published ref whose .lean-receipts/, coverage.yaml and README.md are read (default HEAD of –repo); it must be the commit or an evidence-only descendant of it |
--docs-descendants |
also accept a docs-only descendant (no build input changed); the author’s opt-in lives in a registry the referee cannot read, so this is the referee’s choice, printed in the result |
--name NAME |
the package name the claims must carry (default: package in coverage.yaml, else claims.yaml, else the directory name) |
Details
| Form | What it does | Key flags |
|---|---|---|
receipt check |
an outside referee’s check of a published package: reads no registry, opens no network connection and never runs Lean. Clones --repo privately (local transport only; its working tree is never read or changed), checks out the published ref (--at, default HEAD) and runs gate’s and comparator’s own validators on the receipts under .lean-receipts/ that bind --commit (a JSON file named for the commit that is not a receipt fails, unless its schema is one of the comparator runner’s own records, such as comparator-stages/1, which is skipped and listed): the binding (evidence-only descendants, with gate’s exemption for a formalization.yaml at the package root that differs only in derived keys, printed when applied; docs-only ones too with --docs-descendants, the referee’s choice, printed with the result), the toolchain and Mathlib pins at the commit, every SHA-256 (configurations, logs, the redacted verify log, manifest_sha256 and the other additive evidence keys, the olean manifest record), the claims at the commit, the comparator configurations naming every reusable theorem claim, coverage.yaml (R11) and the README page block against the receipts. One line per check, PASS, FAIL or SKIP (not applicable, with the reason); --json lists them all. A toolchain on lean-pkg’s toolchain advisories list adds one WARN: toolchain advisory ... line per entry after the verdict, never a failure (JSON toolchain_advisories[]; toolchain advisories). Exit 0 only when no check fails, 1 otherwise, 2 on a usage error. Re-running Lean is the comparator step of docs/trust-model.md, “Re-verify a page yourself”. The 1.0 command tree’s read-only verb on the receipt noun; the spelling verify-receipts is reserved for its alias table |
--repo DIR --commit SHA --at REF --docs-descendants --json |
Examples
In a fresh clone of a published package, check its receipts for the page’s bound commit from git alone; no registry, no network, no Lean run.
lean-pkg receipt check --repo . --commit 0123456789abcdef0123456789abcdef01234567
Sample output:
receipt check: PASS my-proof at 0123456789ab (tier comparator; 13 passed, 1 skipped)
commit 0123456789abcdef0123456789abcdef01234567 (published ref 89abcdef0123)
rule: evidence-only descendants (docs-only not accepted; --docs-descendants to accept them)
...
PASS binding: evidence-only descendant of 0123456789ab (+3 evidence file(s))
...
receipt check: PASS my-proof at 0123456789ab (tier comparator; 13 passed, 1 skipped)
The same at a release tag, also accepting a README or notes committed after the evidence (the docs-only rule, the referee’s choice); every check with its verdict as JSON.
lean-pkg receipt check --repo . --commit 0123456789abcdef0123456789abcdef01234567 --at v1.0.0 --docs-descendants --json