← Command reference · lean-pkg registry · CLI overview

lean-pkg registry audit

report expired leases, gh visibility, drift; read-only without –write.

Also spelled: lean-pkg audit (all aliases).

Usage

lean-pkg registry audit [--write] [--toolchain-floor VERSION] [--promotion] [--no-gh]
                        [--quiet] [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
--write clear expired leases and update visibility/archive state from gh (old spelling –fix, kept working)
--toolchain-floor VERSION oldest acceptable lean_toolchain (default: $LEAN_PKG_TOOLCHAIN_FLOOR, else leanprover/lean4:v4.35.0-rc2)
--promotion judge every package against the toolchain floor as for promote (warn, not info)
--no-gh skip the GitHub (gh) checks: visibility and archived state are not compared
--quiet only the count line (“N finding(s): W warn, I info”, or “no findings”); no per-finding line (–json is unchanged)

Details

Form What it does Key flags
audit read-only without --fix: report expired leases, GitHub visibility and archived-flag drift, receipt, comparator, toolchain, formalization.yaml drift, toolchain floor (a warning only for public packages, packages with comparator evidence, or under --promotion; else info); every finding has a level (warn or info); informational findings (never fixed): receipt-untracked (a recorded gate or comparator receipt exists in the working tree but is not tracked at the reference branch tip) and duplicate-path (two packages whose local_path resolve to the same checkout) and duplicate-namespace (two checkouts declaring the same Lean root namespace, which cannot be built or imported together; warn naming lean-pkg update NAME --namespace-note TEXT --namespace NS, info with the note once every package sharing it carries one) and consent-duplicate (the same who and role recorded more than once; displayed once, the history keeps every record) and claims-coverage-none (claims coverage is none, empty or unsynced, so search falls back to declarations; --json adds coverage; skips archived and upstreamed; info under --promotion too); palomar-not-ready (warn; only for packages aiming at Palomar: upstream_target: palomar or a recorded palomar entry, and status not scratch, archived or upstreamed): the error gaps palomar check NAME finds at the commit it reads (gate-bound, else HEAD), with their count, codes and the command lean-pkg palomar check NAME; --json adds palomar {errors, codes[], commit, command}; warn gaps alone (submission steps) are no finding; --fix clears expired leases and reconciles visibility/archived from GitHub; human lines are LEVEL CHECK NAME: DETAIL, with “N finding(s): W warn, I info” both first and last (verdict first; the last line is unchanged for scripts); --quiet prints only that line (or no findings), --json unchanged; --json adds counts {warn, info}; a failed gh query is the check gh-missing/gh-not-authenticated/gh-no-access/gh-not-found/gh-error (--no-gh: gh-skipped) [--fix] [--toolchain-floor VERSION] [--promotion] [--no-gh] [--quiet]

JSON output

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

Examples

Report expired leases, receipt and comparator drift and visibility mismatches; read-only.

lean-pkg registry audit

Clear expired leases and copy GitHub’s visibility and archived flag into the registry.

lean-pkg registry audit --write