Proposal: the 1.0 command tree and format freeze

Status: accepted 2026-10-17 by Le Chen: all five decisions of section 8 and the smaller choices, as proposed. Implementation runs in stages:

Date of the proposal: 2026-10-17. Removing or renaming a command was the maintainer’s decision; this page lays out the options, the evidence and the recommendation the decision accepted.

Scope: roadmap wave 2, “Simplify to 1.0”. It covers the command and flag inventory, real usage, a proposed 1.0 tree with a migration and deprecation policy, and the on-disk format inventory against the 1.0.0 criteria in RELEASING.md. It does not design lean-pkg new (wave 1) or CI-runner receipts (wave 3); where the tree depends on them it says so.

Summary

1. Method and evidence

Source What it measures Caveat
The argparse tree, walked in-process from lean_pkg.cli.main every command, alias and option comparator config, comparator host-check and formalization anchor are values of a positional, found in the code, not the parser. Option totals exclude the 8 global flags; per-command counts in section 2 include the global flags a command repeats
tests/golden/help/*.txt (53 files) and tests/golden/json-keys.json (38 key sets) the public contract as tested today  
Docs references: lean-pkg <command> in README.md, docs/**/*.md and docs/llms.txt how prominent a command is in the story regex count; a subcommand is also counted under its parent noun
Test references: argv lists and lean-pkg <command> strings in tests/**/*.py how much of the suite pins a command regex count; the lease alias collides with the lease record key and is not counted
The lab registry event log, a read-only copy, 2026-09-19 to 2026-10-17 (619 events, 41 packages, 57 distinct actor strings) which write commands real agents ran records writes only: read-only commands leave no event
Shell commands in agent session transcripts on one lab host, last 30 days (298 sessions mention lean-pkg) read-only commands too one host of several; “maintainer” sessions are those working in the lean-pkg repository itself, “lab” the rest

The event log starts on 2026-09-19, so “last 30 days” is the whole log.

2. Inventory: commands today

Personas: N newcomer (one package, own machine), A package author (several packages, publishes), L lab operator or agent (shared registry, leases, cluster), M maintainer of lean-pkg or of the public index.

Columns: docs and test reference counts; shell invocations in transcripts (all / lab sessions only); registry events in 30 days, mapped from event names to the command that writes them.

Registry and package record

Command Purpose Persona Docs Tests Shell all / lab Events 30d Overlaps
board (also no argument) curses TUI on a tty, static table otherwise L 3 25 14 / 13 0 list (same table)
list static package table A, L 4 72 17 / 3 0 board
status NAME full record, history, scope N, A, L 12 338 80 / 13 0 next (its last line), claims ledger
init create an empty registry and event log A, L 10 47 20 / 1 1 new (wave 1) will need an implicit init
migrate upgrade the registry schema L, M 7 29 26 / 24 2 claims migrate, index migrate, comparator config --migrate-signoff
register NAME the only write path for a new package A, L 11 19 22 / 11 34 new (wave 1)
update NAME set fields of a registered package (39 options) A, L 38 102 114 / 39 199 record (events), release --fresh-repo (relocation)
record NAME EVENT record publication evidence (consent, Palomar, DOI, Reservoir, Mathlib PR) A, M 5 40 13 / 10 8 update
validate registry schema and history sanity L, M 2 51 28 / 15 0 doctor, audit
audit expired leases, gh visibility, drift; --fix writes L 6 59 35 / 22 4 validate, doctor
wiki Markdown status page of the registry L 2 11 13 / 10 0 index render, list

update events include relocated (18, from update --path or a release --fresh-repo/--adopt-repo) and status-changed (9).

Leases (multi-agent coordination)

Command Purpose Persona Docs Tests Shell all / lab Events 30d Overlaps
claim NAME (alias lease) CAS lease, 24 h TTL L 18 70 36 / 17 90 renew (a re-claim by the holder also refreshes)
renew NAME restart one’s own live lease L 5 31 6 / 0 31 claim
release NAME release a lease; with --fresh-repo/--adopt-repo, export or adopt a repository L, A 14 69 23 / 5 66 two unrelated jobs under one name; “release” also reads as “publish a version”
leases held leases, soonest expiry first L 5 27 6 / 0 0 list --fields lease..., audit

