← Command reference · CLI overview
lean-pkg verify
both receipts and the gate in one step on this machine: the comparator receipt, the lower-tier receipt (systemd user unit) at the same commit, then the gate; prints each command it runs.
Usage
lean-pkg verify [--work-dir DIR] [--unit UNIT] [--script FILE] [--judges N]
[--agent AGENT] [--reason TEXT] [--dry-run] [common flags] NAME
[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.
Run, at the checkout’s HEAD, receipt comparator, receipt systemd --run -- bash verify.sh and gate (an active package first moves to gate-pending; a gated one is re-gated), each as its own lean-pkg invocation with its own checks. Writes only what those commands write; commits nothing in the checkout. A package whose committed coverage.yaml declares an LTS stack (stack: NAME, docs/stacks/) is checked against it (lean-toolchain, the Mathlib commit, the comparator receipt’s tool digests): a warning per difference, never a refusal.
Arguments and flags
| Argument or flag | Description |
|---|---|
NAME |
|
--work-dir DIR |
where the run’s log and unit output go, outside the checkout (default $XDG_STATE_HOME/lean-pkg/verify/NAME/<commit>-<UTC stamp>, else ~/.local/state/…) |
--unit UNIT |
the systemd user unit (default NAME-verify) |
--script FILE |
the committed lower-tier check, run as bash FILE LOG (default verify.sh) |
--judges N |
comparator judge processes (receipt comparator --judges N) |
--agent AGENT |
the agent acting: passed to the status move and the gate |
--reason TEXT |
re-gate only: accept a commit that does not descend from the gated one (gate --regate --reason) |
--dry-run |
print the steps and their commands; run nothing |
Exit codes
0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.
Examples
Print the three steps (the comparator receipt, the lower-tier receipt at the same commit, the gate) and their exact commands; nothing runs.
lean-pkg verify my-proof --dry-run
Run them in that order at the checkout’s HEAD; an active package first moves to gate-pending, a gated one is re-gated. Commit the receipts afterwards.
lean-pkg verify my-proof
Sample output:
verify: 1/3 comparator receipt: lean-pkg receipt comparator --project .../my-proof
...
verify my-proof: verified-private at a0a4fe68e46c: lower-tier .lean-receipts/a0a4fe68e46c-systemd-user-my-proof-verify.service-<id>-h-<label>.json, comparator .lean-receipts/a0a4fe68e46c-comparator.json
next:
git -C .../my-proof add .lean-receipts && git -C .../my-proof commit -m "evidence: receipts at a0a4fe68e46c"
lean-pkg page my-proof --write