← Command reference · CLI overview

lean-pkg next

read-only: the single recommended next command for a package, with a one-line reason (exit 0 a command to run, 1 blocked).

Usage

lean-pkg next [--agent A] [--repo DIR] [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag Description
NAME  
--agent A who is asking: a live lease held by another agent blocks (exit 1); without it a live lease is only noted; also filled into the recommended command
--repo DIR evaluate the checkout DIR instead of the registered local_path, for this call only (never saved; stderr note, JSON repo_override): for a host whose registered path holds another branch. DIR must be a git work tree, and when it has remotes one must be the package’s repo (Host:/p matches a local-path repo /p; the registered local_path itself needs no remote)

Details

Form What it does Key flags
next NAME read-only and offline (no gh call, no network, nothing written): from the registry record and the checkout, the single recommended next command and a one-line reason. In order: terminal status (upstreamed, archived): nothing to do; no checkout: blocked, the update NAME --path DIR --reason .. --dry-run fix of audit’s missing-path; an unparseable lease: blocked, release --force; a live lease held by another agent (with --agent): blocked, never --force; scratch/active without a live lease: claim; claimed scratch: update --status active; claimed active: update --status gate-pending once a lower-tier receipt in .lean-receipts/ binds HEAD (judged by the gate validator), else gate --check --receipt R (produce the receipt first); gate-pending: gate --receipt R [--comparator C] with the receipt found on disk (the reason points to gate --check first), blocked by a dirty tree or a receipt at HEAD that gate would refuse; verified-private: re-gate when the receipt no longer binds HEAD, comparator --receipt for a valid comparator receipt on disk, lean-pkg receipt comparator --project DIR when configs are tracked, comparator config --from-claims (the first of comparator coverage’s next commands) or claims sync when none is, publish --dry-run (then promote) with comparator evidence and the claims ledger ready, else the ledger’s first fix (comparator coverage’s first command when a reusable theorem or lemma is not compared, otherwise claims ledger NAME, and with no claims the reason adds how to write, migrate or sync them), with the reason promote would refuse: claims ledger …; blocked by a dirty tree or an unreadable recorded receipt; public: update --status upstreamed with upstream evidence, the tag command of publish, reservoir check, record consent-recorded / palomar prepare / record palomar-submitted (upstream_target: palomar), record mathlib-pr-opened (mathlib), else nothing. Without --agent a live lease is a note, not a blocker; a checkout on a branch other than its default (origin/HEAD, else main/master) or on a detached HEAD adds the note evaluating branch X, not the default D (evaluating a detached HEAD <sha12>, ...), and HEAD is still what is judged. Exit 0 with a command (or nothing left), 1 blocked, 2 usage; --json: {ok, name, command, reason, blockers[{kind, detail}], notes[], state{status, visibility, lease, gate_commit, comparator_commit, head, checkout, dirty[], receipt_candidate, rejected_receipts[], comparator_configs[], claims_ledger}} (claims_ledger {package_status, counts, required, ledger_digest} once both tiers bind HEAD, else null), blocker kinds foreign-lease, invalid-lease, missing-checkout, no-commit, dirty-tree, invalid-receipt, unreadable-receipt, below-toolchain-floor. A comparator step (lean-pkg receipt comparator, comparator config) is blocked first when the lean-toolchain committed at HEAD (else the registry’s) is below the comparator floor audit checks (--toolchain-floor default, LEAN_PKG_TOOLCHAIN_FLOOR): command null, blocker below-toolchain-floor {detail, lean_toolchain, floor, deferred_command}, and the reason says to bump the toolchain, commit and re-gate (a legacy-mechanism comparator receipt still works below the floor but is not what Palomar runs); attaching a comparator receipt already on disk is not blocked [--agent A] [--repo DIR] (evaluate the checkout DIR instead of the registered local_path, for this one call, as on a host whose registered path holds another branch: never written to the registry; a 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 and the record names a repository one must be it, otherwise the caller vouches for it; a recommended gate --check carries --repo DIR, and any other recommended command that reads the checkout gets a note that it reads the registered path)

Exit codes

0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.

Exit 1 is also a negative answer here:

JSON output

Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):

Examples

The single command to run now for this package, with a one-line reason; exit 1 when it is blocked.

lean-pkg next my-proof

Sample output:

my-proof (active): lean-pkg lease claim my-proof --workspace W --agent A --reason "..."
  why: status active and no live lease: claim the package before working on it

The same as JSON (command, reason, blockers, state) for an agent or a script.

lean-pkg next my-proof --json