Evidence: receipts, gate, comparator, claims, coverage

Command Purpose Persona Docs Tests Shell all / lab Events 30d Overlaps
receipt slurm lower-tier receipt from a finished Slurm job (24 options) L, A 13 39 56 / 0 0 receipt systemd (13 shared options)
receipt systemd (alias local) the same from a systemd user unit, optionally run bounded N, A 7 7 13 / 0 0 receipt slurm
comparator-receipt (own executable) run the comparator and write the comparator receipt N, A, L many many 350 / 106 0 not a subcommand of receipt
gate NAME validate receipts; gate-pending to verified-private; --check, --regate N, A, L 21 216 90 / 24 91 comparator NAME --check
comparator NAME attach (--receipt) or check (--check) a comparator receipt A, L 57* 174* 59 / 31 3 gate --comparator attaches too
comparator config ... write a comparator configuration from claims, --coverage, --migrate-signoff A, L 17 32 23 / 0 0 a positional keyword, not a subparser; flags of all modes share one usage line
comparator host-check can this host run the comparator; --routes N, A, L 16 15 22 / 0 0 doctor (reports the same verdict)
claims sync read claims.yaml at HEAD, validate, cache A, L 7 41 21 / 9 66 gate checks the same file
claims list table of cached claims A 2 10 3 / 3 0 status (counts)
claims check re-validate cached claims, or --file A, L 8 26 24 / 1 0 gate --check
claims ledger per-claim closure from the evidence A, L 8 13 29 / 0 0 status, page
claims mark set claim statuses from a comparator config A 2 5 5 / 0 0  
claims rebase move claims and coverage to a new manuscript version A 4 6 9 / 0 0  
claims migrate legacy claims.json to claims/1 A 3 3 0 / 0 0 the other migrates
coverage check validate coverage.yaml N, A 5 9 20 / 0 0 page --check runs the same checks

* comparator counts include comparator config and comparator host-check. n/c: not counted in the transcript pass (the row was added after it).

Publication

Command Purpose Persona Docs Tests Shell all / lab Events 30d Overlaps
page NAME the README verification section; --check, --site, --html N, A 23 62 68 / 0 0  
publish NAME --dry-run read-only checklist from verified-private to listed N, A 4 26 4 / 0 0 promote (dry run by default), next
promote NAME [--yes] promotion checklist; --yes flips the GitHub repo public A, L 9 48 29 / 18 3 publish
public-safety NAME scan tree and history for private patterns A, L, M 13 71 16 / 0 0 run by promote
formalization NAME render formalization.yaml (v0.4) A 23 53 26 / 0 0 palomar prepare renders it too
formalization anchor NAME --arxiv IDvN pin the companion to one arXiv version; writes coverage.yaml, formalization.yaml and a source baseline A (paper track) 7 28 n/c 0 a positional keyword of formalization, like comparator config; claims rebase moves to a new version
palomar check / prepare / port-modules Palomar readiness, bundle, module-system port A 10 / 3 / 4 21 / 17 / 13 21 / 5 / 10 0 gate --check prints the Palomar gaps
reservoir check would Reservoir list this package A 3 5 0 / 0 0  
index add / check / render / migrate the public catalog M 5 / 6 / 3 / 1 14 / 11 / 8 / 9 28 / 22 / 26 / 3 10 wiki (another renderer)
search TERM prior-art search over claims, the index and public sources N, A, L 21 20 43 / 26 11  

Help and support

Command Purpose Persona Docs Tests Shell all / lab Events 30d Overlaps
next NAME the one recommended next command N, A, L 6 32 21 / 0 0 status, publish --dry-run
doctor installation, registry, tools N, A, L 8 27 28 / 5 0 comparator host-check, validate
help [TOPIC] topics and per-command help N, A 14 23 35 / 0 0 llms, --help
llms [--short] the agent usage contract (about 10,500 words) L 11 17 49 / 16 0 help
report redacted bug report, filed with --yes all 6 14 31 / 0 0  
--version version and build all     88 / 9    

