← Command reference · lean-pkg claims · CLI overview

lean-pkg claims migrate

legacy claims.json -> a claims/1 skeleton in the checkout (never the registry).

Usage

lean-pkg claims migrate --from PATH [--out OUT] [--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 PATH	the legacy JSON (relative paths are read from the checkout). Required.
--out OUT	repo-relative output (default: claims_file, else claims.yaml)
--dry-run	print the skeleton; write nothing
--agent AGENT	your lease agent, when the package is leased

Details

Form	What it does	Key flags
claims migrate NAME --from PATH	convert a legacy claims JSON (a list of rows, rows under claims/rows/items/entries, or a mapping id to row; PATH relative to the checkout) into a claims/1 skeleton in the checkout: mapped fields are copied (claim_id/id, lean_decl/decl, statement/summary, lean_file/file, type/kind, paper_ref/citation, tags/keywords, depends_on), the rest get TODO markers (decl: TODO, summary: TODO: ..., file: TODO.lean, each of which claims sync refuses) listed in a comment header with any unmapped keys. Never overwrites, never writes the registry or the event log, and grants no verification: commit the finished file, then claims sync	[--out claims.yaml] [--dry-run] [--agent A] [--json]