← Command reference · CLI overview

lean-pkg status

full record + last 5 history entries + scope (gated commit, privacy, the exact comparator-covered declarations).

Usage

lean-pkg status [--fields a,b,c] [--no-claims] [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  
--fields a,b,c trims FIELDS: only these keys of the package record, comma-separated; dotted paths reach into mappings (gate.receipt, lease.agent, the derived lease.expires_at); aliases pin (=mathlib_pin), vis (=visibility), reaudit (=reaudit_after), expires and lease.expires (=lease.expires_at), lease.claimed (=lease.claimed_at), output keeps the record key; –json keeps the nesting, text prints YAML; an unknown field exits 2 listing the valid keys
--no-claims drop the bulk cached arrays (claims; the [bulk] keys below) from each package record; every other key unchanged; –json adds an omitted list

More from –help

package record (the "package" object of status --json, each entry of "packages" in list/board --json; [v2]/[v3]: added by that schema version, [optional]: absent unless set):
  name                  package name; equals its key under packages
  repo                  git URL (or local bare path) of the repository
  local_path            checkout path, $HOME-relative
  visibility            private | public; GitHub is the mirror
  status                lifecycle status: scratch | active | gate-pending | verified-private | public | upstreamed | archived
  owner_project         project that owns the package
  workspace             workspace that registered it
  agent                 agent that registered it
  lease                 live claim {workspace, agent, claimed_at, ttl_hours, reason, contact?} or null; contact: optional address of the holding session (claim/renew --contact); status/list/board output adds the derived expires_at (claimed_at + ttl_hours, UTC; never stored)
  lean_toolchain        lean-toolchain detected in the checkout
  mathlib_pin           Mathlib revision from lake-manifest.json
  upstream_target       upstream goal: none | mathlib | palomar
  automation            automation disclosure (required when upstream_target is mathlib)
  gate                  trust gate {receipt, comparator, axioms_allowed}: receipt paths in the repo
  promoted_at           when promote --yes made it public, or null
  promoted_commit       the commit promoted, or null
  reaudit_after         ISO date after which to re-audit, or null
  notes                 free text
  history               append-only event list (status prints the last 5; --json all)
  license_spdx          SPDX license id or expression, or null [v2]
  formalization_yaml    repo-relative path of formalization.yaml, or null [v2]
  palomar               Palomar evidence entries [{id, version, commit, comparator_config, ...}] [v2]
  doi                   {concept, versions[{doi, tag, commit, minted_at}]} or null [v2]
  reservoir             {listed_at, url} once Reservoir lists it, or null [v2]
  consent               consent records [{who, role, recorded_at, pointer}] [v2]
  claims_file           repo-relative path of the claims/1 file [v3]
  claims                cached claims from the last `claims sync` (can be hundreds of KB) [bulk] [v3]
  claims_synced_commit  40-hex commit the cached claims were read at, or null [v3]
  paper                 {arxiv, status} of the paper behind a paper-coupled package [optional]
  namespace_notes       {Lean root namespace: why sharing it with another package is intended} [optional]
  source_paper          {title, authors[], arxiv, doi} of the formalized paper (credited in formalization.yaml acknowledgements, never as project.authors) [optional]
  ai_assistance         {tools[], roles[]}: AI tools used and for what (rendered into acknowledgements) [optional]
  track                 DOI track: palomar | doi-only (absent = palomar); doi-only lets a public package record doi-minted without a palomar-* event (update --track) [optional]
  docs_descendants      true: a receipt bound to commit C is also accepted at a descendant of C where no build input under the package directory changed (docs-only rule, docs/receipts.md); absent = false (update --accept-docs-descendants) [optional]
  build_inputs          [glob]: extra package-relative paths the docs-only rule treats as build inputs (fnmatch; a glob without / also matches a basename) (update --build-inputs) [optional]
  headline_config       repo-relative path of the headline comparator configuration (the paper's main results; formalization.yaml status.main_results lists its theorems); absent = comparator.headline.json when tracked (update --headline-config) [optional]
  publication_hold      {reason, at, by}: the owner withdrew publication (update --withdraw-publication); promote refuses while it is set; only update --release-publication-hold lifts it [optional]

Details

Form What it does Key flags
status NAME full record plus the last five history entries; a lease that has lapsed ends the output with lease: EXPIRED <age> ago (<agent>); renew no longer works: lean-pkg lease claim ..., one lapsing within 2 h with lease: expires in <time> (<agent>); keep it: lean-pkg lease renew ..., and --json carries lease_state {state: live|expiring|expired|invalid|none, seconds_left} (optional keys such as the DOI track appear when set; --fields track reads it, null when unset); lean-pkg status --help lists the record’s top-level keys (see Package record). --fields a,b,c prints only those keys: dotted paths reach into mappings (gate.receipt, lease.agent, the derived lease.expires_at, the optional lease.contact; through a null lease, or for a lease without a contact, the value is null); the aliases named after the table columns, pin (PIN) for mathlib_pin, vis (VIS) for visibility, reaudit (REAUDIT) for reaudit_after, expires and lease.expires (EXPIRES in list/board/leases) for lease.expires_at, and lease.claimed (the CLAIMED column of leases) for lease.claimed_at, are accepted by status, list and board, and the output and the fields list carry the record key; --json keeps the record’s nesting (package holds just the selected sub-tree, plus an additive fields list), text mode prints them as YAML without the history lines; an unknown field, top-level or nested, is a usage error (exit 2) listing the valid keys at that level. --fields trims fields; --no-claims drops the [bulk] keys (claims) from the record, JSON or text, with every other key unchanged (--json adds an omitted list). Text mode adds a branch: evaluating branch X, not the default D line when the checkout is off its default branch or detached; --json (without --fields) always adds branch: {current, default, detached, is_default} (current null when detached, default null when none can be determined); without --fields, text mode prints a scope: block after the history lines and --json adds 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, or {receipt, readable, commit, mechanism, configs[] {path, theorem_names[], definition_names[]}, 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 (the recorded gate receipt’s), the recorded privacy and publication hold (offline: GitHub is not queried; audit asks gh), the product the page certifies (product: library or paper, read from kind in coverage.yaml committed at HEAD, paper when absent; not declared with the reason when there is no committed or readable file; never the DOI track; see Two tracks), the exact declarations the recorded comparator receipt compared and how many claimed theorem/lemma declarations they cover by the comparator coverage rule (a comparator compares only its theorem_names, never the whole package: compared exactly N declaration(s), not the whole package), and the claims’ counts by status (claim counts: ...; counts, not completion percentages) [--fields a,b,c] [--no-claims]

For the scope: block, --json adds scope.product {kind, source, note}: the product the page certifies (paper or library), read from the committed coverage.yaml at HEAD (kind: paper is the default). With no committed or readable file, the product is null and the output says not declared with a reason; status never refuses. This is separate from the record’s DOI track.

Exit codes

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

JSON output

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

Examples

The full record, the last five history entries and the scope (gated commit, privacy, the comparator-covered declarations).

lean-pkg status my-proof

Only these keys; dotted paths reach into the lease and the gate.

lean-pkg status my-proof --fields status,lease.agent

Sample output:

my-proof:
  status: active
  lease:
    agent: alice