← Command reference · CLI overview

lean-pkg doctor

installation, registry, index and tool diagnostics; exit 1 when the registry is unreadable or its schema version is unsupported.

Usage

lean-pkg doctor [--fetch] [--upgrade-from OLD] [--to NEW] [--source 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 also check this package’s committed lean-toolchain, Mathlib commit (lake-manifest.json) and recorded comparator receipt’s tool digests against the LTS stack its coverage.yaml declares (stack: NAME; docs/stacks/): a warn line on a mismatch or a stack past its window, never an exit 1
--fetch git fetch origin in the tool checkout and the registry repo before comparing (default: local refs)
--upgrade-from OLD instead of the diagnostics: what changed for a package author since OLD (a version, 0.9.0 / v0.9.0, or any commit of the lean-pkg repository): formats, on-disk keys, commands, flags, –json keys, aliases, Python floor, packaged files, and the curated behaviour changes of docs/upgrades/; read-only (docs/design/upgrade-preflight.md)
--to NEW with –upgrade-from: the newer version or commit (default HEAD of the source)
--source DIR with –upgrade-from: the lean-pkg git checkout to read both trees from (default: the checkout this lean-pkg runs from)

Details

Form What it does Key flags
doctor one ok/warn/n/a line each: version; install kind and path (an editable install inside a git checkout adds its short HEAD, branch, and behind/ahead counts against origin/<branch>, from local refs unless --fetch); registry path and schema version, ending [source: flag|env|user-default|cwd] (doctor --json adds "source" to that check); user-default: what ~/.lean-pkg/registry points at (ok) or n/a when it is not set up; events path, ending [source: flag|registry-sibling|env|sibling]; registry-repo: the git work tree holding the registry with its HEAD, branch, behind/ahead of origin/<branch> (or “no origin remote” when there is none) and uncommitted tracked files, naming the registry files among them (warn when behind, ahead, detached, or the registry files are uncommitted: do not write from there yet; n/a outside a work tree); leases: live count, leases lapsing within 2 h and expired-but-unswept ones by name, and leases whose fields cannot be parsed (warn when any is non-empty); time: naive (offset-less, legacy) lease claimed_at / history ts values, read as UTC (warn when any); index path and entry count, ending [source: flag|env|registry-sibling|cwd]; host: the comparator host-check verdict (warn when this host cannot produce comparator receipts); lake, lean, elan, git, gh, reuse, bwrap, comparator, nanoda, go, cargo, jq on PATH (an n/a tool line says what the tool is for and when it is needed, so a host that only reads the registry still has a clean doctor: comparator, nanoda, bwrap, go, cargo and jq only produce comparator receipts on this host, go, cargo and jq being what lean-pkg receipt comparator needs to build the legacy comparator tools; reuse is the release gate’s REUSE lint only; gh serves promote, audit and reservoir check; a lake or lean that is not elan’s proxy in $ELAN_HOME/bin, default ~/.elan/bin, is a warn, since it ignores each project’s lean-toolchain; without bwrap, the tool comparator line adds “run lean-pkg comparator host-check to see whether this host can produce receipts”, see which hosts can produce receipts); gh auth: the github.com account from gh auth status (warn when gh is present but not logged in, since promote and audit need it; n/a without gh); Python version. A check that raises prints warn <item>: internal error ... and the others still run. stack: the declared LTS stacks and the current one (n/a). Exit 1 when the registry is unreadable or its schema version is unsupported (a missing registry counts as unreadable), else 0 [--fetch]
doctor NAME the checks above, and the stack line for package NAME: its committed lean-toolchain, the Mathlib commit of its lake-manifest.json (against the stack’s commit, not only the tag name, since a tag can be moved) and the tool digests of its recorded comparator receipt (gate.comparator, against the stack’s Linux x86_64 digests), compared with the stack its coverage.yaml declares (stack: NAME). ok: on stack NAME (supported until DATE); warn: a difference, a stack past its window, a stack this lean-pkg does not declare, or a lean-pkg outside the stack’s range; n/a: no stack: key. Never an exit 1 (proposal 0004: doctor and verify “never refuse”). --json adds stack {name, declared, matches, supported_until, window, toolchain, mathlib, comparator_tools, lean_pkg, mismatches[], warnings[]}, null without NAME or the key NAME [--fetch]
doctor --upgrade-from OLD instead of the checks above, the upgrade preflight: what changed for a package author between two lean-pkg versions or commits (even when the version string is unchanged), read from a lean-pkg git checkout’s objects and never by running the old code. Mechanical: requires-python, dependencies, executables, format markers (every x/N constant, the registry version, the formalization.yaml version), the on-disk key lists (registry package and lease, lower-tier and comparator receipts, formalization.yaml’s derived keys), command paths and options from the help goldens (a renamed command or flag whose old spelling is an alias is renamed, not removed), the --json key sets, the alias tables and the packaged data files. Curated: the entries of docs/upgrades/<version>.yaml whose pull request lies in OLD..NEW (behavior[], breaking[]), and the range’s pull requests no record names (uncurated[]). OLD and NEW are a version (0.10.0: tag v0.10.0, else the release: 0.10.0 commit) or any revision; --json schema lean-pkg-upgrade/1; read-only, no registry, no network; see the design and the 0.11.0 notes --upgrade-from OLD [--to NEW] [--source DIR]

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

Check the installation, the registry, the index and the tools in one line each; exit 1 when the registry is unreadable or its schema version is unsupported.

lean-pkg doctor