Other executables

Executable Purpose Shell all / lab Note
comparator-receipt the comparator run and its receipt 350 / 106 the most-run program of the package
lean-exercise check judge an exercise Solution against a Challenge 60 / 0 separate audience (teaching)
lean-pkg-extract plan plan a public repository extracted from a mixed one 0 / 0 new in 0.9.0

Flags

3. Usage evidence, last 30 days

Registry write events (whole log, 2026-09-19 to 2026-10-17)

Command Events Event names
update 199 updated 172, relocated 18, status-changed 9
gate 91 gate-passed 56, regated 35
claim 90 claimed 89, claim-forced 1
claims sync 66 claims-synced
release 66 released 64, release-forced 2
register 34 registered
renew (or a re-claim) 31 claim-refreshed
search --record 11 prior-art-searched
index add 10 index-added
record 8 consent-recorded
audit --fix 4 lease-expired 3, audit-fix 1
promote --yes 3 promoted
comparator (attach) 3 comparator-attached
migrate 2 registry-migrated
init 1 registry-created

363 of the 619 events fall in the last 7 days. Six commands (update, gate, claim, claims sync, release, register) produce 546 of 619 events (88%); with renew, 93%.

Shell invocations (one lab host, 30 days)

Top ten across all sessions: comparator-receipt 350, update 114, gate 90, --version 88, status 80, page 68, lean-exercise 60, comparator 59, receipt slurm 56, llms 49. In lab sessions (not working on lean-pkg itself): comparator-receipt 106, update 39, comparator 31, search 26, gate 24, migrate 24, audit 22, index add 20, promote 18, claim 17.

Never or almost never typed in 30 days: reservoir check (0), claims migrate (0), receipt local (0), lean-pkg-extract (0, new), claims list (3), index migrate (3), publish (4), the lease alias (4), claims mark (5), palomar prepare (5), renew and leases (6 each).

What the evidence says

  1. The lease commands are heavily used, but only by agents sharing one registry. A newcomer with one package never needs them.
  2. update is the workhorse (199 events): it is the de facto “edit the record” verb, and its 39 options are where field reports have landed.
  3. comparator-receipt is the most-run program and is not a lean-pkg subcommand, so the main tool’s help never shows the step people run most.
  4. publish (the read-only checklist) is almost unused; promote is what people run. The newcomer-facing name is the unused one.
  5. Readiness checks (reservoir check, palomar check, public-safety, coverage check, claims check) are run by humans rarely; they matter as steps inside gate --check, page --check and promote.

4. Proposed 1.0 command tree

Principles

  1. The package is the implied noun. A top-level verb acts on one package (lean-pkg status NAME), as in cargo or npm. Every other object gets a noun with verbs (lean-pkg lease claim NAME, lean-pkg receipt slurm). This is how the 1.0 criterion “commands are grouped as noun-verb pairs” is met without writing lean-pkg package status.
  2. A noun alone is read-only. lean-pkg claims NAME lists, lean-pkg comparator NAME checks; anything that writes has an explicit verb.
  3. One name, one job. No command changes jobs with a flag (release --fresh-repo) or a positional keyword (comparator config).
  4. Old spellings never break. Each current spelling becomes a permanent alias, pinned by an ARGV_TABLE row; aliases are left out of the first page of --help and listed by lean-pkg help aliases.
  5. Help in tiers. lean-pkg --help shows the five newcomer verbs and one line pointing at lean-pkg help all; the full tree is grouped as below.

Tier 1: newcomer (five verbs)

1.0 command Today What it does
new DIR / new --adopt DIR (wave 1, stream A) register, plus init when no registry exists scaffold or adopt a Lean project, create the default registry when none exists, register the package
verify NAME receipt systemd --run, comparator-receipt, gate (three programs, about 25 flags) run the local lower-tier receipt, the comparator receipt, and the gate, printing each step and the exact command it ran; refuses where any of them would, with the same messages. A wrapper only: it writes the same receipts and events as the three steps run by hand. The CI-runner route (wave 3) plugs in here
status NAME status, ending with next’s recommendation unchanged, plus a next: line
page NAME page unchanged
publish NAME publish --dry-run (checklist) and promote (dry run; --yes publishes) checklist by default; --yes does what promote --yes does today

