← Command reference · CLI overview

lean-pkg publish

the checklist from verified-private to listed, with the exact next commands (read-only); –yes makes the repository public (promote is the same).

Also spelled: lean-pkg promote (all aliases).

Usage

lean-pkg publish [--yes] [--dry-run] [--public-safety] [--skip-public-safety]
                 [--agent AGENT] [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
--yes	publish: run the promotion checklist, then gh repo edit –visibility public (ONE-WAY); first fetches origin’s branches, tags and pull-request heads so the public-safety scan covers them (a failed fetch refuses). With –dry-run: the same checklist, nothing flipped
--dry-run	write nothing (the default without –yes); with –yes: the promotion checklist only
--public-safety	read-only checklist: also scan the tree and git history for private patterns (lean-pkg public-safety); –yes always scans
--skip-public-safety	with –yes: do not run the public-safety scan of the tree and history (a WARN line instead; the scan covers the whole repository when the package is a subdirectory of it)
--agent AGENT	with –yes: the agent acting (recorded as the promoted event’s actor); another agent’s live lease then refuses

Details

Form	What it does	Key flags
publish NAME	read-only release checklist from verified-private to listed (--dry-run says so explicitly and changes nothing): the page --check line (a WARN while the package has no coverage.yaml and no page block, a failure for an unbacked Easley sentence; JSON page); the promotion checklist of --yes, claims ledger included (for a verified-private package; --json claims_ledger as with --yes, null otherwise; a public one only needs HEAD pushed), consent recorded, license_spdx set and the LICENSE text matching it, formalization.yaml present, schema-valid and equal to the render (stale evidence is a ✗; missing is a ✗ for upstream_target: palomar, else WARN), claims.yaml synced at HEAD when tracked, a Lake package name in the lakefile, a tag at HEAD (WARN); then the exact next commands (publish NAME --yes --dry-run, publish NAME --yes, git tag/push, record reservoir-listed, record palomar-submitted; the tag push names the checkout’s GitHub remote, found by URL among git remote -v since origin may be a private mirror, says “after publish –yes” while the package is not public, and says so when no remote points at GitHub). The git-ignored evidence WARN of --yes (for any status) and --json ignored_evidence[] {path, rule}. Exit 0 when no ✗, else 1; --json: ready, checklist[], next[], manuscript_findings (the ledger’s summary of what the formalization found in the manuscript, also one text line manuscript findings (what the formalization found): ... when there is one; never a checklist item, never a status; Lifecycle). --public-safety adds the public-safety scan as a checklist line (the --yes refusal text when it has hits; --json gains public_safety); a WARN item palomar: not submittable ... when palomar check finds error gaps at HEAD (JSON palomar_check, as in gate --check); it never makes the checklist fail	[--dry-run] [--public-safety]
publish NAME --yes	publish: the promotion checklist, then the GitHub repository goes public (one-way); --yes --dry-run runs the checklist and flips nothing (the pre-1.0 publish NAME --yes --dry-run; publish NAME --yes is publish NAME --yes). The checklist requires the claims ledger at the promote stage to be ready (every reusable claim verified, theorems and lemmas by the comparator tier too; a package without claims is unknown and refused; the line is claims ledger ready: N required claim(s) verified (sha256:…) or claims ledger STATUS: REASON; first: ID: CODE naming claims ledger NAME; --json gains claims_ledger {package_status, counts, required, reasons, ledger_digest}; see Lifecycle), both receipts and every comparator log committed at HEAD unmodified, and HEAD contained in origin/<branch> (local refs; the dry run never fetches); under --yes a failed gh query is a failure. --yes first runs git fetch --prune --tags origin with the refspecs +refs/heads/*:refs/remotes/origin/* and +refs/pull/*/head:refs/remotes/origin/pr/* (GitHub’s pull-request heads are published with the repository), 120 s timeout, so the scan covers every branch, tag and pull-request head the remote holds; the first checklist line is then “fetched origin’s branches, tags and pull-request heads: the scan covers them” or the ✗ “git fetch origin failed (…): cannot verify what the public flip would publish”, which refuses. It also runs public-safety NAME (the whole repository when the package is a subdirectory of it: the line then reads “public-safety (whole repository: the package is a subdirectory): …”) and refuses while blocking hits remain, with the checklist line “public-safety: N hit(s) — fix the tree, or publish a fresh-history tree with repo export; see lean-pkg public-safety NAME” (“ (+W warning(s))” after the count when there are warn hits too); warn-only hits give the WARN line “public-safety: 0 blocking hit(s), N warning(s) (FAMILIES) — review with lean-pkg public-safety NAME” and do not block; --skip-public-safety replaces the scan with a WARN line. --json gains public_safety {skipped, hits, tree_hits, history_hits, block_hits, warn_hits, scope (package or repository), unscanned, unscanned_blocking}. Evidence that exists on disk but that git ignores (the gate and comparator receipts, the comparator logs, and the comparator-stages/ files, stages.json and stage logs, beside them; judged by git check-ignore -v, so a force-added tracked file is never reported) is the WARN line “evidence on disk is git-ignored, so git add skips it: PATH (RULE), …; un-ignore it: add !.lean-receipts/ and !**/.lean-receipts/** to .gitignore after the ignoring rule (a !PATH line for evidence elsewhere), or git add -f PATH”, RULE being SOURCE:LINE:PATTERN such as .gitignore:3:*.log; the ✗ for a required file that is not committed names the rule, “not committed: PATH (git-ignored by RULE)”. --json gains ignored_evidence[] {path, rule}	--yes [--dry-run] [--skip-public-safety] [--agent A]

Exit codes

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

Exit 1 is also a negative answer here:

• publish NAME --dry-run: not ready to publish

JSON output

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

• promote-dry-run (exit 1): checklist, claims_ledger, dry_run, ignored_evidence, name, ok, one_way_warning, public_safety, refused
• publish-dry-run (exit 1): checklist, claims_ledger, dry_run, head, ignored_evidence, manuscript_findings, name, next, ok, page, palomar_check, ready

Examples

The read-only checklist from verified-private to listed, with the exact next commands; exit 1 while not ready.

lean-pkg publish my-proof

The same, also scanning the tree and the git history for private strings.

lean-pkg publish my-proof --public-safety

The promotion checklist that –yes runs; nothing changes (the pre-1.0 promote my-proof).

lean-pkg publish my-proof --yes --dry-run

Make the GitHub repository public after the checklist passes again; this cannot be undone in practice.

lean-pkg publish my-proof --yes