lean-pkg new

scaffold a new Lean package (Challenge/Solution, comparator.json, claims, coverage, verify.sh) in a new directory and git init it; no registry, no network.

Usage

lean-pkg new [--kind {paper,library}] [--stack NAME|current|none] [--dir DIR]
             [--module MOD] [--no-mathlib] [--author TEXT] [--license {Apache-2.0,MIT}]
             [common flags] NAME

[common flags]: --json, --commit, --push, --no-commit, also accepted before the command name; see the CLI overview.

Write a minimal Lean 4 package that comparator-receipt, receipt systemd, gate and reuse lint accept unchanged (and page, for –kind library; a paper’s coverage.yaml waits for the paper), then git init it. Nothing is committed, fetched or built; no registry is read or written. Next steps: docs/quickstart.md.

Arguments and flags

Argument or flag	Description
`NAME`	the package name: lower-case letters, digits, single hyphens (e.g. my-proof)
`--kind {paper,library}`	paper (default): the paper is the product; coverage.yaml stays incomplete until you name the paper and `formalization anchor` binds its posted version. library: the Lean package is the product; coverage.yaml lists the example as its main result. Choices: `paper`, `library`.
`--stack NAME\\|current\\|none`	pin lean-toolchain and the Mathlib require to a declared LTS stack and write `stack: NAME` into coverage.yaml (docs/stacks/); current: the newest declared stack whose window covers today; none: the newest pins, no key. Default: current for –kind paper (the newest pins when no stack is current), none for –kind library. An undeclared name exits 2
`--dir DIR`	where to write it (default ./NAME); refused when it exists and is not empty
`--module MOD`	the library and namespace (default: NAME in CamelCase, my-proof -> MyProof)
`--no-mathlib`	core Lean only: no Mathlib dependency (fast to build; comparator-receipt then needs COMPARATOR_RECEIPT_NO_MATHLIB=1)
`--author TEXT`	the CITATION.cff author (default: git config user.name)
`--license {Apache-2.0,MIT}`	the LICENSE written (default Apache-2.0); pass the same id to `update NAME --license-spdx`. Choices: `Apache-2.0`, `MIT`.

Details

Form	What it does	Key flags
`new NAME`	scaffold a minimal Lean 4 package in `./NAME` (or `--dir DIR`; refused when it exists and is not empty) and `git init` it, for the quickstart: the getting-started template (`lean-toolchain`, `.gitignore`, `lakefile.toml`, `MOD/Challenge.lean`, `MOD/Solution.lean`, `comparator.json`) plus `MOD/Axioms.lean` (`#print axioms`), `claims.yaml` (one reusable claim), `coverage.yaml` (below), `CITATION.cff` (the author is `--author`, else `git config user.name`; a name with no space prints a warning, since it looks like a handle), `LICENSE` with the same text in `LICENSES/<SPDX>.txt`, a `REUSE.toml` that puts every file, receipts and logs included, under that license (so `reuse lint`, which `publish --dry-run` runs, passes), a `README.md` carrying the lean-pkg credit, and `verify.sh`, the lower-tier check whose log `receipt systemd --run` reads. The `lakefile.toml` names its library in `defaultTargets`, so a bare `lake build` builds it. Nothing is committed, fetched or built, and no registry is read or written. `--stack NAME` pins a declared LTS stack: its `lean-toolchain` and Mathlib tag, and `stack: NAME` in `coverage.yaml`, which `doctor NAME`, `verify` and `page` check against the committed pins; `--stack current` is the newest declared stack whose window covers today and `--stack none` the newest pins with no key. Without `--stack`, `--kind paper` takes the current stack (the newest pins, with a warning, when none is current) and `--kind library` the newest pins (libraries aimed at Mathlib follow its newest release; proposal 0004, open question 7). An undeclared stack exits 2, listing the declared ones. The stack’s comparator tools are the ones its toolchain bundles, so the toolchain pin is theirs. `--kind paper` (the default) writes a `kind: paper` `coverage.yaml` that is incomplete on purpose: `manuscript.version: unposted` and `FILL-ME` markers, which `coverage check` and `page` refuse until you name the paper and its results; `formalization anchor --write` then binds the posted version (no manuscript is invented). `--kind library`: one main result naming the example claim, which `coverage check` accepts as written. `--no-mathlib`: core Lean only (`lean-pkg receipt comparator` then needs `COMPARATOR_RECEIPT_NO_MATHLIB=1`; `verify.sh` logs `mathlib-rev: none`, the receipt’s explicit value for a package without Mathlib). The name: lower-case letters, digits and single hyphens, starting with a letter; a library named like Lean’s or a Mathlib dependency’s root namespace is refused (exit 2)	`[--kind paper\\|library] [--stack NAME\\|current\\|none] [--dir DIR] [--module MOD] [--no-mathlib] [--author TEXT] [--license Apache-2.0\\|MIT] [--json]`

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):

new-stack (exit 0): author, author_source, committed, coverage_complete, dir, files, git_init, kind, lean_toolchain, license_spdx, mathlib, mathlib_rev, module, name, next_commands, ok, registry_touched, stack, stack_source, warnings

Examples

Scaffold a companion to a paper (kind paper, the default; library MyPaperLean, Mathlib) in ./my-paper-lean and git init it; its coverage.yaml waits for the paper’s title and rows, then formalization anchor.

lean-pkg new my-paper-lean

Sample output:

created my-paper-lean/: package my-paper-lean (kind paper), library MyPaperLean, v4.35.0-rc2, Mathlib v4.35.0-rc2; 15 files, git initialized, nothing committed, no registry read or written

Scaffold a library (its coverage.yaml lists the example as the main result); the quickstart takes it from there.

lean-pkg new my-proof --kind library

The same in core Lean, with the author and the license named.

lean-pkg new my-proof --kind library --no-mathlib --author "Ada Lovelace" --license MIT