# lean-pkg — llms.txt > Registry and trust gate for Lean 4 formalization packages. Install: `pipx install git+https://github.com/lean-pkg/lean-pkg.git`. > Human docs: https://lean-pkg.github.io/lean-pkg/ (source: docs/), README.md, DESIGN.md. Tests: `python3 -m pip install -e '.[test]' && python3 -m pytest -q`. > The block below is the exact output of `lean-pkg llms` (written by `make docs`; tests/test_docs.py checks it byte for byte). lean-pkg llms.txt — agent contract for the Lean 4 package registry PURPOSE A registry YAML file is the source of truth for a set of Lean 4 formalization repos. lean-pkg is the ONLY write path; GitHub is just the visibility mirror. history[] and the event log (lean-package-events.jsonl next to the registry) are append-only. Registry resolution: --registry PATH, else env LEAN_PKG_REGISTRY, else ~/.lean-pkg/registry (dir with lean-packages.yaml, or the file; base env LEAN_PKG_HOME), else ./lean-packages.yaml. STANDING RULES - NEVER hand-edit the registry yaml. Use `lean-pkg register` / `lean-pkg update`. - Command names are the 1.0 tree (`lean-pkg help aliases`): old spellings (claim, release, leases, init, audit, board, promote, comparator NAME --receipt R, release --fresh-repo, comparator-receipt, ...) are permanent aliases with the same output and exit codes; text mode notes the new spelling on stderr (LEAN_PKG_NO_ALIAS_NOTE=1 silences). - One package on one machine: `lean-pkg verify NAME` runs the comparator receipt, the lower-tier receipt (systemd user unit) at the same commit and the gate, in that order, each as its own invocation; commit .lean-receipts/ afterwards; `page NAME --write`; `publish NAME` (read-only checklist), `publish NAME --yes` (public; ONE-WAY). - Before starting Lean work on a package: `lean-pkg registry board --json` (or `list --json`; one package: `status NAME --json [--fields ...]` or `list --json --only NAME`). Writing a paper alongside: check selected intermediate results as they stabilise (docs/paper-companion.md); never assume the target theorem to gain coverage; a certificate covers its exact formal statements, not the whole paper. - Claim before working (`lease claim`): one package = one workspace. Default TTL 24h; `registry audit --write` sweeps expired leases. Work longer than the TTL: `lease renew` before it lapses (`lease list --agent A --expiring 2`). gate, comparator attach, record, publish --yes, claims sync, search --record, verify: pass --agent A (another agent's live lease refuses; A is the event's `actor`); without it a live lease only warns. - Mutating ops are dry-run by default unless a flag says otherwise: publish --yes, registry audit --write. - Fully non-interactive: pass flags, never wait for a prompt. Use --json for machine parsing. - Shared registry in git: --commit (env LEAN_PKG_COMMIT=1) pulls --ff-only, writes, commits the yaml + event log together; --push (LEAN_PKG_PUSH=1) also pushes (a transient transport error such as a connection reset, timeout or HTTP 5xx is retried with backoff: LEAN_PKG_PUSH_RETRIES, default 4, delays LEAN_PKG_PUSH_RETRY_DELAY doubling from 5 s; rejected as non-fast-forward: fetch + `rebase --autostash` of that one commit + push again, an event-log-only conflict merges as a union in timestamp order, any other conflict aborts the rebase with the clone as before, `; rebase conflict in FILES` in the error; a rebased registry with a schema error neither side had is not pushed (reset to the local commit, `; rebased registry fails validation (...)`); a failed push: `push failed: origin/BRANCH: ERR`, commit kept, exit 1, recovery printed (after a rejection: git pull --rebase origin BRANCH, then git push origin BRANCH); a write whose event log cannot be appended to (read-only, a directory) refuses before the registry is replaced, nothing written; a --push write refuses while the clone is ahead of origin/BRANCH); --no-commit overrides; a committed-mode write refuses over modified registry files, naming the uncommitted event (event, package, agent, time), the package's lease holder and the git commit that clears it; a write without committed mode that leaves the registry files in a git clone modified ends with stderr `NOT COMMITTED: FILES modified in CLONE; every --commit/--push write to this registry refuses until they are committed: ...` (--json + registry_uncommitted [files]). stderr: `committed SHA on BRANCH: MSG` (+ `(committed mode: env VAR=1)` when the env, not a flag, turned it on), `pushed origin/BRANCH (SHA)`; `CMD --help` says `set now` when a variable is set. Every write is covered (index add, formalization --write, claims sync, search --record, board TUI keys); dry runs and read-only commands never fetch (an explicit --commit there: stderr "ignored"). Reports on stderr; a --json payload gains "registry_commit": {sha, pushed, error, push_error, push_attempts, rebased} (also as "commit" unless the payload has its own, e.g. gate's source commit). STATUS ENUM AND TRANSITIONS (evidence required) scratch -> active owner_project named active -> gate-pending lower-tier check submitted (terminal executor job identity in notes); also verified-private -> gate-pending to re-gate a new commit (one step instead: `gate --regate`) gate-pending -> verified-private `gate` accepts a receipt (schema below) public -> public `gate` on an already-public package records evidence; status unchanged verified-private -> public `publish --yes` after a clean `publish --yes --dry-run` checklist; ONE-WAY flip public -> upstreamed `update --status`: a recorded mathlib-pr-merged / palomar-registered event, or a --reason with the URL any -> archived `update --status archived --reason` or `registry audit --write` (gh isArchived); public returns to a private status only this way: public -> verified-private by `update --withdraw-publication --reason` only: the owner made the repository private (gh must not report it public; active when never gated); visibility private + publication_hold {reason, at, by}; promotion history kept; publish --yes refuses while held; gate/regate/registry audit --write keep it; only `update --release-publication-hold --reason` lifts it SUBCOMMANDS (global flags: --registry PATH --events PATH --json --commit --push --no-commit, also after the subcommand; env LEAN_PKG_REGISTRY, LEAN_PKG_HOME, LEAN_PKG_EVENTS (ignored when --registry is given: its sibling log); --version: `lean-pkg X.Y.Z ([+dirty], editable )` or `(installed )`, local only; --json {version, commit, dirty, install, path}; --registry-snapshot COMMIT (env LEAN_PKG_REGISTRY_SNAPSHOT): read-only, the registry + event log as of COMMIT of its git repo (git show into a temp copy); reads work (status/list/registry board/registry audit/dry runs/comparator config --dry-run), every write exits 2 `read-only: --registry-snapshot`; --json +registry_snapshot sha) registry board TUI on a tty, static table otherwise; --only, --fields, --no-claims as for list (any: never the TUI). ex: lean-pkg registry board --json --only my-lean list static table; --only NAME[,NAME] filters packages (full records, shape unchanged); --fields a,b.c trims each record as status --fields (+ `fields` list; text: YAML); --no-claims as status. ex: lean-pkg list --json --only my-lean --fields status status full record + last 5 history entries (a lease adds derived expires_at, UTC; a lapsed lease ends the output with `lease: EXPIRED ...`, one lapsing within 2h with `lease: expires in ...`; --json lease_state {state live|expiring|expired|invalid|none, seconds_left}); --fields a,b.c: only those keys (dotted paths; lease.contact: null when unset; aliases = the table columns: pin, vis, reaudit, expires|lease.expires, lease.claimed; --json keeps nesting, text YAML; unknown: exit 2 listing keys); record keys: status --help, docs/cli.md#package-record. --no-claims: drop [bulk] keys (claims; also list/board; +omitted[]). Without --fields: a `scope:` text block and --json scope {gate {receipt, commit, head, head_is_gated_commit, readable}, publication {status, visibility, publication_hold, github}, product {kind paper|library|null, source, note}, comparator null|{receipt, readable, commit, mechanism, configs[], theorem_names[], definition_names[], claimed_theorems, claimed_theorems_covered, reusable_theorems, reusable_theorems_covered, whole_package false, note}, claims {total, by_status, synced_commit, note}}: the gated source commit, recorded privacy + hold (offline: gh not queried), the product (kind in coverage.yaml at HEAD; paper when absent; not the DOI track), the exact declarations the comparator receipt compared and the claimed theorems/lemmas they cover (never the whole package), claim counts by status (not completion percentages). ex: lean-pkg status my-lean --json --fields status,gate.receipt,lease.agent new scaffold a minimal Lean package in a new directory (refused when it exists and is not empty) and git init it; no registry read or written, nothing committed, fetched or built: lean-toolchain (--stack NAME|current|none: a declared LTS stack's toolchain and Mathlib tag, docs/stacks/, plus `stack: NAME` in coverage.yaml; default current for --kind paper (no stack current: the newest pins, warned), none for --kind library: v4.35.0-rc2; an undeclared stack exits 2 listing the declared ones), .gitignore, lakefile.toml (library MOD = NAME in CamelCase, --module MOD, defaultTargets [MOD] so a bare `lake build` builds it; requires Mathlib unless --no-mathlib), MOD/Challenge.lean (sorry) + MOD/Solution.lean (module-headed, the getting-started template) + MOD/Axioms.lean (#print axioms), comparator.json, claims.yaml (one reusable claim), coverage.yaml (--kind paper, the default: kind paper, manuscript version unposted and FILL-ME markers that coverage check refuses until the author names the paper and `formalization anchor --write` binds the posted version, no manuscript invented; --kind library: one main result, passes coverage check), CITATION.cff (--author, else git user.name; a name with no space warns: it looks like a handle), LICENSE + LICENSES/.txt (--license Apache-2.0|MIT), REUSE.toml (every file, receipts and logs included, under that license: reuse lint passes), README.md (the lean-pkg credit), verify.sh (the log `receipt systemd --run` reads; --no-mathlib: a `mathlib-rev: none` line, which the receipt also derives from a lake-manifest.json with no mathlib package); NAME [a-z][a-z0-9]*(-[a-z0-9]+)*, at most 64 (else exit 2); --json {ok, name, dir, kind, module, mathlib, lean_toolchain, mathlib_rev, stack, stack_source, license_spdx, author, author_source, files[], git_init, committed, registry_touched, coverage_complete, next_commands[], warnings[]}. ex: lean-pkg new my-proof (a paper), lean-pkg new my-lib --kind library; the path to a page: docs/quickstart.md registry init bootstrap an empty registry + event log (event: file name + version; --force: empty only, forced: true). ex: lean-pkg --registry ./lean-packages.yaml init registry migrate upgrade the registry schema in place to v3 (v2 adds license_spdx, formalization_yaml, palomar[], doi, reservoir, consent[]; v3 adds claims_file, claims[], claims_synced_commit; additive, idempotent; a legacy literal ~/x local_path is rewritten $HOME-relative). ex: lean-pkg migrate --dry-run record record a D5 evidence event; validated before writing (a schema error it introduces refuses, rule named, nothing written); --field keys (all required, others refused; commit 40-hex, version integer): consent-recorded: who role pointer (a /home, /Users, ~ path: WARN + private_strings; same who+role+pointer again: already recorded, exit 0) | palomar-preflight-pass: commit run (same commit+run again: already recorded, exit 0) palomar-submitted: commit submission_id comparator_config | palomar-review: commit outcome(neutral|revision_required|rejected) palomar-registered: commit id version(int) comparator_config (status public|upstreamed; config tracked at HEAD) | palomar-withdrawn: id version(int) (of a recorded entry) | mathlib-pr-opened, mathlib-pr-merged: url (https://github.com/...) doi-minted: doi(10.NNNN/x) tag commit [concept] (rule doi-in-palomar: commit already recorded by a palomar-* event; skipped on the DOI-only track, --track doi-only or the record's track: doi-only, status public only, rule doi-only-public; the event carries track) | reservoir-listed: url (the package's https://reservoir.lean-lang.org/@owner/name page; Reservoir API: 404 refuses, unreachable records verified=false; a url naming neither package nor repo warns) retract: event ts + --reason: append-only correction (event evidence-retracted); validate and the upstreamed check ignore the entry ex: lean-pkg record my-lean doi-minted --field doi=10.5281/zenodo.1 --field tag=v1.0.0 --field commit=<40hex> register add a package; dedupes by name AND resolved local_path (~/ expanded, stored $HOME-relative; empty --path/--repo refused); auto-detects toolchain + mathlib pin; a Lean root namespace (lakefile lean_lib, else top-level *.lean) another package's checkout also uses: stderr note + `notes`, never a refusal. --like OTHER: a sibling package; copies repo/owner-project/upstream-target/automation from OTHER (flags win; never visibility), refused when DIR is in another git repo and --repo is absent; notes whether toolchain/Mathlib pin match OTHER's (JSON like {name, copied[], toolchain, mathlib_pin}). warn: DIR inside or containing another package's dir; a lake path dependency outside DIR. flags: --url URL (required; old spelling --repo) --path HOME-RELATIVE (required) [--license-spdx SPDX] [--owner-project N] [--visibility private|public] [--status scratch|active|gate-pending|public (public: --visibility public --reason R)] [--upstream-target none|mathlib|palomar] [--automation TEXT] [--notes TEXT] [--workspace W] [--agent A] [--dry-run] --workspace/--agent are metadata only; they do NOT claim. Claiming is a separate act. ex: lean-pkg register my-lean --url git@github.com:you/my-lean.git --path src/my-lean --license-spdx Apache-2.0 update set fields (--notes over non-empty notes: exit 2, nothing written, unless --replace-notes, which replaces, prints the old value, event notes_replaced + notes_from; --append-note TEXT --agent A appends `YYYY-MM-DD (A): TEXT` and prints only `appended note: ` (--json changes.notes keeps from/to), not with --notes); manual status moves and --force need --reason (else exit 1; a refusal lists the allowed moves); empty --repo/--owner-project refused; --license-spdx takes an SPDX expression (MIT OR Apache-2.0); --paper-arxiv ID / --paper-status unpublished|preprint|published set the optional paper {arxiv, status} (an id alone: preprint). --source-paper-title T --source-paper-author A (repeatable) --source-paper-arxiv ID --source-paper-doi DOI / --ai-tool T --ai-role R (repeatable): optional source_paper {title, authors[], arxiv, doi} / ai_assistance {tools[], roles[]}, rendered as formalization.yaml acknowledgements lines (never project.authors; no consent needed). --namespace-note TEXT [--namespace NS]: namespace_notes {NS: TEXT} (default NS: those shared with another package); audit duplicate-namespace is info once all sharers have one. --track palomar|doi-only --reason R: the optional DOI track (see record doi-minted). --accept-docs-descendants | --no-accept-docs-descendants --reason R: the optional docs_descendants true/false (opt in to the docs-only rule, see gate); --build-inputs GLOB,GLOB --reason R: the optional build_inputs list ('' clears); --headline-config REL: the optional headline_config (the headline comparator configuration formalization renders as status.main_results; '' clears); these three accept --dry-run (event update-dry-run, nothing written). register/update/record: schema errors already in the registry (e.g. another package's) go to stderr as pre-existing, not blocking. ex: lean-pkg update my-lean --status gate-pending --reason "check job 4242 submitted" --withdraw-publication --reason TEXT [--agent A] [--dry-run]: record the owner's privacy withdrawal of a public package (see the transitions; event publication-withdrawn {status_from, status_to, visibility_from, visibility_to, reason, by, github_visibility, promoted_commit, forced}; JSON status/visibility {from, to}, publication_hold, github_visibility, github_check). --release-publication-hold --reason TEXT [--agent A] [--dry-run]: lift it, status/visibility unchanged (event publication-hold-released {reason, hold, by, forced}). Each on its own (other fields: exit 2). | --path NEW --reason TEXT [--agent A] [--redetect] [--dry-run]: relocate (same name, history, claims; event relocated). Same path: no-op, exit 0. Refuses another package's path, a foreign live lease (no --force). Gate/claims not bound to NEW's HEAD are cleared (`cleared`). Output ends with a binding block (receipt commit vs new HEAD, evidence-only verdict, formalization.yaml exception) + `next:` commands (or "nothing to re-gate"); JSON binding{} + next_commands[]. lease claim (old spellings: claim, lease NAME) CAS lease; refuses if another agent holds an unexpired lease (names holder + expiry). Any other command naming a package whose lease has lapsed, or lapses within 2h, prints stderr `WARN: NAME lease: EXPIRED ... | expires in ...` with the claim/renew that keeps it (not claim/renew/release/leases/audit/status). Writes take a file lock on .lock (sibling); safe across processes on one host. flags: --workspace W --agent A (required) [--ttl HOURS: 1..8760, 24 new; a holder's re-claim keeps its TTL; above 8760: exit 2, nothing written] [--reason TEXT] [--contact TEXT: address of the holding session (e.g. lab-desk/n14-paper, @lean-ops), stored as lease.contact; one line, <= 200 chars, else exit 2; a re-claim without it keeps it] [--force (needs --reason)] ex: lean-pkg lease claim my-lean --workspace w3 --agent vera --reason "chapter 2" lease release (old spelling: release) holder-only unless --force --reason (released_by: --agent, else force). ex: lean-pkg lease release my-lean --agent vera | repo export NAME DIR (old spelling: release NAME --fresh-repo DIR) [--remote URL] [--keep-receipts] [--source-commit SHA] [--dry-run] (no lease involved): git archive of the gate-bound commit (package dir; drops .lean-pkg-private-patterns, internal paths, .lean-receipts/ unless --keep-receipts, listed; carries ONLY its allow: lines into a committed .lean-pkg-public-allow, merged with one in the tree, plan line `public allow: N allow line(s) ... carried`, JSON public_allow {file, carried, lines[]}; an allow line a private block pattern matches refuses, naming its line number) -> public-safety scan (blocking hit: refused, nothing written; warnings listed) -> new repo at DIR, ONE commit "fresh-history export of ; receipts and gate must be re-run on this commit" (+ source commit, export date), origin = --remote -> relocated as update --path DIR --reason "fresh-history release" (gate/comparator cleared, verified-private -> gate-pending, dated note keeps old receipt paths + source sha; --remote sets repo); refuses public/upstreamed/archived, a non-empty DIR; --dry-run: plan + next commands (gate, comparator-receipt --prepare, publish), writes nothing | repo export NAME DIR --from-tree SRCDIR (not with --source-commit): exports the WORKING TREE at SRCDIR (hand-cleaned, not a commit; in a checkout `git ls-files --cached --others --exclude-standard`, else every file but .git/ .lake/), same drops + scan (+ the commit message), message "fresh-history export of working tree ; ..." + "source commit: none (hand-cleaned tree)" + "source package commit for provenance: " | repo adopt NAME DIR (old spelling: release NAME --adopt-repo DIR) [--remote URL] [--allow-history] [--dry-run]: adopt an existing repo as the public history, no export, no new commit; refuses >1 commit on all refs (unless --allow-history), DIR not its top dir, the package's own source repo, modified tracked files, an origin other than --remote, blocking public-safety hits in its tree or full history; then the same relocation (reason "adopted-repository release"; note names the adopted commit + previous gate-bound sha) lease renew (old spelling: renew) holder-only restart of a LIVE lease (event claim-refreshed); a lapsed lease is refused: claim again. --ttl HOURS: 1..8760 (above: exit 2, nothing written). --contact TEXT sets/replaces lease.contact, omitted keeps it; --no-contact clears it (event contact_cleared: true when one was removed; with --contact: exit 2). leases [--agent A] [--expiring H]: held leases, soonest first, last column CONTACT (blank when unset; JSON contact|null); doctor warns on leases lapsing within 2h or expired-unswept. Unparseable lease fields: shown INVALID, writes refused; `release NAME --force --reason TEXT` clears. gate validate receipt; gate-pending -> verified-private; --receipt/--comparator PATH: a path that exists as given (cwd-relative or absolute) is used as given; a relative one missing from the cwd but present under the package checkout (or --check --repo DIR) is resolved there with a stderr note, a `· receipt R resolved against the package checkout: P` line and JSON resolved_paths[] {what, arg, path, base} (the same relative path, never another matching receipt; also comparator NAME); otherwise refused naming the caller cwd, the checkout, both paths tried and the fix (absolute path, run from the checkout, or --repo DIR with --check). --check takes no lease and checks none, so --agent with --check is a usage error (exit 2) naming the writing form. identical re-gate = no-op "already gated". A receipt whose lean_toolchain is on lean-pkg's toolchain advisories list (known Lean kernel/runtime soundness bugs, src/lean_pkg/data/toolchain-advisories.yaml): one stderr line "WARN: toolchain advisory ID: TOOLCHAIN has a known Lean soundness bug, fixed in vX.Y.Z; LINK ..." per entry and JSON toolchain_advisories[] {id, toolchain, summary, fixed_in, links[], date_added} ([] when none; the same in gate --check, receipt check and palomar check, there after the verdict line), never a refusal. gate/regate record the receipt's lean_toolchain and mathlib_rev[:10] into lean_toolchain/mathlib_pin when each agrees with lean-toolchain / lake-manifest.json at the receipt commit (a prefix match is unchanged; one "pins updated" line; event and JSON pins {field: {from, to}}); a receipt whose lean_toolchain or mathlib_rev (prefix-equal) disagrees with lean-toolchain / the mathlib rev in lake-manifest.json committed at its commit is refused; with no readable mathlib entry the rev is not checked and the pin is kept: "NAME: pins kept: receipt mathlib_rev X does not match lake-manifest.json at (unreadable)", JSON pins_kept {field: {receipt, manifest}}; --check reports both, nothing written. report_sha256 must equal the SHA-256 of --verify.redacted.log wherever found (beside the receipt, .lean-receipts/, tracked at HEAD), else refused; a .gz copy (receipt --compress-log) is stream-decompressed and its UNCOMPRESSED bytes must hash to report_sha256 (never the .gz hash), the .gz to report_compressed.sha256 and the length equal report_compressed.bytes when recorded, output past that refused (gzip-bomb guard); none found (or a copy unreadable) is refused too: "report log missing: ...", naming where it looked and the path to restore it to (docs/receipts.md "Restoring preserved evidence"); the same check runs wherever a recorded lower-tier receipt is judged (ledger/promote, next, comparator, palomar, index check); JSON report_log {checked, log, where[], copy[]}; the sealed log beside --receipt is copied beside the canonical .lean-receipts/-.json when no copy is there, so it verifies on its own. Every check of both copies runs before either is written (a refusal writes nothing); a symlinked .lean-receipts or destination file is refused. --regate [--reason T]: re-gate verified-private (or public) in one step, status unchanged, event regated {previous_commit, commit, job_id, reason[, non_descendant]}; the commit must descend from the gated one unless --reason; plain gate on verified-private is refused naming --regate; --check --regate writes nothing. claims.yaml tracked at the receipt commit (never the working tree) must pass the claims/1 schema and every claim's decl must occur in its file at that commit (claims sync's check), else refused, nothing copied (JSON claims_schema {checked, commit, file, ok, claims, errors[], declarations {checked, ok, problems[]}}). Judged on the receipt commit's tree, refused (sources not bound): a committed symlink with an absolute or `..` target, or one resolving into .lean-receipts/ or to the formalization.yaml pointer; a lake-manifest.json `path` package whose dir leaves the package dir, or is (or passes through) a symlink, a submodule gitlink or an untracked dir (.lake/), or contains a gitlink. A tracked in-package path dependency is fine. Progress files (PROGRESS.md, state file, ledgers) live outside the package dir: any other change inside it needs a new receipt, and so does a .gitattributes/.gitmodules/.lfsconfig changed at the repo root or between it and a subdirectory package, unless the package opted in (update --accept-docs-descendants --reason R; record docs_descendants: true): then HEAD may also be a docs-only descendant of the receipt commit C, where no build input under the package dir changed (*.lean, lakefile.*, lake-manifest.json, lean-toolchain at any depth, the record's build_inputs globs, files the receipt's checker names; always refused: a symlink or gitlink added/changed/removed, a changed file a committed symlink points to, .gitattributes, .gitmodules, .lfsconfig, claims.yaml, and for a subdirectory package a .gitattributes/.gitmodules/.lfsconfig at the repo root or in any directory between it and the package dir; formalization.yaml keeps its derived-keys rule). The gated commit stays C; text "✓ HEAD is a docs-only descendant of (N non-build file(s): ...; opted in)"; gate/regate/comparator events and --json (and --check) add descendant_of C and docs_paths[] (<= 50). Without the opt-in a refusal the docs rule would have admitted adds the hint `update NAME --accept-docs-descendants`. flags: --receipt PATH (required), --comparator PATH (optional), --refuse-private (private paths in a receipt: refuse, exit 1, nothing copied; default a stderr WARN "receipt field F contains a ... (kept: ...; --refuse-private refuses such a receipt)" + JSON private_strings[{field, kind}]), --refuse-dirty (modified tracked files; default WARN + JSON dirty[]), --refresh-formalization [--agent A] (then regenerate formalization.yaml + pointer in one step, JSON "formalization": {...}; lease + schema checked BEFORE the gate; identical re-gate with a current file: refused, nothing written; no pointer recorded yet: the derived-only formalization.yaml exception applies to the path it will own), --check (read-only, any status: every gate validation vs HEAD, both tiers with --comparator; ✓ lines or gate's refusal; claims.yaml at the receipt commit: ✓ schema ok / ✗ first error (exit 1) / · not tracked; no write, no event; exit 0/1; JSON event gate-checked, checks[], claims_schema; comparator --check prints the same binding ✓ lines), --check --repo DIR (validate against the checkout DIR, not the registered local_path, this call only: never saved; stderr note; JSON repo_override {path, registered_path, remote_match}, null without it; DIR must be a git work tree and, when it has remotes, one must be the package's repo (a local-path repo /p also matches Host:/p, ssh://Host/p, file:///p; DIR = the registered local_path needs no remote), else the caller vouches; a writing gate refuses --repo, exit 2: it binds the registered checkout, move that with update --path). Success (and promote --yes) ends with a results-ledger: line (JSON rl_reminder, rl_hint): lean-pkg keeps no results ledger, the outcome is in `status NAME` and `claims ledger NAME`; add it to the project's own results ledger if it keeps one (docs/lifecycle.md#results-ledger) ex: lean-pkg gate my-lean --receipt /tmp/receipt.json --comparator /tmp/comparator.json | receipt slurm --job J --log PATH --commit SHA [--stdout JOB.out] [--stderr JOB.err] [--checker TEXT] [--repo DIR] [--redact REGEX]... [--sacct-file F] [--out PATH] [--append-readme] (no registry): writes the lower-tier receipt from a finished Slurm job; refuses (exit 1, nothing written) unless sacct's main job line is COMPLETED 0:0, the stdout's verify-log-sha256 = sha256(raw log) and pre-manifest-sha256 = post-manifest-sha256 = sha256(lake-manifest.json at SHA) (no --stdout: the log's own `verify-log-sha256:` line = sha256 of the log minus that line), stderr is empty, lean_toolchain/mathlib_rev from SHA agree with any log line, sorry 0 and axioms from the log (sorry-count:/axioms: lines, else 'sorry' warnings/#print axioms output; a sorry-count: below the log's own 'sorry' warnings, or an axioms: line omitting an axiom its #print axioms output reports, is refused; universe suffixes .{u} ignored), a checker (--checker or checker:), a log commit: line equal to SHA (none: refused without --stdout; with --stdout a WARN "the verify log has no commit: line; it is bound to the commit only through lake-manifest.json", JSON log_commit_bound false, also in the written receipt, and a `- WARN:` line in the README entry), fields read from the RAW log (a redaction that removes or alters a sorry warning, #print axioms output, a build-completion line or a key: line other than checker: is refused; checker is published redacted), no committed symlink at SHA into .lean-receipts/, and no public-safety blocking hit is left after redacting /tmp/-job, /scratch// and --redact (blocking also this machine's user and host names and a bare /home/, /Users/); --append-readme: a symlinked or non-UTF-8 README.md refuses before writing; job_id slurm-; writes .lean-receipts/-slurm-.json + -slurm--verify.redacted.log (report_sha256; --compress-log: <...>.log.gz instead, deterministic gzip, report_sha256 still of the uncompressed log, additive report_compressed {format gzip, sha256 of .gz, bytes}, restore gzip -dc X.log.gz > X.log; without it a log over 90 MiB WARNs naming the flag; log_commit_bound true/false; with --stdout also job_stdout_sha256 + manifest_sha256; additive keys gate ignores: it never reads log_commit_bound), prints the README entry (with --stdout a `- Seal:` line naming both; --append-readme: appended to .lean-receipts/README.md) and `gate NAME --check --receipt PATH`; --json {ok, receipt, log, report_sha256, job_id, sealed[] {role, path, sha256, receipt_key} (the exact files bound; systemd's `properties` is the raw unsealed capture), checks[], refusals[], ...}; --template (no other flag, no registry): print a minimal sbatch wrapper emitting every line the receipt reads (stdout seal lines, empty stderr, checker:/sorry-count:/axioms: in the log; exact-runtime preflight before any tool runs: LC_ALL=C LANG=C PYTHONUTF8=1 (#SBATCH --export line + export; stderr stays strict, never filtered) and a `type -P` probe of the host tools (+EXTRA_TOOLS) and, under $RUN, the first word of VERIFY_CMD/AXIOMS_CMD/LEAN_PATH_CMD (+lean beside lake, +RUN_TOOLS): a missing one fails the job before the work, log line runtime-preflight: ok (...); optional artifact seal ARTIFACTS_DIR=: after the audit the job copies every regular file under it to ARTIFACTS_OUT (default $OUT_DIR/artifacts-, never overwritten) with artifacts.sha256, sorted ` ` lines (a symlink, special file or newline name fails the job), and prints `artifacts-manifest-sha256 ` on stdout before post-manifest-sha256); --check --log PATH [--stdout] [--stderr] [--commit SHA] [--job J --sacct-file F]: preflight a job's files, every problem named, no sacct, nothing written, exit 0/1, --json {ok, log_commit_bound (true/false; null without --commit), checks[], problems[]}; --preflight-deps (--deps-tar T | --deps-dir D) [--commit SHA, default HEAD] [--entries GLOB]... (before sbatch, reads only, builds and writes nothing, exit 0/1): the import closure of the entry files committed at SHA (default Verify/**/*.lean, Audit/**/*.lean, OwnedAudit/**/*.lean, **/AxiomCheck*.lean, **/TypeCheck*.lean, **/Examples*.lean, **/OwnedAudit*.lean), followed through the package's modules and the dependency sources in the cache, must have every external module's .olean and .ilean (regular files) in exactly one manifest package (import Mathlib = Mathlib.olean and everything Mathlib.lean imports, transitively; toolchain roots Init/Std/Lean/Lake aside), every manifest git package present at its rev (.git/HEAD); --json {ok, preflight_deps, commit, entries[], required_external_modules, missing_count, missing[] {module, package, files, required_by}, checks[], problems[]}; + --fill-plan DONOR [--plan-out FILE] [--base-list FILE] (read-only; steps 1-4 of docs/receipts.md "Filling missing dependency artifacts from a pinned donor"): every missing module (no 500 cap), each with every regular file DONOR holds under its path in the package's .lake/build or build (lib/lean, lib, ir: .) with size and sha256; refuses (exit 1, refusals[] {code, reason}) on base-problem (a preflight problem other than missing files: not fillable), donor-cache, donor-toolchain (DONOR/lean-toolchain not the commit's byte for byte), donor-manifest (a manifest package not at its rev, the preflight's pin check), donor-source-edits (git status --porcelain --untracked-files=no non-empty, no .git directory or unreadable; GIT_OPTIONAL_LOCKS=0), olean-header (a candidate .olean's first 80 bytes (46 for format 1) differ from the base's, which must agree), donor-lacks-module (no .olean/.ilean in DONOR either), base-overlap (an addition is a base member, a --base-list name, or under a non-directory member), package-build (under the package's own .lake/build or a root namespace), plan-out (exists, inside DONOR/the base/.lake, unwritable); --plan-out FILE, only when ok: FILE = additions one per line (relative to the directory holding .lake, for tar -T) + FILE.provenance.json (schema lean-pkg-fill-provenance/1: commit, lean_toolchain, manifest_revs, base, donor, donor_checks, plan, additions, created_utc; collector provenance, never a job seal), never overwritten; the archive is written by the user and the preflight rerun on it confirms the fill; --json {ok, preflight_deps, fill_plan, commit, entries[], required_external_modules, missing_count, missing[], base, donor, donor_checks[] {check, ok, detail}, plan[] {module, package, lacking, required_by, fillable, files[] {path, size, sha256}, bytes}, not_fillable[], refusals[], totals {missing_modules, fillable_modules, files, bytes}, plan_out, checks[], problems[]}; --artifacts DIR [--artifacts-manifest NAME] (needs --stdout; also with --check): sha256(DIR/NAME, default artifacts.sha256) must equal the stdout's one artifacts-manifest-sha256 line, and every file under DIR is rehashed in 1 MiB chunks against it (missing, extra, changed files, symlinks, special files, path traversal, duplicate or unsorted entries refuse; previously copied files are adopted only by this rehash, never by another attempt's hashes); the receipt gains artifacts_manifest_sha256 (additive, gate ignores it) and the manifest is written beside it as -slurm--artifacts.sha256 (sealed[] role artifacts.sha256), JSON artifacts {ok, dir, files, bytes, manifest, manifest_sha256}; without --artifacts nothing changes | receipt systemd (alias local) --unit U --log PATH --commit SHA [--properties-file F | --run [--memory-max 8G] [--memory-swap-max 0] [--cpu-quota 400%] [--runtime-max 4h] [--setenv K=V]... [--require-tools A,B,...]... [--properties-out PATH] -- CMD...] + the same --stdout/--stderr/--checker/--repo/--redact/--out/--append-readme/--json: the same receipt from a finished systemd --user service unit; the unit state comes from --run (lean-pkg runs CMD bounded via systemd-run --user -p RemainAfterExit=yes, WorkingDirectory=--repo, so the finished unit stays loaded: properties are captured to .unit.properties before it is stopped and reset; --require-tools: each named executable resolved with type -P in the unit's PATH before the unit is created (paths and sha256 to stderr and --json run_tools; a missing one refuses, nothing run); the checkout must be at SHA with no tracked change and no untracked file (less .lean-receipts/, .lake/ and the run's own files; ignored files are not bound) under the package dir before and after), --properties-file (saved `systemctl --user show U -p ...` + a Hostname= line) or live `systemctl --user show U`; refuses unless LoadState=loaded, Id=U, terminal (failed/inactive or active+exited), Result=success (oom-kill, timeout, signal named), ExecMainCode exited with ExecMainStatus 0, NRestarts 0, plus every receipt slurm seal/field/redaction check (optional stdout invocation-id = InvocationID); job_id systemd-user::@ (label h-<12 hex of sha256(lower-cased host name)>; the name itself is never written); also writes --unit.properties (additive unit_properties_sha256); built-in redaction , , /run/user//; --run interrupted (SIGINT/SIGTERM/SIGHUP) while waiting: the unit is not stopped, its temporary LAKE_CACHE_DIR is kept while the unit may still run (removed when it is gone or finished), exit 128+N, and the recovery command `lean-pkg receipt systemd --unit U --log ... --commit ...` (no --run) is printed with a WARN that recovery skips the source-unchanged-during-the-run check verify NAME [--work-dir DIR] [--unit U] [--script verify.sh] [--judges N] [--agent A] [--reason T] [--dry-run]: the newcomer's one step to verified-private on this machine. Refuses first (nothing run) an unknown package, a checkout that is not a clean commit (untracked files other than this commit's receipts), no committed verify script, no comparator config, status scratch/archived/upstreamed, --registry-snapshot. Then, each printed and run as its own invocation, at HEAD X: (1) `receipt comparator --project CHECKOUT` (COMPARATOR_RECEIPT_NO_MATHLIB=1 when verify.sh declares `mathlib-rev: none` and the manifest has no Mathlib), (2) `receipt systemd --unit NAME-verify --receipt-commit X --log W/verify.log ... --run -- bash verify.sh W/verify.log` (W outside the checkout: $XDG_STATE_HOME/lean-pkg/verify/NAME/-), (3) an active package: `update NAME --status gate-pending --reason ...`, (4) `gate NAME --receipt LOWER --comparator COMP` (--regate for verified-private/public). Comparator first: it refuses untracked files, the lower tier allows .lean-receipts/; nothing is committed between them, so both bind X. A receipt of X already present is reused. Writes only what those commands write, commits nothing in the checkout; HEAD an evidence-only descendant of the gated commit: `already verified`, nothing run. coverage.yaml at HEAD with `stack: S`: lean-toolchain and the lake-manifest.json Mathlib commit checked against stack S, then the comparator receipt's tool digests; `on stack S (supported until D)` or a warning per difference, a stack past its window or undeclared here warns too; never refuses (proposal 0004). --json {ok, name, commit, checkout, dry_run, status_before, status, work_dir, steps[{step, command, rc, skipped?, output?}], receipts{lower, comparator}, gate, next[], stack (null without the key: {name, declared, matches, supported_until, window, toolchain, mathlib, comparator_tools, lean_pkg, mismatches[], warnings[]}), already?, error?} comparator attach NAME --receipt PATH (old spelling: comparator NAME --receipt PATH) attach comparator evidence to a verified-private/public package; no status change; event comparator-attached; identical re-attach = no-op; another receipt for the same commit: --replace keeps the old one as -comparator.replaced-.json, event comparator-replaced {replaced}. It is required by promote. The receipt is written by `lean-pkg receipt comparator` (the comparator-receipt program: the same code and flags) on a host its policy allows (a Slurm job, a host in COMPARATOR_RECEIPT_ALLOWED_HOSTS, COMPARATOR_RECEIPT_ALLOW_HOST=1, or the workstation default: no allow-list set, no Slurm on the machine, COMPARATOR_RECEIPT_WORKSTATION_DEFAULT not 0; recorded as `host h-LABEL: the machine running the command (workstation default ...)`). Stages checkout, cache-get, build, comparator, receipt log to /comparator-stages/NN-.log + stages.json (kept on failure; the error names the stage and log; --evidence-dir DIR, default .lake/comparator-receipt); readiness before any expensive stage: a .lake/.lake/packages(/*) symlink resolving outside the project is refused (the lake comparator sandbox cannot read it), and the checkout stage ends with `lake --no-build build M` per configured module (unknown target: fails naming the missing [[lean_lib]]); a judge that stops before judging (sandboxed dependency resolution) is a tool/environment error, not a rejection; --prepare runs only the setup stages (idempotent); a later run at the same commit/toolchain/config hash skips them (--from-prepared DIR: reuse DIR's, refuse a mismatch); receipt gains an additive stages[] summary; a run replacing an earlier run's stage files first keeps them read-only as comparator-stages/attempts/NNN/ + attempt.json {n, verdict, failed_stage, started_at, finished_at, olean_manifest_sha256, files sha256} (numbers never reused, never deleted or read back: resume/setup reuse/receipts use the current run only; prune by hand), `comparator-receipt --attempts [DIR] [--json]` lists them (exit 1 if a kept file changed). A receipt written in a Slurm job claims it only through SLURM_JOB_ID (job_id J, host_policy "Slurm job J on H"), which any shell can set: after the job finished, `comparator-receipt --seal-sacct R [--sacct-file F] [--user NAME] [--json]` (no host policy) corroborates it with sacct (main line J COMPLETED, 0:0; Start..End, with zone, containing generated_at; User = this account with live sacct or --user; NodeList = the receipt's host: its h- label against the node's label (or its first DNS label's), an older receipt's host name against the node name; an operator --host-label or a node range is not compared), refuses otherwise (exit 1, nothing written), and writes .lean-receipts/-comparator-sacct.txt (JobID|State|ExitCode|Start|End|Elapsed, UTC; no user or node names) plus the additive slurm_sacct {schema slurm-sacct-seal/1, job, file, sha256, state, exit_code, start, end, elapsed, checks, source} into R; only a sealed comparator receipt (seal committed at HEAD, rehashed and reparsed) backs a coverage.yaml compute job. flags: --receipt PATH (required); `comparator check NAME --receipt PATH` (old spelling: --check) validates only, records nothing ( works at any status; stderr `WARN: palomar: ...` when `palomar check` finds error gaps at the receipt's commit, JSON palomar_check as in publish, never a refusal), --check --repo DIR (validate against the checkout DIR, e.g. a worktree or feature branch, not the registered local_path; same rules as gate --check --repo: never saved, stderr note, JSON repo_override {path, registered_path, remote_match}, null without it; attaching refuses --repo, exit 2), --refuse-private, --refuse-dirty ex: lean-pkg comparator attach my-lean --receipt .lean-receipts/-comparator.json | comparator config --from-claims NAME [--out comparator.json] [--dry-run]: one TODO theorem_names entry per synced theorem/lemma claim not yet configured (name Audit.; the TODO markers go to lean-pkg-signoff.json configs[].scaffold.todo, never into the config; a config still carrying the deprecated inline lean_pkg_scaffold is refused until migrated); never overwrites; counts existing/added/skipped; --challenge-from-type pre-fills Challenge (elaborated type) + Solution (`exact @_root_.`) via `lake env lean` [--lake-env DIR --jobs N --timeout S], or split it: --emit-script F (bash F OUT.json on a Slurm node, JSON comparator-types/1; ENFILE/EMFILE: halves jobs, retries) then --from-output OUT.json (commit must be HEAD; driver exits 1 on extraction errors, 2 if none filled; ingest refuses those unless --allow-partial: failures kept TODO, extraction_failed; --checkout DIR instead of local_path; --claims-file PATH: claims from that working-copy claims.yaml instead of the synced registry cache (no claims sync; schema-checked like claims check --file, package must be NAME; never written to the registry; same config as the registry route for the same claims; output line `claims source:` and JSON claims_source {kind registry|file, path, sha256, synced_commit, claims}); --no-registry --out FILE: scratch config, no lease check); per entry: type_error keeps the TODO, needs_restatement flags project vocabulary; each printed type re-elaborated vs the decl (example : (T) := @decl), failure keeps TODO, round_trip_failed | comparator config --coverage NAME: read-only; claims covered/not/TODO by the config tracked at the gate-bound commit (never a candidate); a changed or uncommitted config cannot certify that tree, a new gate at a commit tracking it is required; prints the exact next commands (JSON next_commands[]) | comparator config --migrate-signoff PATH [--write]: no registry; moves the deprecated inline judged_as (-> configs[].definitions, one {reviewer, date, judged_as} per hole, config_sha256 bound to the migrated bytes) and lean_pkg_scaffold (-> configs[].scaffold) of that configuration into lean-pkg-signoff.json at the package root; dry run by default (prints both would-be files); refuses an invalid inline sign-off or a conflicting sidecar entry; the Palomar keys and their values never change, but the file's bytes do: a gated package needs a new comparator receipt (receipt impact + next commands printed; JSON {moved[], dropped[], config_sha256_before/after, receipt_impact, next_commands[]}) | comparator host-check: read-only, no registry: kernel, landlock ABI, bwrap, go/cargo/jq/git/lean/lake/python3 ok|warn|fail, then `mechanism toolchain|legacy: ok|fail` (toolchain = bwrap+lean+lake+python3, what Palomar runs; legacy = Landlock ABI>=1 + go/cargo/git/jq/lean/lake) + verdict naming only usable ones (exit 0 can / 1 cannot); warn git-env (JSON env_warnings[]) when GIT_DIR/GIT_WORK_TREE/GIT_INDEX_FILE/GIT_OBJECT_DIRECTORY/GIT_ALTERNATE_OBJECT_DIRECTORIES/GIT_COMMON_DIR/GIT_NAMESPACE is set (comparator-receipt and package-checkout git drop them; stages.json git_env_scrubbed[]); --routes (field report #5; run it before sbatch inside the job's image with the job's binds and PATH): per route judge (`lake comparator` in bwrap: the toolchain mechanism's needs; no unsandboxed route ever) / prepare (comparator-receipt --prepare: kernel+lake/lean/git/python3) / transfer (build here, judge elsewhere: prepare + tar/sha256sum) `route R: yes|no (reason)` + `run:` lines, executables resolved like type -P (the receipt slurm --template HOST_TOOLS list included; time: binary only), locale (LANG/LC_ALL/LC_CTYPE, C.UTF-8 installed, warn when a set locale is not installed: stderr warning; export LC_ALL=C LANG=C PYTHONUTF8=1), limits (ulimit -n soft/hard, /proc/sys/fs/file-nr; tight: LEAN_NUM_THREADS=3), resources (sched_getaffinity CPUs, cgroup v1/v2 memory limit, MemAvailable, SLURM_* allocation), advice[]; JSON additive routes_schema host-routes/1, routes[{route, supported, needs, failing, reason, commands, notes}], executables{name: {path, level, required_by[], note?}}, locale, limits, resources, advice[]; read-only, no network; exit 0 when any route is supported publish NAME --yes (old spelling: promote NAME --yes; `publish NAME --yes --dry-run` is the old `promote NAME`) flips GitHub visibility to public (ONE-WAY) + one notification (via LEAN_PKG_NOTIFY_CMD when set). Needs an authenticated `gh` (--yes: a failed gh query is a failure). Refuses without a byte- valid comparator receipt bound to HEAD, a claims ledger that is not ready (`claims ledger NAME`: every reusable claim verified, theorems/lemmas by the comparator too; no claims = unknown = refused; JSON claims_ledger {package_status, counts, required, reasons, ledger_digest}), both receipts + comparator logs committed unmodified at HEAD, HEAD in origin/ (local refs; --yes first runs git fetch --prune --tags origin incl. +refs/pull/*/head:refs/remotes/origin/pr/*, 120 s; a failed fetch is a ✗), (paper field) a paper unpublished with no arXiv id, and blocking public-safety hits (the whole repository when the package is a subdirectory of it; warn-only hits: a WARN line; skip: --skip-public-safety, a WARN). Evidence on disk that git ignores (receipts, comparator logs, comparator-stages/ files) is a WARN naming each path + rule (.gitignore:3:*.log) and the remedy (!.lean-receipts/ + !**/.lean-receipts/** after it, or git add -f); a not-committed ✗ names the rule; JSON ignored_evidence[{path, rule}] (also publish, and gate/comparator after attaching: stderr WARN). ex: lean-pkg publish my-lean --yes --dry-run # always read the checklist first | publish NAME [--dry-run] (read-only, the default without --yes): promote checklist (claims ledger included; JSON claims_ledger) + consent, license_spdx vs LICENSE, formalization.yaml current+valid, claims synced, the README page block (`page --check`; JSON page {status, adopted, problems[]}; not adopted: WARN, an unbacked Easley sentence: ✗), lakefile package name, tag at HEAD, a WARN item `palomar: not submittable ...` when `palomar check` finds error gaps at HEAD (JSON palomar_check {ready, commit, errors, warns, codes[], command}; never a ✗) (--public-safety: + the scan below, implies --dry-run); prints the next promote/tag/record commands (the tag push names the GitHub remote, found by URL); exit 0 ready / 1 not | public-safety NAME [--history|--no-history] [--strict] [--package-only] [--quiet] [--gzip-limit BYTES] (read-only; --quiet: summary + verdict, no hit lines): tree git would ship + (default) every blob/commit message/author+committer identity/annotated tag/branch+tag name on any ref; the whole repository when the package dir is a subdirectory (promote publishes it all; --package-only: the package dir alone); symlinks by target string; UTF-16/32 decoded; long lines in overlapping chunks; binary via printable runs; up to 64 MB per file, the rest listed in skipped[] and a blocking `unscanned` hit unless `allow: GLOB: ^unscanned$`; gzip content (bytes 1f 8b, any name; tree and history) stream-decoded up to --gzip-limit (env LEAN_PKG_GZIP_LIMIT, default 512M, K/M/G; 0 = off) and the DECODED text scanned instead of the compressed bytes (hit encoding gzip-decoded, location `path (decoded):LINE`; header file name/comment: gzip-header; decoded[] lists each; a binary decode such as a tar is scanned by printable runs, skipped reason `binary (gzip-decoded)`, not blocking); corrupt/truncated/over the limit/over the 500:1 ratio guard: hits of the decoded part kept, compressed bytes scanned as before, skipped[] `gzip ...` reason, a blocking `unscanned` hit unless allowed; for .lean-pkg-private-patterns regexes (# comments; bare or `block: RE` blocks, `warn: RE` warns, `allow: RE` exempts; `TAG: GLOB: RE` scopes any of the three to files whose package-relative path matches GLOB (* ** ?; no / = file name at any depth; trailing / = under that dir; never commit messages); tracked = a hit), a committed .lean-pkg-public-allow (allow: lines only, public on purpose; any other line ignored with a warning; inside it every allow line applies whatever its scope, and a line a private block pattern or registry-derived name matches is the blocking hit public-allow-private, tree and history; patterns_source public_allow_file, public_allow), built-ins (/home//, /Users//, ~/Dropbox/, approvals/, notes/, *.private, TODO-private, emails not declared: ordinary commit/tag addresses, consent[] or allow: lines; a host-like commit/tag address, user@hostname or a local TLD such as .lan or .invalid, is not declared and is an identity-email hit; a fixture address under .invalid in a file needs an allow line), names from the record's local_path/agent/workspace and its lease's agent/workspace/contact (an allow line exempts one only where its match in the token's non-space run covers it), internal paths (approvals/ notes/ drafts/ scratch/ *.priv), warn-only latex-label (lem:/thm:/eq:/sec:... keys, main.tex, \ref{ \cite{ \label{, Overleaf, arXiv ids; Lean-calibrated: never inside a name like foo_eq_bar, eq/def/ex only with `:`, key- only with a digit/capital/inner `.`, built-in allow def-eq defeq eq-of eq-iff ex-falso; the summary counts its warnings); hit = location (path:line, history: commit + path) + pattern label + severity (block|warn; warn printed as WARN) + excerpt with each match as […] (raw strings never printed); --json {ok, hits[], tree_hits, history_hits, block_hits, warn_hits, latex_label_hits, strict, scope, package_prefix, skipped[], skipped_blocking, decoded[] {where, path, compressed_bytes, decoded_bytes, content, complete, commit}, gzip_limit, patterns_source, warnings[]}; exit 1 on blocking hits (--strict: on any hit) | reservoir check NAME [--offline] (read-only): public, not a fork, >=2 stars (gh), lake-manifest.json + lean-toolchain tracked, LICENSE vs license_spdx, lakefile package + no `reservoir := false` (+ WARN without description/keywords/versionTags), lean-toolchain a release (rc/nightly: WARN), tag at HEAD; not yet public: GitHub items `pending promote: ...` (still ✗) + a `pre-promote:` line; then the Reservoir API (200: prints the `record ... reservoir-listed` command; never records itself); exit 0 eligible / 1 not | palomar prepare NAME [--out DIR] [--dry-run] (no network; submits nothing): bundle at /.lean-receipts/palomar-/ (never overwritten): formalization.yaml (rendered, schema-valid), configs/, receipts/, README.txt (manual steps + Palomar URL + the record palomar-submitted command), MANIFEST.sha256; refused without receipts bound to HEAD, without consent, on any error gap `palomar check` finds at HEAD (each listed as `✗ CODE: detail` + fix; nothing written, --dry-run too; its warn gaps are `lean-pkg: warning: palomar check: ...` lines, never a refusal; JSON palomar_check {ready, commit, errors, warns, codes[], command}), on blocking public-safety hits in the bundle; event palomar-prepared {commit, bundle, bundle_sha256} | palomar check NAME [--rev REV] [--config PATH] [--rules FILE] [--repo DIR] (read-only, offline; reads git objects at the commit: --rev, else the gate-bound commit, else HEAD): gaps to Palomar's mechanical rules, pinned at PalomarSubmission d4e41c1d5b0d (read 2026-10-16; --rules FILE: a newer browser-preflight-policy.json): every tracked .lean file of the repository starts with `module` (comments may precede; lakefile.lean exempt; .git/.lake excluded; <= 10,000 lines; no symlinks), lean-toolchain leanprover/lean4:vX.Y.Z[-rcN] >= v4.35.0-rc2, lakefile, no submodules, each comparator config (or --config PATH): required keys, no keys outside challenge_module/solution_module/theorem_names/definition_names/permitted_axioms/enable_nanoda (judged_as and lean_pkg_scaffold are refused), standard axioms, module sources tracked, Challenge <= 1,000 lines and 100 KiB, definition holes (warn); the headline configuration (registry headline_config, else comparator.headline.json): the same config checks, comparator.headline_uncovered (error: names not covered or holes unsigned by the gate-bound comparator receipt), comparator.headline_unjudged (warn: no receipt validates at HEAD), comparator.headline_missing/_invalid (error), JSON headline {config, source, judged, covered} or null; formalization.yaml tracked, v0.4-valid, no placeholders, Palomar's metadata minimum; one root licence file matching license_spdx; GitHub repo; visibility public and commit pushed (warn); gap {code, severity error|warn, paths[], detail, fix}; verdict first and last; JSON {ok, ready, commit, commit_source gate|head|rev, project_path, lean_toolchain, toolchain_advisories[], configs[], lean_files, missing_module, counts{error, warn}, gaps[], rules{}, not_checked[], repo_override}; exit 0 no error gap / 1 error gaps / 2 usage | palomar port-modules NAME [--dry-run (default) | --write] [--agent A] (reads git objects at HEAD; never commits, never the registry): the mechanical port of the package's tracked .lean files to the module system: `module` first (after ordinary comments; before /-! -/ and /-- -/), `import X` -> `public import X` (`meta import` -> `public meta import`; `import all`/private/public kept; never `public import all`), body in `public section` ... `end` (no `end` when a scope stays open); module-headed files skipped (a re-run is a no-op); refused per file: prelude, non-UTF-8, symlink; review items (never auto-fixed, lines of the ported file): expose (a def another file unfolds/simp/rw/rfl/decide: add @[expose]), private, meta (#eval/native_decide/initialize), imports-non-module, scope-balance; .lake/, lake-packages/, nested Lake projects, path deps excluded, lakefile.lean exempt; dry run: per-file report + unified diff; --write: clean working tree only (dirty/untracked, a refused file, or a foreign live lease without --agent: exit 1, nothing written), then follow-ups (lake build, @[expose] review, palomar check after the commit, a new gate for a gated package); JSON {ok, name, dry_run, written[], commit, project_path, files[{path, action port|skip|refused, reason, edits[], reviews[{code, line, detail}]}], counts{port, skip, refused, review}, expose[], excluded[], vendored_dirs[], outside_package, diff, follow_ups[]}; exit 0 / 1 a refused file blueprint check NAME [--decls PATH] (read-only; clean checkout): lake build, then lake exe checkdecls PATH (default blueprint/lean_decls, leanblueprint's list of the \lean{} names; PatrickMassot/checkdecls, a Lake dependency the package adds, pinned rev 3d425859e73f; never edits the lakefile: without it, refused with the require line); every `NAME is missing.` line is reported; then claims.yaml at HEAD: a claim whose decl the blueprint names must be accepted by checkdecls (else problems[]); claims outside the blueprint and blueprint names without a claim are notes; no blueprint/ and no list: skipped, exit 0; JSON {ok, commit, skipped, reason, decls_file, declarations, missing[], checkdecls {rev, url, pinned}, claims {file, present, checked, problems[], outside_blueprint[], blueprint_without_claim[]}}; exit 0 nothing missing / 1 registry audit (old spelling: audit) read-only without --write (old spelling --fix) (expired leases reported); --fix: sweep leases, gh -> registry visibility; toolchain/formalization.yaml drift; receipt/comparator drift judged at the reference branch tip (origin/HEAD, else main, else master; local refs; a checkout elsewhere: checkout-branch finding). --toolchain-floor V (env LEAN_PKG_TOOLCHAIN_FLOOR; default leanprover/lean4:v4.35.0-rc2): below-toolchain-floor, rc < release, nightly -> toolchain-unparsed, scratch/archived exempt; floor is warn only for public/comparator-evidence packages or --promotion, else level info; --json findings carry level warn|info; repo not on GitHub -> no-github-mirror (human: one line); informational: receipt-untracked (receipt file not tracked at the tip), duplicate-path (two packages, one checkout), duplicate-namespace (two checkouts, one Lean root namespace), consent-duplicate (one who+role recorded twice; shown once), claims-coverage-none (claims coverage none|empty|unsynced: search falls back to declarations; --json coverage; archived/upstreamed skipped); a failed gh query: check gh-OUTCOME, gh = gh-missing|not-authenticated|no-access|not-found|error, detail names the remedy (archived + not-found: info); human line `LEVEL CHECK NAME: DETAIL`, the line "N finding(s): W warn, I info" first and last (--quiet: it alone); --json counts {warn, info}; --no-gh: gh-skipped (info); missing-path: recorded path + `update NAME --path DIR --reason .. --dry-run` (+ "found at DIR": a sibling with lakefile + same remote); palomar-not-ready (warn; only packages aiming at Palomar: upstream_target palomar or a palomar entry, not scratch/archived/upstreamed): `palomar check`'s error gaps at its commit (gate-bound, else HEAD), detail = count + codes + `lean-pkg palomar check NAME`, --json palomar {errors, codes[], commit, command}; warn gaps alone: no finding. ex: lean-pkg audit --json registry validate schema + enum + history sanity. ex: lean-pkg registry validate next NAME [--agent A] [--repo DIR] read-only, offline (never gh, never writes): the ONE recommended next command + a one-line reason, from the record + checkout (claim / update --status / gate --check / gate / gate --regate (verified-private, HEAD moved) / comparator-receipt / comparator config --from-claims / comparator / publish --dry-run (only when the claims ledger is ready; else its first fix or `claims ledger NAME`) / reservoir check / palomar prepare / record ...); without --agent a live lease is only noted; a checkout off its default branch (or detached) is noted, HEAD still judged; --repo DIR evaluates the checkout DIR instead of the registered local_path for this call (never saved; stderr note; JSON repo_override {path, registered_path, remote_match}, null without it; DIR a git work tree whose remotes, if any, include the package's repo (Host:/p matches a local-path repo /p; the registered local_path itself needs no remote); carried into a recommended gate --check, any other recommended command that reads the checkout gets a note that it uses the registered path); a comparator step (comparator-receipt, comparator config) whose lean-toolchain at HEAD is below audit's comparator floor (--toolchain-floor default / LEAN_PKG_TOOLCHAIN_FLOOR) is blocked first: command null, blocker below-toolchain-floor {lean_toolchain, floor, deferred_command}, reason says bump the toolchain, commit, re-gate; exit 0 command (or nothing left: command null), 1 blocked; --json {ok, name, command, reason, blockers[{kind: foreign-lease|invalid-lease|missing-checkout|no-commit|dirty-tree|invalid-receipt|unreadable-receipt|below-toolchain-floor, detail}], notes[], repo_override, state{status, lease, gate_commit, comparator_commit, head, dirty[], receipt_candidate, claims_ledger, ...}}. ex: lean-pkg next my-lean --agent vera --json doctor ok/warn/n/a: version, install, registry [source: flag|env|user-default|cwd], user-default, events [source: flag|registry-sibling|env|sibling], registry-repo (behind/ahead of origin or no origin remote, dirty registry files: warn = do not write yet; --fetch first), index, host (comparator host-check verdict; warn = cannot produce comparator receipts or a leaked GIT_* repository variable), tools (n/a = optional; the detail says what it is for and when it is needed; tool comparator without bwrap: run `comparator host-check`), gh auth (account; warn = not logged in, promote needs it), python, stack (n/a: the declared LTS stacks and the current one; doctor NAME: the package's committed lean-toolchain, Mathlib commit and recorded comparator receipt's tool digests against the stack its coverage.yaml declares, warn on a difference, a stack past its window or one this lean-pkg does not declare; --json adds stack {name, declared, matches, supported_until, window, toolchain, mathlib, comparator_tools, lean_pkg, mismatches[], warnings[]} or null); exit 1 if the registry is unreadable or its schema version is unsupported (every other command refuses a newer version: upgrade lean-pkg). doctor --upgrade-from OLD [--to NEW] [--source DIR] (read-only, no registry, no network): instead of the checks, what changed for a package author from OLD (a version: tag vX.Y.Z or the `release: X.Y.Z` commit; or any commit) to NEW (default HEAD) of a lean-pkg git checkout (default: the one running), read from git objects and never executed: requires-python, dependencies, executables, format markers (x/N constants, registry version, formalization.yaml version), on-disk key lists, commands/options from the help goldens (renamed = alias kept), --json key sets, aliases, packaged files; plus the curated docs/upgrades/.yaml entries whose PR (#N) lies in OLD..NEW (behavior[], breaking[]) and the range's PRs no record names (uncurated[]); --json schema lean-pkg-upgrade/1. docs/design/upgrade-preflight.md llms this contract (--json: {"ok": true, "text": ...}); --short: ~40 lines cut from it by section (title, PURPOSE head, STANDING RULES, the first line of each subcommand; --json adds "short": true; the rest, e.g. publish, public-safety, reservoir check, palomar prepare, comparator config/host-check, release --fresh-repo/--adopt-repo: the full text). ex: lean-pkg llms --short | help [TOPIC|COMMAND ...] gh-style help topics, no registry read: exit-codes (0/1/2, what 1 means per command, comparator-receipt/lean-exercise codes), environment (every variable lean-pkg, comparator-receipt and lean-exercise read, with its default; --json variables[{name, section, meaning, default}]), formatting (--json, stdout vs stderr, named schemas, jq); no argument: commands + topics; COMMAND: exactly its --help; unknown: exit 2. ex: lean-pkg help environment registry wiki render a Markdown status page. ex: lean-pkg registry wiki --out status/index.md | report (read-only): a bug report in the shape of .github/ISSUE_TEMPLATE/bug_report.md: version + doctor ok/warn lines + host-check verdict, --command "ARGS" re-run in a subprocess (+ --json when the subcommand has it; a writing command is not re-run), --body TEXT (no re-run) and/or --from-log FILE[:N] (last N lines, default 200, as Log excerpt) first in What happened (one of --command/--body/--from-log required, else exit 2), --package NAME record (status, lease, receipt commits); every captured text redacted (registry/checkout paths -> //, home -> ~, public-safety built-ins + .lean-pkg-private-patterns of the checkout and registry dir + record-derived names -> […]); a blocking hit left: exit 1, nothing filed. Dry run unless --yes: gh issue create -R lean-pkg/lean-pkg (--repo OWNER/NAME) --label bug|enhancement (--enhancement), prints the URL; no gh or gh not logged in: exit 1 (gh auth login). --json {ok, filed, url, title, labels, body, redactions, log_excerpt {path, lines} with --from-log}. ex: lean-pkg report --command "status my-lean" --package my-lean index public catalog //entry.yaml + receipts/ (root: --index, env LEAN_PKG_INDEX, index/ beside the registry if present, ./index; check/render/migrate exit 1 when it is missing). add NAME --by HANDLE --headline 'Name :: File.lean :: One sentence.[ :: ChallengeTheorem]' [--from-registry] [--repo URL] [--repo-dir P] [--lower REL] [--comparator REL] [--license SPDX] [--tag T] [--field-tag T] [--consent-recorded] [--allow-unpushed] (default: the pin and evidence must be on a branch of the public repo; consent must be recorded) validates the receipts at the pin (their commit) in a clone; trust computed; receipts copied verbatim; duplicate repo+commit refused; never writes local_path; event index-added (event log only). check [NAME ...] [--clone | --repo-dir P] static without a source; else re-derive from bytes at the pin. Palomar/Reservoir verified by API when reachable, else "skipped" (never failed, never passed). exit 0/1/2. render [--out PATH] [--check] Markdown table, default /README.md; --check exits 1 when stale. migrate [--check] rewrite index-entry/1 entries as index-entry/2 (claims derived from the headline). claims claims.yaml (schema claims/1) at the package repo root: named reusable results, cached in the registry. sync NAME read claims.yaml at HEAD (committed bytes only); every decl must occur in its file; event claims-synced; a pin on no remote-tracking branch (unpushed) prints a stderr WARN (--json pin_published true|false|null). mark NAME --from-comparator CONFIG.json --status reusable|internal|experimental [--write|--dry-run] [--agent A]: set status on exactly the claims whose decl the config's theorem_names cover (the --coverage/ledger rule: full name or . of a fully qualified decl), in the checkout's working copy; default prints the plan; --write edits only those status values (else re-dumps, reformatted true), never commits, never the registry; lists unmatched names, then the rule and a hint per name that differs from exactly one claim's decl only in its leading namespace component (never applied); --json {ok, name, file, config, status, matched[{id, decl, from, to, changed}], changed, unmatched[], written, reformatted, rule, hints[{name, decl, shape, rename_to, hint}]}. sync and check print `WARN NAME: gated, N claim(s), none with status reusable: ...` (--json warnings[]) for a gated package with no reusable claim. | list [NAME] | check [NAME] [--file PATH] cached claims with status and derived trust | re-validate; exit 0/1 (--file: schema-check a working-copy file, schema only: no checkout, so declarations unchecked; no registry; --json {ok, path, claims, errors[]}). With NAME both report coverage synced|empty|unsynced|none (--json: coverage, cached_claims, claims_yaml present|absent|unknown, legacy_claims[], hint); check NAME exits 1 on none/unsynced (no coverage is not ok) and names any legacy *claims.json in the checkout | migrate NAME --from PATH [--out claims.yaml] [--dry-run] [--agent A]: legacy JSON rows -> a claims/1 skeleton in the checkout (mapped fields; TODO markers, TODO.lean for the rest, which sync refuses); never overwrites, never writes the registry, grants nothing: commit it, then claims sync. | ledger NAME [--stage gate|promote]: read-only, nothing stored: each claim (claims.yaml at the gate-bound commit, else the cache) with named diagnostics from the recorded receipts, re-checked with gate's and promote's validators; a claim is verified only with zero diagnostics. Claim status: out-of-scope (internal/superseded) | blocked (a depends_on claim not verified) | unknown (unreadable evidence) | verified | open. Required = status reusable; --stage promote (default) also needs the comparator tier for reusable theorems/lemmas. Package status fails closed: unknown (no claims, none reusable, no checkout, unreadable evidence) | failed (evidence contradicts a required claim) | open | ready. Codes: docs/lifecycle.md. Exit 0 only when ready, else 1; --json {ok, package_status, reasons[], stage, bound_commit, receipt_sha256, comparator_sha256, counts, claims[{id, decl, kind, claim_status, required, status, statement_basis, manuscript_findings[], diagnostics[{code, detail}]}], manuscript_findings {total, open, fixed, by_kind, corrected_statements[], findings[], source}, ledger_digest} (sha256 over the canonical claims, codes and receipt hashes: recompute, never trust a stored one). Manuscript findings change no status (publish --dry-run and palomar prepare print the same one-line summary, JSON manuscript_findings); a lean_evidence decl missing at the bound commit is finding-evidence-missing. | rebase NAME --from-tex OLD.tex --to-tex NEW.tex --to-aux NEW.aux [--from-aux OLD.aux] [--from-sha256 HEX] [--to-version arXiv:IDvN | --to-commit HEX [--to-repo URL]] [--unwrap-macro NAME ...] [--claims-file PATH] [--coverage-file PATH] [--out-dir DIR] (#6): move claims.yaml + coverage.yaml (committed at HEAD) to a new manuscript version; never writes the registry or the checkout, never changes a claim status, never sets fixed_in. Refused: OLD.tex's sha256 differs from coverage.yaml's manuscript sha256, or is none of the .tex hashes of the data/source-baselines record of its arXiv version (none recorded: --from-sha256 must state it; the proposal drops eprint_sha256), TeX not UTF-8 or with unbalanced begin/end, a referenced label defined twice (OLD, NEW or NEW.aux). References: coverage rows (paper.label, else paper.number via --from-aux), manuscript_findings location.label (a TeX label, else a number via --from-aux), TeX labels named in a citation. Per label, the enclosing statement (theorem-like incl. \newtheorem names) or equation environment in OLD vs NEW, normalized (comments, label commands, \textcolor/\colorbox/\color, --unwrap-macro, ~, whitespace, trailing . , ; :; braces kept): unchanged (carried; number token re-keyed from NEW.aux, finding page from NEW.aux, tex_line shifted only when the environment is byte-identical, else null) | changed | missing | moved-into-proof | not-in-old | unsupported | unnumbered (no NEW.aux number); all but unchanged need review and are left as they were. --out-dir (new or empty; files read-only): claims.yaml, coverage.yaml (manuscript.version = --to-version or {repo, commit, sha256 of NEW.tex}; required when coverage.yaml exists), rebase-report.json (schema claims-rebase/1), rebase-report.md (old/new excerpts), review/NNN-LABEL.{old.tex,new.tex,diff}, MANIFEST.sha256; deterministic. Without --out-dir: report only. --json {ok, name, written, out_dir, counts, labels[], rows[], findings[], citations[], needs_review[{where, label, status, reason}], proposed_errors[], statuses_changed, normalizations[], inputs, to_version, warnings[], files[{path, sha256}]}; exit 0 everything carried / 1 something needs review or refused / 2 usage. docs/prior-art.md#move-to-a-new-manuscript-version formalization NAME [--write] [--no-registry] [--out PATH] [--force [--reason TEXT]] [--author A ...] [--headline-config PATH] [--repo DIR] [--agent A] render formalization.yaml (mathlib-initiative v0.4, what Palomar reads) from the registry + the repo at HEAD. Derived every run: project.name/license (license_spdx), automation.notes, status.sorry_count/axioms/evidence (gate receipt), status.main_results (every tracked comparator config: comparator_config, declaration, file; definition holes carry judged_as, from lean-pkg-signoff.json or the deprecated inline key, null when unsigned; with a headline configuration (--headline-config PATH, else registry headline_config, else comparator.headline.json when tracked; Palomar's six keys only, else refused) its theorems only, when every name is covered (the --coverage rule) by a config with the same challenge/solution modules in the gate-bound comparator receipt validated at HEAD and every hole is signed in lean-pkg-signoff.json by such a config, else refused naming them; no receipt validating at HEAD: not applied, stderr warning, the default; --write records --headline-config; JSON headline {config, source, applied, reason, receipt, theorems} or null), alignment (claims.yaml). Every other key is KEPT from the file; first render seeds authors from consent[] owner/author, else "[PLACEHOLDER] ..." + stderr warning (never invented: no paper titles). --write: idempotent; lease + update checked BEFORE writing (foreign lease: --force --reason); a differing file needs --force; --write also sets the registry pointer (a registry write); --write --no-registry: the file only, registry untouched (no lock/--commit). --repo DIR: read that checkout instead of local_path for this call (never saved; not with --write, exit 2; the checkout rules and stderr note of page --repo): claims, comparator configs, the kept keys and the receipts at DIR's committed HEAD, never its working tree; the registry's gate receipt feeds status.sorry_count/axioms/evidence only when it validates at that HEAD, else they are omitted with a warning; JSON repo_override {path, registered_path, remote_match, head, source committed-head, receipt_facts {receipt, included, reason}}, null without it. Validated against the vendored v0.4 schema (jsonschema, else structural). audit: formalization-missing/-drift. docs/formalization.md | coverage check NAME [--file PATH] [--allow-private-manuscript] read-only; exit 0/1. coverage.yaml (schema coverage/1, package dir, committed at HEAD; --file: a working copy) is the paper-centric map: manuscript {title, version: "arXiv:IDvN" | {repo https, commit 40hex, sha256 64hex} | "unposted" (refused without --allow-private-manuscript)}, summary (one line), rows[{paper {number, title, label?}, class same-assumptions|inputs-supplied|outside, claims[] (ids in claims.yaml at HEAD; none for outside; superseded refused), inputs[] (required for inputs-supplied, refused for same-assumptions), note?}], nothing_excluded {reason} (only when no outside row; one of the two is required), compute[{cluster: easley, jobs: [slurm-J]}] (each job a Slurm receipt committed under .lean-receipts/), lean_pkg_version {version, doi} (checked against lean-pkg's own CITATION.cff when readable), stack lts-YYYY.04|10 (optional, both kinds: the LTS stack the package opts into, name shape checked here; doctor NAME, verify and page check the pins against it, never failing a check). The lab's lean-scope-page rules that apply: no placeholder text (FILL-ME, TODO, TBD, FIXME, XXX), every named claim's file committed at HEAD, every theorem of the recorded comparator receipt the decl of a claim some row names, every configuration there with definition_names carrying judged_as.reviewer. Strict: exact key sets, closed enums, duplicate keys refused. --json {ok, name, file, rows, counts, manuscript, private_manuscript, errors[], warnings[]}. docs/page.md | page NAME [--write | --check | --out PATH] [--site DIR] [--html PATH] [--repo DIR] [--allow-private-manuscript] [--agent A] the README verification section, rendered between and in the package README.md from coverage.yaml, claims.yaml, the claims ledger (promote stage: a row is "verified" only when the ledger closes every claim it names), the receipts committed under .lean-receipts/ (allow-listed fields only: commit, toolchain, Mathlib rev, sorry count, axioms, theorem/permitted-axiom/definition names, date, SHA-256, slurm-J job ids; never hosts, paths, users), lean-toolchain, lake-manifest.json, CITATION.cff (authors required), registry repo/status/license_spdx/doi. Sections: status capsule, paper-Lean map, Not formalized, trust boundary, reproduce, evidence, citation, license, acknowledgments (always the lean-pkg credit with the concept DOI; the Easley sentence only when coverage.yaml compute names easley jobs backed by committed Slurm receipts). Deterministic; every rendered string passes the public-safety scanner + the package's .lean-pkg-private-patterns (a blocking hit refuses). Default: print the block. --write: replace only the marked block (append when absent; prose outside untouched; never commits; a foreign live lease refuses without --agent HOLDER); not a registry write (no lock/--commit). --check: exit 1 when README.md is missing, the block is missing or stale, the lean-pkg credit is missing, or the Easley sentence appears without backing; writes nothing. --site DIR: also write DIR/verification.md (the full page, one H1) and DIR/coverage.md (every row: claims, decls, each claim's ledger status, inputs, note) for MkDocs; --html PATH: one static HTML file of both (no script, no external asset, inline CSS, every text escaped, links only https/#anchor); the same bytes whatever DIR; atomic writes, symlink targets refused; with --check they are compared instead (missing/stale: exit 1). User text is escaped in every output (&<> as entities, Markdown markup backslash-escaped). --repo DIR: read that checkout instead of local_path for this call (CI; not with --write). publish --dry-run carries the same check as one checklist line (JSON `page`). --json {ok, name, readme, markdown, written, unchanged, current, problems[], warnings[], site_files[{path, status written|unchanged|current|missing|stale|refused}], repo_override, rows, counts, verified_rows, ledger_status, ledger_digest, private_manuscript, manuscript, easley {backed, jobs}, receipts}. docs/page.md | formalization anchor NAME --arxiv v (--from-file E-PRINT | --fetch) [--compare-tex LOCAL.tex [--accept-diff REASON]] [--main-tex PATH] [--write] [--agent A] pin the companion to one arXiv version: the version is required (unversioned: exit 2); network only with --fetch (https, 60 s, 64 MiB); the e-print (tar.gz|gz|tar; PDF-only refused; absolute/../link/device members refuse it) is read in memory and recorded in data/source-baselines/arXiv-v.json (source-baseline/1, deterministic: e-print sha256, .tex/.bib/.bbl/.sty sha256, main_tex, compare, retrieved_at/arxiv_api only when fetched); without --write a dry run; --write refuses unless tied (coverage.yaml already that version, a bound {sha256} equal to an e-print file, or --compare-tex identical / --accept-diff REASON, recorded), then sets coverage.yaml manuscript.version + eprint_sha256 and the formalization.yaml sources[].id; never the registry or a commit; a move from another version prints rebase_command (claims rebase). | formalization kept [--repo DIR] [--file REL] [--at REV] [--against REV2] read-only, no registry: the kept view (formalization.DERIVED_PATHS and the renderer's acknowledgements lines removed; YAML 1.1 safe, timestamps kept as strings) as canonical JSON (sort_keys, separators ',' ':', ensure_ascii false, UTF-8, no trailing newline) + its sha256, for a release-input audit; --at REV: the committed file; --against REV2: changed_kept_keys, exit 1 when any; --json {schema formalization-kept/1, kept_view, canonical, sha256, commit, derived_paths, against {rev, commit, sha256}, changed_kept_keys, same}. docs/formalization.md#the-kept-view search TERM [--package NAME] [--offline] [--sources a,b,c] [--loogle] [--loogle-query PATTERN] [--require-complete] [--cache-dir DIR] [--record [--repo-dir P]] [--json] prior-art search. Routed by shape: a Lean pattern (→ -> ∀ fun : ( ? _ ⊢ " math operators, Nat.x dotted names) is `signature` and goes to Loogle; prose is `natural-language` and Loogle is skipped ("natural-language query; Loogle takes declaration patterns ..."); --loogle forces it; --json: top-level and per-source route. Loogle parses Lean, not prose: a term mixing the two fails there ("query not understood: Unknown identifier ...; Loogle takes Lean names, terms and patterns ... --loogle-query"); keep the prose as TERM and pass the Lean part as --loogle-query PATTERN (Loogle gets PATTERN whatever the route, every other source the term; --json loogle_query; usage error when --sources leaves out loogle). --require-complete: exit 1 when complete is false (a source skipped, failed in part, capped or incomplete); the output is printed in full first, --json gets ok false + error "search incomplete (--require-complete): skipped: ...; ", stderr the same line; without it an incomplete search still exits 0. Cache: Palomar snapshots and the Reservoir index are cached under $XDG_CACHE_HOME/lean-pkg (default ~/.cache/lean-pkg) and refreshed by any online search, --record or not (the registry is never written without --record); each block's cache_writes[] and --json cache {root: --cache-dir|XDG_CACHE_HOME|default, writes[] (paths relative to the cache root)} say what was written, and the text adds "cache: wrote ... under ..."; --cache-dir DIR uses DIR as the lean-pkg cache for that search only (or set XDG_CACHE_HOME for a whole session). order: registry, index, loogle, leansearch, reservoir, palomar, github; each "ok" or "skipped: " (never zero hits). local score: exact alias or package name 3, keyword 2, every term word 1; registry hits: packages (name, notes, owner_project, repo; hit_kind package) and claims; a package without synced claims is searched by declaration in its checkout at HEAD (tracked *.lean names + docstrings; hit_kind "declaration (unclaimed)", trust none, file PATH:LINE, after claim hits), and a "registry coverage: N of M packages have no synced claims: D searched by declaration only, K not searched (no checkout: ...)" line precedes consulted: (--json coverage {claims, declaration_only, not_searched[], not_searched_reasons[] {package, code no-path|no-checkout|no-git-head|scan-error, remedy (read-only, no host path), detail (scan-error only, else null: "git grep exit N: " or "git grep killed by signal N ...", never git's stderr), the coverage line names it: "scan error: NAME (git grep exit 128: ...)"}, declaration_hits_omitted}; coverage is computed per run from the registry file (read once, written atomically) and the checkouts at HEAD, with no shared cache, so two runs differ only when a checkout, its HEAD or a git grep outcome differs); any skipped source adds "incomplete: searched N of M sources; skipped: ..." before consulted: (--json complete, searched, skipped_sources[]); a source that answered only in part (GitHub code or repository search failed) stays ok with partial[] in its block, is listed in truncated_sources and named on the incomplete: line; a part that returned its result limit (GitHub 30) is listed in capped[] (cap_limit) and truncated_sources ("github: code search returned its 30-result limit"). exit 0 even with zero hits; 2 on usage errors. --record: docs/prior-art/-.md in the package checkout (or --repo-dir; never the registry dir; never overwritten; "decision: pending" for a human) + event prior-art-searched; prints "note: is new; a strict MkDocs build needs a nav entry (or a literate-nav glob) for it" when the repository has an mkdocs.yml (--json nav_hint {path, reason}, else null; mkdocs.yml is never edited). claim/index add print advisory notes on stderr (`notes` in --json). RECEIPT SCHEMA (JSON object; `gate` enforces every line) commit 40 lowercase hex; MUST equal HEAD, or HEAD must be an evidence-only descendant of it (only .lean-receipts/ paths differ between the two commits) lean_toolchain string; MUST equal the lean-toolchain file committed at `commit`, stripped (the working tree never counts) mathlib_rev nonempty string (full mathlib rev; `none` for a package whose lake-manifest.json lists no mathlib) sorry_count integer; MUST be 0 axioms list of strings; subset of gate.axioms_allowed (default exactly: propext, Quot.sound, Classical.choice) report_sha256 64 hex chars; SHA-256 of the verification report job_id nonempty terminal executor job identity, unique within that executor (stored as -.json) checker nonempty exact checker command/mode (e.g. serial leanchecker manifest) generated_at ISO-8601 timestamp; MUST parse COMPARATOR RECEIPT SCHEMA ("comparator-receipt/2"; "comparator-receipt/1" still validates; written by comparator-receipt; `promote` re-derives every line from bytes) schema "comparator-receipt/2" (or "/1": legacy mechanism implied) mechanism "toolchain" (lake comparator + the toolchain's bundled NanoDa/con-ron; Lean v4.35.0-rc2+; what Palomar runs) or "legacy" (pinned comparator/lean4export/nanoda/landrun stack); comparator-receipt --mechanism auto|toolchain|legacy commit 40 lowercase hex; MUST equal the lower-tier receipt commit, and equal HEAD or have HEAD as an evidence-only descendant (only .lean-receipts/ differs, plus the recorded formalization.yaml when only its derived keys changed) lean_toolchain MUST equal the lean-toolchain file committed at `commit`, stripped tools legacy: {comparator, lean4export, nanoda, landrun}: 40-hex commits actually used toolchain: {lean_toolchain, lake_sha256, leanexport_sha256, leanchecker_sha256, nanoda_bin_sha256, con-ron_sha256}: 64-hex sha256 of the judging binaries under `lean --print-prefix`/bin host, job_id, generated_at nonempty (Slurm job id, or local---); generated_at MUST parse as ISO-8601; host (and ) is the host's label, never its name: h- + 12 hex of the SHA-256 of the lower-cased host name, or --host-label (a receipt by lean-pkg 0.10.0 or earlier may name the host: still valid; public-safety reports them as receipt-raw-host) host_label optional, not validated: the label in host (always written since host labels) host_policy optional; the runner's host-policy reason (an override run is visible here); a "Slurm job J" claim backs coverage compute only with slurm_sacct, comparator-receipt --seal-sacct; stack_limit optional, not validated: {soft_kb, hard_kb, source} the lake/lean children ran under (COMPARATOR_RECEIPT_STACK=unlimited| raises it; WARN at <= 8 MiB); build_provenance optional, not validated: {compiled, modules_built, prebuilt, source} whether the build stage compiled any of the package's oleans or found them prebuilt (source: COMPARATOR_RECEIPT_BUILD_SOURCE, redacted); comparator --check and gate --check print it; lean_threads optional, not validated: N or null, the LEAN_NUM_THREADS given to the lake/lean children (COMPARATOR_RECEIPT_LEAN_THREADS=N); olean_manifest optional, not validated: {schema olean-manifest/1, files, sha256, lean_toolchain, lake_manifest_sha256, captured} the digest of the sorted ` ` lines of the package's own compiled modules under .lake/build/lib (comparator-stages/03-build.oleans.sha256), recorded after setup and rechecked by the runner before and after the comparison (a difference fails the stage, nothing written; it also keys the slot cache); `comparator-receipt --verify-oleans [DIR] [--json]` is the read-only check (exit 0 same, 1 different/none recorded) test_only, partial if present and true (a test-only override; a --slots subset run) the receipt is REFUSED result "pass" (the runner writes a receipt only on PASS) configs[] MUST list exactly the comparator*.json / comparator/config*.json files tracked at HEAD (no omissions, no extras). Per config: path, sha256 of its HEAD bytes; challenge_module, solution_module, theorem_names[] (non-empty), definition_names[], permitted_axioms[] (subset of gate.axioms_allowed) — each MUST equal the config file at HEAD; non-empty definition_names MUST be signed off in lean-pkg-signoff.json at HEAD: configs[] {config_sha256 (the config's bytes), definitions {: {reviewer (human, never a model/agent token), date YYYY-MM-DD, judged_as text}}} (deprecated, warned: inline judged_as {reviewer, date, definitions ⊇ definition_names, basis?}) — comparator never compares hole bodies (runner before a run + every validator; the receipt's copy, signoff {source, definitions}, MUST equal the sidecar's); log MUST be .lean-receipts/-comparator-.log (cfgname = path minus .json, '/' -> '_'); log_sha256; result "pass". The log must contain the full line "Your solution is okay!" (both mechanisms; `lake comparator` prints it last, after the per-kernel acceptance lines). A file already at the canonical .lean-receipts path that differs from the receipt being recorded is refused (no silent pointer drift). INDEX ENTRY SCHEMA ("index-entry/2"; "index-entry/1" still validates; YAML keys in this order; unknown keys refused; no local paths) schema name repo(https) pin{commit = the receipts' commit, tag|null} lean_toolchain mathlib_rev|null license_spdx trust(lower-tier|comparator|palomar; computed, never typed) receipts{lower|null, comparator|null} headline[{name, file, summary, judged_as?}] (comparator trust needs every headline judged_as in a config) claims[{id = name/slug-of-decl, decl, kind theorem, summary, judged_as, trust}] (/2 only; derived from headline at add) palomar[{id, version}] doi|null reservoir|null formalization_yaml|null fields[] consent{recorded} added{at, by} notes CLAIMS FILE SCHEMA ("claims/1"; claims.yaml at the package repo root; unknown keys refused; no local paths) schema package claims[{id = package/slug [a-z0-9][a-z0-9-]*, decl, kind definition|lemma|theorem|construction|library, summary, aliases[]?, keywords[]?, file (.lean), status reusable|internal|experimental|superseded, superseded_by|null (required iff superseded; acyclic), citation|null, depends_on[]?, statement_basis? null|as-printed|corrected, manuscript_findings[]? [{id (slug, unique in the package), kind misprint|proof-gap, location{label, tex_line?, page?}, summary, lean_evidence[Lean name (in the claim's file) | {decl, file}] (each must occur at the checked commit, like decl), fixed_in null|arXiv:v}] (exact keys; a misprint needs statement_basis corrected, corrected needs a misprint; findings never change a status), judged_as? null| (theorem/lemma only; one claim per name; replaces the naming rule for that claim; must be a configured theorem_names entry)}]; trust is derived, never typed EXECUTOR EVIDENCE The gate is executor-neutral. The frozen report named by report_sha256 must bind the exact candidate commit/tree, source archive, toolchain/dependency pins, complete checker coverage, terminal state/exit, and executor-specific identity/resource evidence. Slurm reports bind terminal scheduler accounting; hosted reports bind run/attempt/job identity, terminal conclusion, immutable workflow/control revision, runner identity, and resources. A pilot, partial manifest, pre-terminal marker, or prior-candidate receipt is not gate evidence. EVENT LINE SCHEMA (one JSON object per line; package events also go to history[]; index-added, prior-art-searched, registry-* are log-only) ts UTC ISO-8601 with offset, second precision (all written times; dates are UTC; same-second order = file order; naive = legacy UTC, doctor warns) event one of: registry-created, registry-migrated, registered, updated, claimed, claim-refreshed, claim-forced, released, release-forced, lease-expired, gate-passed, regated, promoted, audit-fix, relocated, status-changed, comparator-attached, comparator-replaced, palomar-prepared, index-added, claims-synced, prior-art-searched, evidence-retracted, and the evidence events under `record` name package name or null plus event-specific fields (agent, workspace, ttl_hours, reason, contact, commit, receipt, ...) EXIT CODES 0 success, including dry-runs and the "already gated" no-op 1 refused or validation failed (stderr has the reason; with --json stdout also gets {"ok": false, "error": ...}) 2 usage error (argparse, or an interactive prompt attempted off-tty; with --json a usage refusal, argparse's included, also prints {"ok": false, "error": ..., "usage": true}); what 1 means per command, and comparator-receipt's and lean-exercise's codes: lean-pkg help exit-codes