← Command reference · lean-pkg formalization · CLI overview

lean-pkg formalization anchor

bind the companion to one posted arXiv version (writes package files, never the registry).

Usage

lean-pkg formalization anchor [--arxiv ID] [--from-file E-PRINT] [--fetch]
                              [--compare-tex LOCAL.tex] [--accept-diff REASON]
                              [--main-tex PATH] [--write] [--agent AGENT] [common flags]
                              [PACKAGE]

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

lean-pkg formalization anchor NAME --arxiv <id>v<N> (--from-file E-PRINT \| --fetch) [--compare-tex LOCAL.tex [--accept-diff REASON]] [--main-tex PATH] [--write]: bind the companion to one posted arXiv version. Reads the e-print (gzip’d tar, gzip’d .tex or tar; PDF-only is refused) in memory, hashes it and its .tex/.bib/.bbl/.sty files, finds the main .tex (\documentclass), compares it with LOCAL.tex and records it all in data/source-baselines/arXiv-<id>v<N>.json. Without –write: a dry run. –write refuses unless the e-print is tied to the manuscript coverage.yaml is bound to (same version, a matching bound sha256, or –compare-tex identical / –accept-diff); a move to another version prints the claims rebase command. Never writes the registry; never commits

Arguments and flags

Argument or flag Description
PACKAGE the package to anchor
--arxiv ID the arXiv id WITH its version (<id>v<N> or arXiv:<id>v<N>); unversioned ids are refused
--from-file E-PRINT the e-print as downloaded from arxiv.org/e-print/<id>v<N> (offline; no network)
--fetch download the e-print over HTTPS (60 s timeout, 64 MiB cap) and the arXiv API entry of that version; the only network access this command makes
--compare-tex LOCAL.tex compare this local .tex with the e-print’s main .tex (line endings and trailing whitespace normalised); the differing lines are shown
--accept-diff REASON with –compare-tex: anchor although the files differ; the reason is recorded
--main-tex PATH the e-print’s main .tex when more than one file carries \documentclass
--write write the source-baseline record, coverage.yaml manuscript.version and the formalization.yaml source id (never the registry; not committed); without it a dry run
--agent AGENT lease holder, if one is live

Details

Form What it does Key flags
formalization anchor NAME bind the companion to one posted arXiv version: read the e-print (--from-file, offline, or --fetch, the only network access: HTTPS, 60 s timeout, 64 MiB cap) in memory (gzip’d tar, gzip’d single .tex or tar; a PDF-only submission is refused; an absolute, .., link or device member, or the member and size caps, refuse the archive), hash it and each .tex/.bib/.bbl/.sty, find the main .tex (\documentclass; --main-tex when several), compare it with --compare-tex LOCAL.tex (normalised; differing lines shown), and record it deterministically in data/source-baselines/arXiv-<id>v<N>.json (schema source-baseline/1). --arxiv must carry the version. Without --write a dry run (would_write). --write refuses unless the e-print is tied to the manuscript coverage.yaml is bound to (that version already, a bound {sha256} equal to an e-print file, or --compare-tex identical, or differing with --accept-diff REASON, recorded); it writes the record, coverage.yaml manuscript.version and eprint_sha256 (other lines kept) and the formalization.yaml source id; never the registry, never a commit. A move from another version prints rebase_command; see Anchoring to an arXiv version --arxiv <id>v<N> --from-file E-PRINT|--fetch [--compare-tex LOCAL.tex [--accept-diff REASON]] [--main-tex PATH] [--write] [--agent A]

JSON output

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