← Command reference · lean-pkg coverage · CLI overview
lean-pkg coverage check
validate coverage.yaml against claims.yaml and the receipts at HEAD; exit 0/1; read-only.
Usage
lean-pkg coverage check [--file PATH] [--allow-private-manuscript] [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 |
|
--file PATH |
check this working-copy file instead of coverage.yaml committed at HEAD (claim ids and receipts are still read at HEAD) |
--allow-private-manuscript |
accept manuscript.version ‘unposted’ (a private draft); the output says so |
Details
| Form | What it does | Key flags |
|---|---|---|
coverage check NAME |
read-only: validate coverage.yaml (schema coverage/1, committed at HEAD; --file PATH checks a working copy) against claims.yaml and the receipts at HEAD: exact key sets, closed enums (same-assumptions, inputs-supplied, outside; cluster easley), duplicate keys refused, claim ids that exist and are not superseded, inputs for every inputs-supplied row, at least one outside row or nothing_excluded: {reason}, a posted manuscript version (arXiv:IDvN or {repo, commit, sha256}; unposted only with --allow-private-manuscript), every compute job a committed Slurm receipt; the lab’s lean-scope-page rules that apply: no placeholder text (FILL-ME, TODO, TBD, FIXME, XXX), every named claim’s file committed at HEAD, every theorem of the recorded comparator receipt the declaration of a claim some row names, every configuration there with definition_names carrying judged_as.reviewer; kind: library (no manuscript; rows {title, claims, note?}, the library’s main results; manuscript, nothing_excluded and paper row keys refused); exit 0 or 1; --json {ok, name, file, kind, rows, counts, manuscript, private_manuscript, errors[], warnings[]} (manuscript and counts null for a library) (The verification page) |
[--file PATH] [--allow-private-manuscript] |
JSON output
Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):
coverage-check(exit 0):counts,errors,file,kind,manuscript,name,ok,private_manuscript,rows,warnings
Examples
Validate coverage.yaml committed at HEAD (the paper-to-Lean map that page renders).
lean-pkg coverage check my-proof
Check the working copy before committing it.
lean-pkg coverage check my-proof --file coverage.yaml