lean-pkg record

record a publication evidence event (consent, Palomar, DOI, Reservoir, Mathlib PR).

Usage

lean-pkg record [--field KEY=VALUE] [--reason REASON] [--doi-track {palomar,doi-only}]
                [--agent AGENT] [common flags] NAME EVENT

[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`
`EVENT`	one of: consent-recorded, palomar-preflight-pass, palomar-submitted, palomar-review, palomar-registered, palomar-withdrawn, doi-minted, reservoir-listed, mathlib-pr-opened, mathlib-pr-merged, or retract (–field event=E –field ts=T –reason TEXT: mark an evidence entry retracted)
`--field KEY=VALUE`	event field (repeatable); required keys per event are listed by `lean-pkg llms`
`--reason REASON`	free-text reason stored with the event
`--doi-track {palomar,doi-only}`	doi-minted only: the DOI track for this event (default: the record’s track, else palomar); doi-only skips rule doi-in-palomar for a public package (old spelling –track, kept working). Choices: `palomar`, `doi-only`.
`--agent AGENT`	the agent acting (recorded as the event’s actor); another agent’s live lease then refuses

Details

Form	What it does	Key flags
`record NAME EVENT`	record a publication evidence event with its required fields: `consent-recorded`, `palomar-preflight-pass`, `palomar-submitted`, `palomar-review`, `palomar-registered`, `palomar-withdrawn`, `doi-minted`, `reservoir-listed` (verified against Reservoir’s package API: a 404 refuses, an unreachable network records `verified: false`), `mathlib-pr-opened`, `mathlib-pr-merged`; each updates the matching v2 field (the `mathlib-pr-` events only append to history) and appends to history. The would-be registry is validated first: an event that introduces a schema error is refused with the rule named and nothing is written (rule doi-in-palomar: a `doi-minted` commit must already be recorded by a `palomar-` event). The DOI-only track skips doi-in-palomar for a package with no Palomar-shaped claim: when the package’s `track` is `doi-only` (set by `update NAME --track doi-only --reason R`) or the command is given `--track doi-only`, `doi-minted` needs no `palomar-` event, but the package must have status `public` (else refused, rule doi-only-public); the history entry and event line carry `track` (`palomar` or `doi-only`), the `doi.versions[]` entry carries `track: doi-only` (so `validate` keeps accepting it if the record’s track later changes), and `--json` adds `track`; `--track` with another event is a usage error (exit 2). Fields are checked first, each refusal naming its rule: `doi` (and `concept`) must look like a DOI, `10.<4-9 digits>/<suffix>` (doi-format); a `mathlib-pr-` `url` must be an `https://github.com/<owner>/<repo>/...` URL (mathlib-pr-url); `palomar-registered` needs status `public` or `upstreamed` (palomar-registered-public) and a `comparator_config` tracked at the package’s HEAD (palomar-config-tracked); a `version` must be an integer, compared as one (`01` is `1`) by `palomar-withdrawn` (palomar-version). A `reservoir-listed` url that names neither the package nor its repository is recorded with a warning (stderr and `notes`); the same `palomar-preflight-pass` commit and run again is a no-op, exit 0 (`"already_recorded": true`), and so is a `consent-recorded` with the same `who`, `role` and `pointer` as a recorded one (a changed pointer is a new record; consent is displayed once per who and role); a field holding a local absolute path (`/home/`, `/Users/`, `~`) is recorded with a stderr WARN and listed in `private_strings`. `record NAME retract --field event=E --field ts=T --reason TEXT` marks an earlier evidence entry retracted, append-only (event `evidence-retracted`); `validate` and the upstreamed check ignore it	`--field KEY=VALUE` (repeatable) `[--reason]` `[--track palomar\|doi-only]` (doi-minted only)

Exit codes

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