← Command reference · CLI overview

lean-pkg register

the ONLY write path for new packages: validated, deduping, auto-detecting.

Usage

lean-pkg register [--url URL] --path PATH [--like OTHER] [--owner-project OWNER_PROJECT]
                  [--license-spdx SPDX] [--visibility {private,public}]
                  [--status {scratch,active,gate-pending,public}]
                  [--upstream-target {none,mathlib,palomar}] [--automation AUTOMATION]
                  [--notes NOTES] [--reason REASON] [--workspace WORKSPACE]
                  [--agent AGENT] [--ttl TTL] [--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  
--url URL git URL (or local bare path); required unless –like gives it (old spelling –repo, kept working)
--path PATH local checkout path, $HOME-relative. Required.
--like OTHER a sibling of registered package OTHER: copy its repo, owner-project, upstream-target and automation (flags given here win; visibility is never copied, default private), and report whether the toolchain and Mathlib pin match OTHER’s
--owner-project OWNER_PROJECT  
--license-spdx SPDX the package’s license, an SPDX identifier or expression (Apache-2.0, MIT OR Apache-2.0); the page, the publish checklist and formalization.yaml read it (later: update –license-spdx)
--visibility {private,public} Choices: private, public. Default: private.
--status {scratch,active,gate-pending,public} public only with –visibility public and –reason (an already-public repo). Choices: scratch, active, gate-pending, public. Default: active.
--upstream-target {none,mathlib,palomar} default none. Choices: none, mathlib, palomar.
--automation AUTOMATION  
--notes NOTES  
--reason REASON required with –status public
--workspace WORKSPACE metadata only; does NOT claim
--agent AGENT metadata only; does NOT claim
--ttl TTL accepted and ignored (register never claims; claim separately with lean-pkg lease claim NAME --ttl H)
--dry-run print the would-be entry as YAML without writing

Details

Form What it does Key flags
register NAME the only write path for new packages; validated, deduping by name and by resolved checkout (~/ expanded, relative paths taken from $HOME, stored $HOME-relative), auto-detects toolchain and Mathlib pin; a Lean root namespace (each lean_lib in lakefile.lean or lakefile.toml, else the top-level *.lean files) that another registered package’s checkout also uses is a stderr note and a notes entry in --json, never a refusal; an empty --path, --repo or --owner-project, or a path resolving to $HOME, is refused; a --path that does not exist on this host is only a warning (warn: local_path does not exist on this host), and lean_toolchain and mathlib_pin are then recorded as null: fix the path later with update NAME --path DIR --reason R, then update NAME --redetect. NAME is the package name every later command takes. --like OTHER registers a sibling of a registered package (for example lean-r2/ beside lean/ in one manuscript repository; see Sibling packages): repo, owner_project, upstream_target and automation are taken from OTHER unless given (visibility is never copied: it defaults to private); copying OTHER’s repo is refused when both checkouts are on this host in different git repositories and --repo is absent (nothing written); a stderr note says whether the detected toolchain and Mathlib pin match OTHER’s, never a refusal; --json gains like {name, copied[], toolchain {this, like, match}, mathlib_pin {this, like, match}} and the registered event like; an unknown OTHER is refused (exit 1); with neither --repo nor --like it is a usage error (exit 2). Warnings (warn: lines, warnings[] in JSON), never refusals: the checkout lies inside, or contains, another registered package’s directory (every commit to the inner one is drift for the outer one’s receipt); its lake-manifest.json has a path dependency outside the package directory (gate refuses that receipt) --repo URL (or --like OTHER) --path HOME-RELATIVE [--like OTHER] [--owner-project] [--visibility] [--status scratch|active|gate-pending|public] (public needs --visibility public and [--reason]) [--upstream-target none|mathlib|palomar] [--automation] [--notes] [--dry-run]

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

Print the entry that would be written, detected toolchain and Mathlib pin included; nothing is written.

lean-pkg register my-proof --url git@github.com:you/my-proof.git --path src/my-proof --license-spdx Apache-2.0 --dry-run

Register a new package from its checkout (the path is relative to $HOME); it starts at status active.

lean-pkg register my-proof --url git@github.com:you/my-proof.git --path src/my-proof

Sample output:

my-proof: registered (status=active, visibility=private, toolchain=leanprover/lean4:v4.24.0, pin=?)