Helpers always visible: doctor, help.

Two product tracks on the newcomer page

There are two kinds of final product, and the newcomer page shows a path for each. Both share the five verbs; they differ in what page maps (the kind of coverage.yaml, paper or library, already in coverage/1 since 0.9.0) and in what follows publish.

Step Track P: the paper is the product Track L: the Lean package is the product
Start new DIR (kind paper) new DIR --kind library, or new --adopt DIR for an existing repository
Bind the source formalization anchor NAME --arxiv IDvN; claims rebase for a new version none: the rows are the library’s main results
Verify verify NAME verify NAME
Page page NAME --write: the paper-Lean map, Not formalized page NAME --write: Main results, no manuscript
Publish publish NAME --yes (public repository, cited from the paper) publish NAME --yes (public repository)
After palomar prepare and record palomar-*; record doi-minted public repository: index add, reservoir check, record reservoir-listed, record doi-minted --track doi-only. Mathlib: update --upstream-target mathlib --automation T, record mathlib-pr-opened and mathlib-pr-merged, then update --status upstreamed

Three consequences for the tree:

  1. The selector is --kind, not --track. --track already exists on record and update with another meaning (the DOI track, palomar or doi-only). new --kind paper|library writes the same kind key that coverage.yaml carries, so one word names the product everywhere. Renaming the DOI --track (to --doi-track, old spelling an alias) would remove the remaining ambiguity; it is listed under the smaller decisions.
  2. lean-pkg help paper and lean-pkg help library become help topics, each printing its column above with the exact commands, beside the existing environment, exit-codes and formatting topics. The first page of --help names both in one line each.
  3. The Mathlib route records evidence; it does not prepare the PR. lean-pkg has no verb that checks a Mathlib contribution against Mathlib’s conventions (naming, docstrings, no sorry, the AI-disclosure note). That is a gap for track L, not a tree question: a future mathlib check NAME (read-only, like reservoir check) would sit in tier 2 beside palomar check, and does not change any name proposed here.

Tier 2: package author

1.0 command Today Decision
register NAME register keep
update NAME update keep; --path moves to repo move (alias kept)
record NAME EVENT record keep
gate NAME gate keep (advanced; verify calls it)
next NAME next keep (also printed by status)
list list keep
search TERM search keep
receipt slurm / receipt systemd the same keep; receipt local stays an alias
receipt comparator comparator-receipt (executable) new spelling that runs the same code; the executable stays
comparator attach NAME --receipt R comparator NAME --receipt R merge into a noun; old form a permanent alias
comparator NAME / comparator check NAME comparator NAME --check read-only default
comparator config NAME comparator config --from-claims NAME becomes a real subparser with only its flags
comparator coverage NAME comparator config --coverage NAME split out (read-only)
comparator host-check the same becomes a real subparser
comparator migrate-signoff PATH comparator config --migrate-signoff PATH split out
claims sync / list / check / ledger / mark / rebase the same keep; claims NAME alone lists
claims migrate the same keep as a format migration (see section 6)
coverage check the same keep
formalization NAME the same keep
formalization anchor NAME the same (a positional keyword today) becomes a real subparser with only its flags
palomar check / prepare / port-modules the same keep
reservoir check the same keep (rare, but cheap and it is the only Reservoir entry point)
public-safety NAME the same keep
report the same keep

Tier 3: coordination and maintenance

