← Command reference · lean-pkg claims · CLI overview
lean-pkg claims ledger
per-claim closure from the recorded evidence: verified only with zero diagnostics; read-only; exit 0 only when the package is ready.
Usage
lean-pkg claims ledger [--stage {gate,promote}] [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 |
|
--stage {gate,promote} |
the authority required: gate (lower tier) or promote (also the comparator tier for every reusable theorem and lemma; the default). Choices: gate, promote. |
Details
| Form | What it does | Key flags |
|---|---|---|
claims ledger NAME |
read-only, nothing stored: each claim (the claims file at the gate-bound commit, else the cache, else the file committed at HEAD) with named diagnostics from the recorded receipts, re-checked with gate’s and promote’s validators; a claim is verified only with zero diagnostics, else out-of-scope, blocked, unknown or open; the package is ready, open, failed or unknown (fails closed: no claims or no reusable claim is unknown); --stage promote (default) also requires the comparator tier for reusable theorems and lemmas, --stage gate only the lower tier; exit 0 only when ready; --json adds ledger_digest; codes and rules in Lifecycle. Manuscript findings (manuscript_findings, statement_basis: corrected; schema) are listed per claim with one summary line and --json manuscript_findings, and change no status; a lean_evidence declaration missing at the gate-bound commit is finding-evidence-missing |
[--stage gate\|promote] [--json] |
Exit codes
Exit 1 is also a negative answer here:
claims ledger NAME: the ledger is not ready
JSON output
Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):
claims-ledger(exit 0):bound_commit,claims,claims_source,comparator_sha256,counts,ledger_digest,manuscript_findings,name,ok,package_status,reasons,receipt_sha256,required,schema,stage