Command reference

Every lean-pkg command and subcommand, with its usage line, every flag, its exit codes, its --json keys and, for the commands people run most, examples. Flags shared by every command (--registry, --json, --commit, --push, committed mode, --registry-snapshot) are on the CLI overview. Older spellings (claim, init, audit, …) keep working; see Command aliases.

New here? The quickstart takes a new package from new to a verified page with five verbs: new → verify (both receipts and the gate) → status → page → publish (--yes to go public). verify runs, in order, receipt comparator, receipt systemd and gate; a cluster uses receipt slurm instead. A shared registry adds lease claim before work. At any point next NAME prints the one command to run now. The sample workflow walks the same path on a real package.

START HERE: one package on your own machine

Command	Purpose
`lean-pkg new`	scaffold a new Lean package (Challenge/Solution, comparator.json, claims, coverage, verify.sh) in a new directory and git init it; no registry, no network
`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
`lean-pkg status`	full record + last 5 history entries + scope (gated commit, privacy, the exact comparator-covered declarations)
`lean-pkg page`	render the README verification section from coverage.yaml, claims, the ledger and the receipts; stdout unless –write/–check/–out/–site/–html
`lean-pkg publish`	the checklist from verified-private to listed, with the exact next commands (read-only); –yes makes the repository public (`promote` is the same)
`lean-pkg doctor`	installation, registry, index and tool diagnostics; exit 1 when the registry is unreadable or its schema version is unsupported
`lean-pkg help`	help topics (exit-codes, environment, formatting) or a command’s –help

PACKAGE AUTHOR: evidence, publication, the catalog

Command	Purpose
`lean-pkg register`	the ONLY write path for new packages: validated, deduping, auto-detecting
`lean-pkg update`	set fields of an already-registered package (register is for NEW ones)
`lean-pkg record`	record a publication evidence event (consent, Palomar, DOI, Reservoir, Mathlib PR)
`lean-pkg gate`	validate a lower-tier receipt; gate-pending -> verified-private; records the receipt’s lean_toolchain and mathlib_rev as the package’s pins
`lean-pkg next`	read-only: the single recommended next command for a package, with a one-line reason (exit 0 a command to run, 1 blocked)
`lean-pkg list`	static table, pipe-friendly
`lean-pkg search`	prior-art search over claims, the index and public sources
`lean-pkg receipt`	produce receipts (slurm, systemd: the lower tier; comparator: the comparator run; each writes files in the package checkout, never the registry); check a published package’s receipts from git alone (check)
`lean-pkg receipt slurm`	a lower-tier receipt from a finished Slurm job, its verify log and its stdout seal (–template: an sbatch wrapper that meets it; –check: preflight the job’s files)
`lean-pkg receipt systemd`	a lower-tier receipt from a finished systemd –user service unit (run bounded with –run, or its saved properties), its verify log and its stdout seal
`lean-pkg receipt comparator`	run the comparator on a Lake project and write the comparator receipt (the `comparator-receipt` program: the same code and flags)
`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)
`lean-pkg comparator`	comparator receipts: attach one to a gated package, or check it; config (write a configuration from claims), coverage, migrate-signoff; host-check
`lean-pkg comparator attach`	attach a comparator receipt to a gated package; no status change (`comparator NAME --receipt R` is the same)
`lean-pkg comparator check`	validate a comparator receipt against the package; read-only, records nothing, works at any status (`comparator NAME --receipt R --check` is the same)
`lean-pkg comparator config`	write a comparator configuration from claims (–from-claims); coverage and migrate-signoff are verbs of their own
`lean-pkg comparator coverage`	read-only: the claims covered by the comparator configuration tracked at the gate-bound commit, and why a changed one needs a new gate (`comparator config --coverage NAME` is the same)
`lean-pkg comparator migrate-signoff`	move the deprecated inline judged_as / lean_pkg_scaffold keys of a configuration into lean-pkg-signoff.json; dry run unless –write (`comparator config --migrate-signoff PATH` is the same)
`lean-pkg comparator host-check`	can this host run the comparator; read-only
`lean-pkg claims`	claims.yaml: sync \| list \| check \| migrate \| ledger \| mark \| rebase (named reusable results)
`lean-pkg claims sync`	read claims.yaml at HEAD of the checkout; validate (TODO placeholders refused); cache; event
`lean-pkg claims list`	table of cached claims with status and trust
`lean-pkg claims check`	re-validate cached claims; exit 0/1 (–file: a working-copy file)
`lean-pkg claims migrate`	legacy claims.json -> a claims/1 skeleton in the checkout (never the registry)
`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
`lean-pkg claims mark`	set the status of the claims a comparator config’s theorem_names cover (exact full-name match); read-only unless –write; never commits
`lean-pkg claims rebase`	move claims.yaml and coverage.yaml to a new manuscript version: carry unchanged statements re-keyed from the new .aux, list the rest for review; writes only –out-dir; never changes a status
`lean-pkg coverage`	coverage.yaml (coverage/1): the paper-to-Lean map (or a library’s main results) `page` renders
`lean-pkg coverage check`	validate coverage.yaml against claims.yaml and the receipts at HEAD; exit 0/1; read-only
`lean-pkg formalization`	formalization.yaml (v0.4, what Palomar reads): render it from the registry and the repo at HEAD; anchor the companion to one arXiv version
`lean-pkg formalization render`	render formalization.yaml (v0.4, what Palomar reads) from the registry and the repo at HEAD; stdout unless –write/–out (`formalization NAME` is the same)
`lean-pkg formalization anchor`	bind the companion to one posted arXiv version (writes package files, never the registry)
`lean-pkg formalization kept`	the canonical kept view of formalization.yaml (derived keys removed) and its SHA-256, for a release-input audit; –against REV: exit 1 when a kept key changed (read-only)
`lean-pkg palomar`	Palomar: prepare (build a submission bundle), check (read-only readiness), port-modules (plan or write the module-system port); no network
`lean-pkg palomar prepare`	build the submission bundle (formalization.yaml, comparator configs, receipts, README.txt, MANIFEST.sha256); event palomar-prepared
`lean-pkg palomar check`	read-only, offline: every gap to Palomar’s mechanical rules at one commit (module headers, toolchain floor, comparator configs, formalization.yaml, licence, repository); exit 0 ready / 1 gaps
`lean-pkg palomar port-modules`	plan (dry run, default) or –write the mechanical port of the package’s tracked .lean files to Lean’s module system; never commits
`lean-pkg reservoir`	Reservoir: check (read-only listing criteria)
`lean-pkg reservoir check`	would Reservoir list this package? read-only; exit 0 eligible / 1 not
`lean-pkg blueprint`	blueprint: check (\lean{} names with checkdecls)
`lean-pkg blueprint check`	run checkdecls on the blueprint’s declaration list at HEAD and check claims.yaml against it; exit 0 nothing missing / 1; writes nothing
`lean-pkg public-safety`	read-only: scan the package’s tree and git history for private patterns (exit 1 on hits; publish –yes runs it)
`lean-pkg report`	read-only: a redacted bug report in the repository’s issue format; dry run unless –yes (files it with gh issue create)

COORDINATION AND MAINTENANCE: shared registries, leases, the registry file

Command	Purpose
`lean-pkg lease`	leases for agents sharing a registry: claim, renew, release, list (the old spellings claim, renew, release, leases keep working)
`lean-pkg lease claim`	CAS lease on a package (24h default TTL)
`lean-pkg lease release`	release a lease (holder-only unless –force); exporting or adopting a repository is `repo export` / `repo adopt`
`lean-pkg lease renew`	restart your own live lease from now (holder-only; refuses once it has lapsed: claim again)
`lean-pkg lease list`	held leases, soonest expiry first; read-only
`lean-pkg registry`	the registry file itself: init, migrate, validate, audit, board, wiki (the old top-level spellings keep working)
`lean-pkg registry board`	curses TUI on a tty; static table otherwise
`lean-pkg registry init`	bootstrap an empty registry and its event log
`lean-pkg registry migrate`	upgrade the registry schema in place (additive; idempotent)
`lean-pkg registry audit`	report expired leases, gh visibility, drift; read-only without –write
`lean-pkg registry validate`	schema + enum + history sanity; exit 0/1
`lean-pkg registry wiki`	render a Markdown status page
`lean-pkg repo`	the package’s checkout: move (relocate the record), export (a new single-commit public repository), adopt (an existing one)
`lean-pkg repo move`	relocate: point the record at another checkout, keeping name, history and claims (the same as `update NAME --path PATH`)
`lean-pkg repo export`	export the gate-bound commit’s tree (or –from-tree SRCDIR) as a NEW single-commit repository at DIR, then move the package there (`release NAME --fresh-repo DIR` is the same)
`lean-pkg repo adopt`	adopt the existing repository at DIR as the public history, then move the package there (`release NAME --adopt-repo DIR` is the same)
`lean-pkg index`	the public catalog: add \| check \| render \| migrate
`lean-pkg index add`	write <index>/<name>/entry.yaml from a clone at the pin
`lean-pkg index check`	static check, or re-derive entries from bytes at the pin; exit 0/1/2
`lean-pkg index render`	write the Markdown table (default <index>/README.md)
`lean-pkg index migrate`	rewrite index-entry/1 entries as index-entry/2 (claims derived)
`lean-pkg llms`	print the agent-oriented usage contract

Other programs

Command	Purpose
`lean-exercise`	Judge a Lean exercise Solution against its Challenge with `lake comparator`.
`lean-pkg-extract`	Plan a standalone public Lean-verification repository from a mixed working repository, with exact provenance. Read-only; no registry, no network.
`comparator-receipt`	the program spelling of `lean-pkg receipt comparator`

Other spellings of these commands are listed on Command aliases.

Regenerating these pages

Every page here is generated by scripts/command_docs.py (make docs) from the argparse parsers (the tiers included), lean-pkg help exit-codes, the golden --json key sets and the curated sources in docs/_commands/ (examples, the introduction, per-command notes). CI fails when a committed page differs from the generator’s output, and when an example no longer parses.