← Command reference · CLI overview

lean-pkg update

set fields of an already-registered package (register is for NEW ones).

Usage

lean-pkg update [--automation AUTOMATION] [--notes TEXT] [--replace-notes]
                [--upstream-target {none,mathlib,palomar}]
                [--doi-track {palomar,doi-only}] [--accept-docs-descendants]
                [--no-accept-docs-descendants] [--build-inputs GLOB,GLOB]
                [--reaudit-after ISO8601] [--owner-project OWNER_PROJECT] [--url URL]
                [--license-spdx SPDX] [--formalization-yaml REL] [--headline-config REL]
                [--paper-arxiv ID] [--paper-status {unpublished,preprint,published}]
                [--source-paper-title TITLE] [--source-paper-author NAME]
                [--source-paper-arxiv ID] [--source-paper-doi DOI] [--ai-tool TOOL]
                [--ai-role ROLE] [--append-note TEXT] [--namespace-note TEXT]
                [--namespace NS]
                [--status {scratch,active,gate-pending,verified-private,public,upstreamed,archived}]
                [--reason REASON] [--redetect] [--agent AGENT] [--force]
                [--path HOME-RELATIVE] [--withdraw-publication]
                [--release-publication-hold] [--dry-run] [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  
--automation AUTOMATION AI-disclosure note; required by mathlib when upstream_target is mathlib
--notes TEXT set the notes; refused when notes exist unless –replace-notes (use –append-note)
--replace-notes with –notes: replace non-empty notes (the old text stays in history as notes_from)
--upstream-target {none,mathlib,palomar} Choices: none, mathlib, palomar.
--doi-track {palomar,doi-only} the DOI track (needs –reason): doi-only lets a public package record doi-minted without a palomar-* event; palomar (the default when absent) keeps rule doi-in-palomar (old spelling –track, kept working). Choices: palomar, doi-only.
--accept-docs-descendants opt in (needs –reason): a receipt bound to commit C is also accepted at a descendant of C where no build input under the package directory changed (*.lean, lakefile.*, lake-manifest.json, lean-toolchain, –build-inputs globs, the checker’s files; never a symlink/gitlink change, .gitattributes, .gitmodules, .lfsconfig, claims.yaml, nor those attribute files in a directory above a subdirectory package); the gated commit stays C (docs/receipts.md); –dry-run supported
--no-accept-docs-descendants opt out again (needs –reason): only the evidence-only rule applies
--build-inputs GLOB,GLOB extra build inputs for the docs-only rule (needs –reason): comma-separated package-relative fnmatch globs (* crosses /; a glob without / also matches a basename), replacing the recorded list; ‘’ clears it
--reaudit-after ISO8601  
--owner-project OWNER_PROJECT  
--url URL remote URL (e.g. after publishing a private dep) (old spelling –repo, kept working)
--license-spdx SPDX the package’s license as an SPDX id or expression, e.g. ‘MIT OR Apache-2.0’ (what the index and Reservoir expect)
--formalization-yaml REL repository-relative path of the package’s formalization.yaml
--headline-config REL repository-relative path of the headline comparator configuration (the paper’s main results, fed to formalization.yaml status.main_results); ‘’ clears it (then comparator.headline.json applies when tracked)
--paper-arxiv ID arXiv id of the paper this package verifies (sets paper.arxiv; status defaults to preprint)
--paper-status {unpublished,preprint,published} the verified paper’s status; promote refuses while unpublished without an arXiv id. Choices: unpublished, preprint, published.
--source-paper-title TITLE title of the formalized paper (source_paper.title; rendered into formalization.yaml acknowledgements, #22.6)
--source-paper-author NAME an author of the formalized paper (repeatable; the list replaces the recorded one). Credited in acknowledgements, never in project.authors; no consent needed
--source-paper-arxiv ID arXiv id of the formalized paper (source_paper.arxiv)
--source-paper-doi DOI DOI of the formalized paper (source_paper.doi)
--ai-tool TOOL an AI tool used (repeatable; the list replaces the recorded one; ai_assistance.tools)
--ai-role ROLE what the AI tools did (repeatable; replaces; ai_assistance.roles)
--append-note TEXT append a line YYYY-MM-DD (AGENT): TEXT (UTC date, –agent) to notes, keeping what is there; –notes replaces instead
--namespace-note TEXT record why this package shares a Lean root namespace with another (namespace_notes); audit’s duplicate-namespace is info once both packages carry a note for it
--namespace NS with –namespace-note: the namespace (repeatable); default every root namespace this checkout shares with another registered package
--status {scratch,active,gate-pending,verified-private,public,upstreamed,archived} manual transitions only; verified-private is gate’s and public is promote’s. Choices: scratch, active, gate-pending, verified-private, public, upstreamed, archived.
--reason REASON required for –status and –force
--redetect re-read lean_toolchain and mathlib_pin from the repo
--agent AGENT lease holder, if one is live
--force override a live lease held by another agent; needs –reason
--path HOME-RELATIVE relocate: move local_path to another checkout, keeping name, history and claims (needs –reason; event relocated; commit-bound evidence not bound to the new HEAD is cleared)
--withdraw-publication the owner made a promoted (public) repository private again: record it (needs –reason; refused while gh still reports it public). status public -> verified-private (active when never gated), visibility private, publication_hold {reason, at, by}; promotion history kept; promote refuses while held; gate/regate keep the hold; –dry-run supported
--release-publication-hold lift a publication hold (needs –reason); status and visibility unchanged; a later public flip still goes through promote
--dry-run with –path, –withdraw-publication or –release-publication-hold: print the would-be changes, write nothing

Details

Form What it does Key flags
update NAME set fields; manual status moves and --force need --reason (else a refusal, exit 1); empty --repo/--owner-project are refused (--notes '' clears); --notes TEXT over non-empty notes is refused (exit 2, nothing written, no event; --json {"ok": false, "usage": true, "error"}) unless --replace-notes is given, and the refusal names --append-note, --replace-notes and the recovery of replaced text from history (the updated event’s notes_from); on empty notes --notes needs no flag; with --replace-notes it replaces the notes, the event carries notes_replaced: true, and, when it drops earlier text, it prints “replaced notes were: …” and “use –append-note to keep the previous note” (JSON hint); --append-note TEXT --agent A appends the line YYYY-MM-DD (A): TEXT (UTC date) to the notes, creating them if absent, and cannot be combined with --notes; its text output prints only appended note: YYYY-MM-DD (A): TEXT (the full before/after stays in the event’s notes_from and in --json changes.notes); --license-spdx takes an SPDX identifier or expression (MIT OR Apache-2.0); --path uses the register normaliser and the current checkout is a no-op (exit 0); public to upstreamed needs a recorded mathlib-pr-merged/palomar-registered event or a URL in --reason; any status may move to archived; a refused move lists the allowed ones; schema errors already in the registry (another package’s) are reported on stderr as pre-existing and do not block (same for register and record) record); --track palomar|doi-only sets the optional DOI track (needs --reason; event updated with track in fields; see record for what doi-only allows; validate refuses any other value); --accept-docs-descendants / --no-accept-docs-descendants set the optional docs_descendants true/false and --build-inputs GLOB,GLOB replaces the optional build_inputs list ('' clears it; package-relative, no leading / or ..): each needs --reason (else refused, nothing written), records event updated with the field in fields and its old value as <field>_from, follows the lease rule, and accepts --dry-run (event update-dry-run, nothing written); see Docs-only descendants --status --reason --automation --notes [--replace-notes] [--append-note TEXT --agent A] --upstream-target --reaudit-after --owner-project --repo --redetect --agent --force [--accept-docs-descendants \| --no-accept-docs-descendants] [--build-inputs GLOB,GLOB] --reason T [--dry-run] [--license-spdx SPDX] [--formalization-yaml REL] [--headline-config REL] (the optional headline_config: the headline configuration; repository-relative .json; '' clears it) [--paper-arxiv ID] [--paper-status unpublished|preprint|published] (the optional paper field of a paper-coupled package; an arXiv id alone sets status preprint) [--source-paper-title T] [--source-paper-author NAME]... [--source-paper-arxiv ID] [--source-paper-doi DOI] (the optional source_paper {title, authors[], arxiv, doi}: the formalized paper, credited in formalization.yaml’s acknowledgements and never in project.authors, so its authors need no consent row; a repeated flag’s list replaces the recorded one, other keys are kept; it needs a title, an arXiv id or a DOI) [--ai-tool T]... [--ai-role R]... (the optional ai_assistance {tools[], roles[]}, rendered into acknowledgements as AI assistance: TOOLS for ROLES.) [--namespace-note TEXT [--namespace NS]...] (records in the optional namespace_notes why this package shares a Lean root namespace with another, such as a comparator Challenge/Solution layout; without --namespace, every root namespace the checkout shares with another registered package; notes for other namespaces are kept; audit’s duplicate-namespace becomes info once every package sharing the namespace carries a note for it) [--path HOME-RELATIVE --reason TEXT [--dry-run]] (relocate: event relocated; the output ends with a binding at the new path block: each recorded receipt’s commit against the new HEAD with the evidence-only verdict, the formalization.yaml exception (pointer, changed, derived-only), other changes since the receipt commit, then next: with the command(s) to run, such as lean-pkg gate NAME --receipt R [--refresh-formalization], lean-pkg update NAME --formalization-yaml REL when only a missing pointer clears a derived-only regeneration, lean-pkg receipt comparator + lean-pkg comparator, claims sync, or nothing to re-gate; JSON binding {head, receipt, comparator, formalization, other_changes} and next_commands[]) [--withdraw-publication --reason TEXT [--dry-run]] (privacy withdrawal: the owner made a promoted repository private again; on its own, public status only (an upstreamed one is withdrawn upstream), refused while gh still reports the repository public (lean-pkg never changes visibility here; a failed or non-GitHub query is noted, not a refusal); status public -> verified-private (active when no gate receipt is recorded), visibility: private, and publication_hold {reason, at, by} (by: --agent, else unknown); promoted_at, promoted_commit and the promoted event are kept; one publication-withdrawn event {status_from, status_to, visibility_from, visibility_to, reason, by, github_visibility, promoted_commit, forced}; while held, promote (and the promote checklist of publish) fails with ✗ publication hold since AT by BY: REASON, next recommends nothing to publish, gate/--regate keep the hold, audit --fix never flips a held record public; see Lifecycle) [--release-publication-hold --reason TEXT [--dry-run]] (lift the hold: status and visibility unchanged, event publication-hold-released {reason, hold, by, forced}; a public flip still goes through promote)

Exit codes

0 success (dry runs and no-ops included), 1 refused or failed, 2 usage error; see Exit codes.

JSON output

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

Examples

Set a field of a registered package (register is only for new ones).

lean-pkg update my-proof --license-spdx Apache-2.0