← Command reference · lean-pkg blueprint · CLI overview

lean-pkg blueprint check

run checkdecls on the blueprint’s declaration list at HEAD and check claims.yaml against it; exit 0 nothing missing / 1; writes nothing.

Usage

lean-pkg blueprint check [--decls PATH] [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
--decls PATH	the declaration list, relative to the checkout (default blueprint/lean_decls, written by leanblueprint)

Details

Form	What it does	Key flags
blueprint check NAME	read-only: the blueprint cross-check. It runs checkdecls (Patrick Massot, Apache-2.0), never a parser of its own: on a clean checkout, lake build, then lake exe checkdecls blueprint/lean_decls (the list leanblueprint writes from the \lean{...} tags); every NAME is missing. line is reported. Then claims.yaml at HEAD: a claim whose decl the blueprint names must be a declaration checkdecls accepts (else a problem); claims outside the blueprint and blueprint names no claim carries are notes. checkdecls must be a dependency in lake-manifest.json at HEAD; without it the command prints the require line to add (lean-pkg never edits the lakefile). A package with no blueprint/ directory and no declaration list is skipped (exit 0). Uncommitted changes to tracked files refuse. Exit 0 nothing missing, 1 a missing name, a claim problem or a refusal; --json: commit, skipped, reason, decls_file, declarations, missing[], checkdecls {rev, url, pinned}, claims {file, present, checked, problems[], outside_blueprint[], blueprint_without_claim[]}. See page: blueprint cross-check	[--decls PATH]

Examples

Run checkdecls on blueprint/lean_decls at HEAD (after lake build) and check that every claim the blueprint names is a declaration checkdecls accepts.

lean-pkg blueprint check my-proof

Sample output:

my-proof: blueprint check at 0123456789ab: FAILED; 2 declaration(s) in blueprint/lean_decls, 1 missing; checkdecls 3d425859e73f
  missing: MyProof.absent_lemma
  claims: 1 claim(s) in claims.yaml name a blueprint declaration
  note: 1 blueprint declaration(s) no claim carries: MyProof.absent_lemma

A blueprint kept elsewhere in the repository; the JSON lists missing[] and the claim cross-check.

lean-pkg blueprint check my-proof --decls docs/blueprint/lean_decls --json