← Command reference · lean-pkg claims · CLI overview

lean-pkg claims rebase

move claims.yaml and coverage.yaml to a new manuscript version: carry unchanged statements re-keyed from the new .aux, list the rest for review; writes only –out-dir; never changes a status.

Usage

lean-pkg claims rebase --from-tex OLD.tex --to-tex NEW.tex --to-aux NEW.aux
                       [--from-aux OLD.aux] [--from-sha256 HEX]
                       [--to-version arXiv:IDvN] [--to-commit HEX] [--to-repo URL]
                       [--unwrap-macro NAME] [--claims-file PATH] [--coverage-file PATH]
                       [--out-dir DIR] [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-tex OLD.tex the (flattened) TeX the claims were written against; its SHA-256 must match coverage.yaml’s manuscript sha256 (an arXiv version: a .tex of its source-baseline record), or –from-sha256 when none is recorded. Required.
--to-tex NEW.tex the new version’s (flattened) TeX. Required.
--to-aux NEW.aux the .aux of a full build of NEW.tex: new numbers and pages come from it. Required.
--from-aux OLD.aux the old .aux: resolves references written as numbers (Lemma 4.2, (3.7)) to TeX labels
--from-sha256 HEX the SHA-256 of OLD.tex, required when coverage.yaml records none (checked, never trusted)
--to-version arXiv:IDvN the new manuscript.version for the proposed coverage.yaml
--to-commit HEX or: the manuscript repo commit of NEW.tex (sha256 is NEW.tex’s)
--to-repo URL with –to-commit: the manuscript repo (default: coverage.yaml’s)
--unwrap-macro NAME also read \NAME{X} as X (a revision-highlight macro); repeatable
--claims-file PATH a working-copy claims file instead of the one committed at HEAD
--coverage-file PATH a working-copy coverage file instead of coverage.yaml committed at HEAD
--out-dir DIR write the proposals, the report and the review packet here (a new or empty directory); without it nothing is written

Details

Form What it does Key flags
claims rebase NAME --from-tex OLD.tex --to-tex NEW.tex --to-aux NEW.aux move claims.yaml and coverage.yaml (committed at HEAD) to a new manuscript version (#6); never writes the registry or the checkout, never changes a claim status, never sets fixed_in. Refused (exit 1): OLD.tex’s SHA-256 differs from the manuscript sha256 coverage.yaml records, or is none of the .tex hashes of the source-baseline record of its arXiv version (formalization anchor; none recorded: --from-sha256 must state it; the proposal drops manuscript.eprint_sha256), TeX that is not UTF-8 or has unbalanced environments, a referenced label defined twice in OLD.tex, NEW.tex or NEW.aux. Each referenced label (coverage paper.label, else paper.number via --from-aux; a finding’s location.label; a label in a citation) is classified by its statement or equation environment, compared after a fixed normalization: unchanged (carried; number, page and line re-keyed from NEW.aux), changed, missing, moved-into-proof, not-in-old, unsupported, unnumbered; all but unchanged need review and stay as they were. --out-dir DIR (new or empty) gets the proposed claims.yaml and coverage.yaml, rebase-report.json (claims-rebase/1) and .md with old/new excerpts, review/ excerpts and diffs, and MANIFEST.sha256; deterministic; without it nothing is written. Exit 0 all carried, 1 review needed or refused, 2 usage; --json {ok, counts, labels[], rows[], findings[], citations[], needs_review[], proposed_errors[], files[], …}. Move to a new manuscript version [--from-aux OLD.aux] [--from-sha256 HEX] [--to-version arXiv:IDvN \| --to-commit HEX [--to-repo URL]] [--unwrap-macro NAME ...] [--claims-file PATH] [--coverage-file PATH] [--out-dir DIR] [--json]

JSON output

Top-level keys of --json, as recorded in the golden contract (tests/golden/json-keys.json):