← Command reference · lean-pkg comparator · CLI overview

lean-pkg comparator config

write a comparator configuration from claims (–from-claims); coverage and migrate-signoff are verbs of their own.

Usage

lean-pkg comparator config [--from-claims NAME] [--out OUT] [--dry-run]
                           [--challenge-namespace CHALLENGE_NAMESPACE] [--agent AGENT]
                           [--challenge-from-type] [--emit-script F] [--from-output F]
                           [--repo DIR] [--claims-file PATH] [--no-registry]
                           [--allow-partial] [--lake-env DIR] [--jobs JOBS]
                           [--timeout TIMEOUT] [common flags]

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Arguments and flags

Argument or flag	Description
--from-claims NAME	add a TODO theorem_names entry per synced claim (theorem/lemma) no comparator configuration covers yet; never overwrites
--out OUT	the configuration to extend or create (default comparator.json)
--dry-run	print the would-be JSON; write nothing
--challenge-namespace CHALLENGE_NAMESPACE	namespace of the new Challenge names (default <Package>Audit)
--agent AGENT	lease holder, if one is live
--challenge-from-type	pre-fill each new Challenge/Solution from the declaration’s elaborated type (runs lake env lean in the checkout)
--emit-script F	write the type driver to F (run it elsewhere: cd CHECKOUT && bash F OUT.json); no Lean runs here
--from-output F	fill the scaffold from the driver’s comparator-types/1 JSON F
--repo DIR	with –from-claims: use this package checkout instead of the registry’s local_path (HEAD must be the claims-synced commit or an evidence-only descendant) (old spelling –checkout, kept working)
--claims-file PATH	with –from-claims: read the claims from this working-copy claims.yaml instead of the registry’s synced cache (no claims sync needed); schema-checked exactly like claims check --file; never written to the registry; the output names the file and its sha256
--no-registry	with –from-output/–challenge-from-type and –out FILE: scratch mode; write the merged config to FILE outside the checkout, lease not consulted
--allow-partial	with –from-output/–challenge-from-type: ingest a run with extraction failures (the failed entries keep TODO, restatement_reason extraction_failed)
--lake-env DIR	with the type flags: Lake directory inside the checkout (default: the checkout)
--jobs JOBS	with the type flags: parallel Lean processes (default 2, at most the CPUs; halved and retried on too many open files)
--timeout TIMEOUT	with the type flags: seconds per declaration (default 120)

Details

Form	What it does	Key flags
comparator config --from-claims NAME	scaffold comparator entries from the synced claims: one theorem_names entry <Package>Audit.<decl> per theorem/lemma claim (not superseded) that no tracked configuration covers, with a TODO: Challenge and Solution line each under configs[<config>].scaffold.todo in lean-pkg-signoff.json (never in the configuration; one still carrying the deprecated inline lean_pkg_scaffold is refused until migrated); never removes or reorders existing keys or entries; prints already-configured/added/skipped counts; refuses when claims.yaml is not tracked or not synced at HEAD; a foreign live lease refuses the write; the registry is never written; see The comparator tier. --challenge-from-type pre-fills each new entry’s Challenge with the declaration’s elaborated type and its Solution with exact @_root_.<decl> by running lake env lean in the checkout (scratch files in a temp dir); a declaration that fails keeps its TODO: lines with type_error, and needs_restatement: true marks types that use project definitions; each printed type is re-elaborated against the declaration and one that fails keeps its TODO (restatement_reason: round_trip_failed); refuses without a lakefile or with a non-elan lake/lean. Split across hosts: --emit-script F writes the driver (cd CHECKOUT && bash F OUT.json, JSON comparator-types/1), --from-output OUT.json ingests it (refused unless its commit is HEAD, and, unless --allow-partial, when any extraction failed: driver exit 1, or 2 when nothing was filled); --repo DIR (old spelling --checkout DIR) replaces the registry’s local_path (HEAD must be the claims-synced commit or an evidence-only descendant; refusal names the differing paths); --no-registry --out FILE writes the merged configuration to a scratch FILE outside the checkout without consulting the lease and prints what it did not do; --claims-file PATH reads the claims from that working-copy claims.yaml instead of the synced registry cache (no claims sync, so no registry write; checked like claims check --file PATH NAME; never written to the registry; the same configuration as the registry route for the same claims; output line claims source: ... and JSON claims_source {kind, path, sha256, synced_commit, claims}); see Pre-filling statements	[--out comparator.json] [--dry-run] [--challenge-namespace NS] [--agent A] [--challenge-from-type \| --emit-script F \| --from-output F] [--allow-partial] [--repo DIR] [--claims-file PATH] [--no-registry --out FILE] [--lake-env DIR] [--jobs N] (default 2, at most the CPUs; the driver halves it and retries on “too many open files”) [--timeout S] (per declaration, default 120) [--json]

Examples

Print one comparator configuration entry per synced theorem claim that no configuration covers yet.

lean-pkg comparator config --from-claims my-proof --dry-run