1.0 command Today Decision
lease claim NAME claim, lease move; both old spellings are permanent aliases
lease renew NAME renew move; alias
lease release NAME release NAME (no export flag) move; alias
lease list leases move; alias
repo export NAME DIR release NAME --fresh-repo DIR split out; the old form stays as an alias
repo adopt NAME DIR release NAME --adopt-repo DIR split out; alias
repo move NAME PATH update NAME --path PATH split out; alias
registry init init move; alias. new calls it when needed
registry migrate migrate move; alias
registry validate validate move; alias
registry audit [--fix] audit move; alias
registry board board, and lean-pkg with no argument move; alias. No-argument behavior is decision 5
registry wiki wiki move; alias
index add / check / render / migrate the same keep (catalog maintainers)
llms the same keep (agents rely on it; also help agents)

Counts: 34 top-level names today; 28 canonical top-level names in 1.0 (5 newcomer, 7 package verbs, 10 nouns, 6 helpers and maintenance nouns), with 11 of today’s names (board, init, migrate, validate, audit, wiki, claim, renew, release, leases, promote) kept only as aliases and 5 new names (new, verify, lease, registry, repo). A newcomer reads five.

Extensions

Per the 1.0 criterion “unknown commands dispatch to extensions”: an unknown lean-pkg foo runs lean-pkg-foo from PATH with the remaining arguments, as git does, after the built-in names and aliases. This makes lean-pkg extract plan work for the existing lean-pkg-extract executable at no cost. lean-exercise serves a different audience (teaching) and stays its own executable; a lean-pkg-exercise link would make lean-pkg exercise work too. Extensions never shadow a built-in name.

The lab-specific workflow (the lab registry, committed mode, cluster routes) is a candidate for an extension, but the lease and committed-mode code sits inside the registry write path. Moving it out is a wave 3 question for the lab-coupling audit; for 1.0 the lease and registry nouns are enough to take it off the newcomer’s page.

JSON output

The criterion asks for --fields and --jq on JSON output. Today --fields exists on status, list and board. Proposal: --fields on every command with --json, with the same dotted paths and unknown-field error (exit 2) status --fields has; --jq EXPR runs jq when it is installed and refuses (exit 2, naming --fields) when it is not, so lean-pkg gains no dependency. The goldens in tests/golden/json-keys.json stay the contract for the full key sets.

Flag hygiene for 1.0

Changes that keep every old flag working:

Generated command reference

After the refactor, full command documentation is generated from the argparse tree into docs/commands/ on the Pages site (a separate stream builds the generator). The tree proposed here constrains it as follows:

  1. One page per canonical parser node, named by its path: docs/commands/lease-claim.md, docs/commands/comparator-config.md. Pages are keyed by the 1.0 canonical name, never by an alias, so claim, lease, renew, release, leases, init, migrate, validate, audit, board, wiki and promote get no page of their own. Each alias is listed on its canonical page (“Also spelled”) and in one generated docs/commands/aliases.md, from the same alias table the ARGV_TABLE rows test.
  2. The three pseudo-subcommands must become real subparsers first (comparator config, comparator host-check, formalization anchor), with comparator coverage and comparator migrate-signoff split out of comparator config. A generator run before that either misses them or needs special cases that would have to be removed later. Until they are split, the generator should fail loudly on a node whose help names a positional keyword, rather than render a page that hides them.
  3. Split modes get their own pages: repo export, repo adopt and repo move (today release --fresh-repo, release --adopt-repo, update --path); comparator attach and comparator check (today comparator NAME --receipt and --check); publish with --yes (today promote --yes). The old flags appear on the old command’s page only as “moved to”.
  4. Flag renames: the generator prints the canonical flag first and its aliases after it: --url (alias --repo on register, update, index add), --repo (aliases --repo-dir, --checkout), --target-repo (alias report --repo), registry audit --write (alias --fix), and --doi-track if that rename is accepted.
  5. Groups and tiers come from the parser, not from a list kept in the generator: each canonical node carries its tier (newcomer, author, coordination) and track (paper, library or both), so --help, the two track topics and the index page of docs/commands/ are rendered from the same data and cannot drift.
  6. Executables and extensions. receipt comparator is the canonical page for the comparator run; the comparator-receipt executable is an alias there. lean-exercise and lean-pkg-extract are documented on their existing pages, not generated with the tree; extensions found on PATH are never documented by the generator.
  7. Global flags (--registry, --events, --json, --commit, --no-commit, --push, --registry-snapshot) go on one generated page and are linked, not repeated, from each command page; receipt --commit SHA (the receipt’s commit) needs a distinct name before then (--receipt-commit, alias kept), or every receipt page shows two --commit lines.
  8. docs/cli.md becomes the generated index; its hand-written 19,000-word tables are the input that the per-command help text must absorb before it is retired.

