← Command reference · lean-pkg claims · CLI overview

lean-pkg claims mark

set the status of the claims a comparator config’s theorem_names cover (exact full-name match); read-only unless –write; never commits.

Usage

lean-pkg claims mark --from-comparator CONFIG.json
                     --status {reusable,internal,experimental} [--write] [--dry-run]
                     [--agent AGENT] [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
--from-comparator CONFIG.json	the comparator configuration whose theorem_names select the claims (relative paths are read from the checkout). Required.
--status {reusable,internal,experimental}	the status to set. Required. Choices: reusable, internal, experimental.
--write	edit the claims file in the checkout (only the status values; never committed)
--dry-run	print the changes; write nothing (the default)
--agent AGENT	with –write: the lease holder, when the package is leased

Details

Form	What it does	Key flags
claims mark NAME	set status on exactly the claims whose decl a comparator configuration’s theorem_names cover (the comparator coverage and ledger rule: the full name, or <Prefix>.<decl>, of a fully qualified decl; a shared last component never matches), in the checkout’s working copy of the claims file; read-only unless --write (the default prints the plan); --write edits only the changed status: values (comments and layout kept; when that is impossible the file is re-dumped and the output says so), validates the result against claims/1, never commits and never writes the registry; another agent’s live lease refuses --write; configuration names that cover no claim are listed (unmatched theorem name: ...), followed by the rule (rule: ...) and a hint: for each name that differs from exactly one claim’s decl only in its leading namespace component (never applied; docs/comparator.md#how-a-theorem-name-maps-to-a-claim); next: commit, claims sync, re-gate. claims sync and claims check print WARN NAME: gated, N claim(s), none with status reusable: ... (JSON warnings[]) for a gated package with claims and none reusable, and the ledger’s unknown reason names this fix. --json {ok, name, file, config, status, matched[] {id, decl, from, to, changed}, changed, unmatched[], written, reformatted, rule, hints[] {name, decl, shape, rename_to, hint}}	--from-comparator CONFIG.json --status reusable\|internal\|experimental [--write \| --dry-run] [--agent A] [--json]