← Command reference · lean-pkg comparator · CLI overview
lean-pkg comparator coverage
read-only: the claims covered by the comparator configuration tracked at the gate-bound commit, and why a changed one needs a new gate (comparator config --coverage NAME is the same).
Also spelled: lean-pkg comparator config --coverage NAME (all aliases).
Usage
lean-pkg comparator coverage [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 |
Details
| Form | What it does | Key flags |
|---|---|---|
comparator coverage NAME |
read-only: at the gate-bound commit (the recorded gate receipt’s commit), how many theorem/lemma claims the comparator configuration tracked there covers, does not cover, or lists only as scaffold TODO (definitions and superseded claims are not compared); names any configuration changed since then (working tree, uncommitted, untracked, committed after the gate) with the candidate’s counts shown apart, never substituted; states that a changed or uncommitted config cannot certify the bound tree and a new gate at a commit that tracks it is required; ends with the exact next commands. Exit 0; no gate receipt is a refusal (exit 1) | [--json] (bound_commit, covered, not_covered, todo, uncovered[], config_changed, changed_configs[], candidate, statement, next_commands[]) |
JSON output
Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):
comparator-coverage(exit 0):bound_commit,candidate,changed_configs,claims_source,config_changed,configs,covered,head,hints,judged_as_problems,name,next_commands,not_applicable,not_covered,ok,statement,theorem_claims,todo,uncovered
Examples
Which claims the comparator configuration at the gate-bound commit covers, and which it does not.
lean-pkg comparator coverage my-proof