5. Migration and deprecation policy

RELEASING.md asks for two things that pull in different directions: “old spellings are permanent aliases” and “an old spelling or flag keeps working, with a warning, for at least one minor release before it is removed”. This proposal separates them.

Aliases (renames). A renamed command or flag is an alias forever. It prints no warning in --json mode and never changes exit codes or output. In text mode it prints one stderr line, note: 'lean-pkg claim' is now 'lean-pkg lease claim' (the old spelling keeps working), which LEAN_PKG_NO_ALIAS_NOTE=1 silences. Each alias is an ARGV_TABLE row and has its own help golden, so removing one fails the suite.

Deprecations (removals of behavior). A flag, mode, key or command whose behavior goes away:

  1. is announced in a ### Deprecated CHANGELOG section with its replacement;
  2. keeps working with a stderr WARN: deprecated: ... line naming the replacement and the earliest version that may remove it, and a deprecations[] key in --json output;
  3. lives for at least two minor releases and 60 days, whichever is longer. “One minor release” is too short at the current cadence (65 releases in two weeks); after 1.0 a removal is a major release anyway;
  4. is removed only in a release whose ### Removed section names it.

The inline judged_as and lean_pkg_scaffold keys (moved to lean-pkg-signoff.json, warned today) are the precedent and would be the first entries of the ### Deprecated list.

Formats. A format changes only with a version bump and a migration command that is a dry run by default. Readers accept every earlier version forever when the file is evidence (receipts are never rewritten: rewriting would break the bytes they bind); for state files (registry, claims, index entries) the migration rewrites them and readers accept older versions until the next major.

Order of work. (1) Accept the tree (a decision record). (2) Add the new spellings as parsers that call the existing functions, with ARGV_TABLE rows and goldens; old spellings stay canonical in the docs for one minor. (3) Switch the docs and llms to the new spellings and add the alias notes. (4) Tag 1.0 once the remaining criteria hold.

6. On-disk formats

Format File Version marker Readers accept Migration Gap
Registry lean-packages.yaml version: 3 1, 2, 3; a newer version is refused with “upgrade lean-pkg” migrate (in place, additive, idempotent, --dry-run) none
Event log lean-package-events.jsonl none any line with event, name, ts none no version; event names and keys are documented only in prose
Claims claims.yaml schema: claims/1 claims/1 claims migrate (legacy claims.json to claims/1) none until a /2
Coverage coverage.yaml schema: coverage/1 coverage/1 (kind: library added within /1) none needed yet the rule for “additive within a version” is unwritten
Lower-tier receipt .lean-receipts/<c12>-<job>.json none the key set gate enforces none no schema key; later additions (log_commit_bound, artifacts_manifest_sha256, unit_properties_sha256, report_compressed) are distinguishable only by presence
Comparator receipt .lean-receipts/<c12>-comparator.json schema: comparator-receipt/2 /1 (legacy mechanism implied) and /2 reader compatibility (evidence is never rewritten) none
Comparator estimate printed JSON comparator-estimate/2 not read back none needed RELEASING lists it as on-disk; it is output only
Comparator configuration comparator.json none (Palomar’s format) Palomar’s keys; deprecated inline keys warned comparator config --migrate-signoff owned by Palomar; lean-pkg should only document which Palomar version it tracks
Headline configuration comparator.headline.json (or registry headline_config) none (Palomar’s six keys) the same as a comparator configuration none as above
Sign-off sidecar lean-pkg-signoff.json schema: lean-pkg-signoff/1 /1 from inline keys: comparator config --migrate-signoff none
formalization.yaml formalization.yaml version: v0.4 (mathlib-initiative) v0.4 (vendored JSON schema) none the plan for v0.5 (render both? refuse?) is unwritten
Source baseline data/source-baselines/... schema: source-baseline/1 /1 none none
Index entry index/<name>/entry.yaml schema: index-entry/2 /1 and /2 index migrate (--check) none
Comparator stage artifacts comparator-stages/ (stages.json, attempts, slots, partial receipts, olean manifest, type checkpoints) comparator-stages/1 and siblings the runner none internal: should be declared not public API
Reports claims-ledger/1, claims-rebase/1, host-routes/1, exercise-check/1, lean-pkg-extract-plan/1 yes printed or written on request none needed already versioned

