← Command reference · lean-pkg claims · CLI overview
lean-pkg claims sync
read claims.yaml at HEAD of the checkout; validate (TODO placeholders refused); cache; event.
Usage
lean-pkg claims sync [--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 |
|
--agent AGENT |
the agent acting (recorded as the event’s actor); another agent’s live lease then refuses |
Details
| Form | What it does | Key flags |
|---|---|---|
claims sync NAME |
read claims.yaml (schema claims/1) at HEAD of the checkout, check every decl occurs in its file (a decl is a dotted Lean name whose components may be «quoted», as in Demo.«foo bar»; its last component, «» kept whole, is looked up), refuse any claim still carrying a claims migrate placeholder (decl: TODO, or a summary starting with TODO), naming the claim, cache the claims and the commit in the registry; event claims-synced; identical re-sync is a no-op; when the pinned commit is on no remote-tracking branch of the checkout (as of its last fetch, so never pushed) both print a stderr WARN naming the commit and the push to make, and --json carries pin_published (true, false, or null without a remote) |
Examples
Read claims.yaml at HEAD of the checkout, validate it and cache the claims in the registry.
lean-pkg claims sync my-proof