lean-pkg list

static table, pipe-friendly.

Usage

lean-pkg list [--only NAME[,NAME]] [--fields a,b,c] [--no-claims] [common flags]

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

Arguments and flags

Argument or flag	Description
`--only NAME[,NAME]`	filters PACKAGES, never fields: only these packages (comma-separated names), each with its full record (cached claims included: –no-claims or –fields shrink it); the same table or –json shape, restricted; an unknown name exits 1
`--fields a,b,c`	trims FIELDS, never packages: each package record cut to these keys, comma-separated; the same validation, dotted paths and aliases as `status --fields` (gate.receipt, lease.agent, lease.expires_at; the table columns as aliases: pin, vis, reaudit, expires; an unknown field exits 2 listing the valid keys); –json keeps the dump’s shape plus a `fields` list, text prints the selected keys of each package as YAML
`--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
`list`	static table, script-friendly. `--only` filters packages, never fields: the table or the `--json` dump holds just the named packages, each with its full record, cached claims included (the dump’s shape is unchanged: `version` plus `packages` holding just those records); an unknown name exits 1 like `status`. `--fields` trims fields, never packages: each package record is cut to those keys with the validation and dotted paths of `status --fields` (an unknown field exits 2 listing the valid keys); `--json` keeps the dump’s shape and adds a `fields` list, text mode prints each package’s selected keys as YAML instead of the table. Combine them for one value of one package: `list --json --only NAME --fields status`. `--no-claims` drops the bulk cached arrays, the keys tagged `[bulk]` in Package record (today `claims`), from each record and leaves every other key and the dump’s shape unchanged; `--json` adds an `omitted` list naming them	`--json` `[--only NAME[,NAME]]` `[--fields a,b,c]` `[--no-claims]`

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):

list (exit 0): packages, version

Examples

One line per package, for a terminal or a pipe.

lean-pkg list

Sample output:

NAME      STATUS  VIS      LEASE  EXPIRES  PIN  REAUDIT
my-proof  active  private  -      -        -    -

One value of one package, as JSON for a script.

lean-pkg list --json --only my-proof --fields status