What is missing for “versioned formats with migrations”

  1. Lower-tier receipt schema. Add schema: lower-receipt/1 to new receipts (additive: gate ignores unknown keys today). gate keeps accepting receipts without the key forever, read as version 0, because receipts are evidence bound to bytes and are never rewritten.
  2. Event log version. Add an optional v: 1 key to new events, and a documented list of event names with their keys (from the code, checked by a test). Readers treat a line without v as version 0.
  3. A formats page (docs/formats.md): each format, owner (lean-pkg or an outside project), current version, accepted versions, migration command, and the rule for additive changes within a version (a new optional key keeps the version; a new required key, a removed key or a changed meaning bumps it).
  4. A compatibility corpus in the tests: one fixture per accepted version of each lean-pkg-owned format, each read by the current code, so dropping support for an old version fails the suite.
  5. One discovery point for migrations. Today migrations are spread over migrate, claims migrate, index migrate and comparator config --migrate-signoff. Rather than one command that rewrites everything, doctor would list every file that is not at the current version, with the exact migration command for each (read-only).
  6. Outside formats. Record which Palomar and formalization.yaml versions a lean-pkg release targets, and the policy when they change.

7. How this meets the 1.0.0 criteria

Criterion (RELEASING.md) Met by
Final command tree, noun-verb, old spellings permanent aliases section 4 (package as the implied noun, nouns for everything else) and section 5 (aliases forever, ARGV_TABLE rows)
Unknown commands dispatch to extensions lean-pkg-<name> on PATH, section 4
--fields and --jq section 4, JSON output
Every format versioned, with migrations section 6, items 1 to 6
Goldens are the public API already true for help texts and JSON key sets; each alias adds a golden; a golden change needs a CHANGELOG entry
Written deprecation policy section 5, to be copied into RELEASING.md when accepted
Used in practice outside this proposal (waves 1 and 5)

8. Decisions for the maintainer

  1. Adopt the tiered tree with the package as the implied noun, and the two product tracks on the newcomer page? Recommendation: yes. It meets the criterion with the least churn (no lean-pkg package ... prefix), puts five verbs in front of a newcomer, and shows the paper track and the Lean-package track as two columns of the same five verbs, selected by new --kind paper|library.
  2. Aliases: permanent, or deprecated and removed? Recommendation: permanent, with a silenceable one-line note in text mode; warnings and removal only for behavior, never for spellings. Amend RELEASING.md to say so.
  3. Split release and fold promote into publish --yes? Recommendation: yes. release is the most misleading name in the tree for an outsider, and publish is the name a newcomer will look for.
  4. Add verify as a wrapper of receipt, comparator receipt and gate? Recommendation: yes, as a pure orchestrator that writes nothing the three steps would not, so the trust model is unchanged; it depends on wave 3 for hosts without systemd.
  5. What does lean-pkg with no argument do? Today it opens the board. Recommendation: short help (the five verbs) when no registry exists or stdout is not a tty, the board otherwise, which keeps the lab’s habit.

Further, smaller: the deprecation window (two minors and 60 days is proposed), --repo unification, renaming the DOI --track to --doi-track and receipt --commit to --receipt-commit (aliases kept), whether track L gets a read-only mathlib check, whether the event log gets a version key or a documented “unversioned, append-only” status, and the order against the command-reference generator (split the pseudo-subcommands before generating, section 4).