← Command reference · CLI overview

lean-pkg-extract

Plan a standalone public Lean-verification repository from a mixed working repository, with exact provenance. Read-only; no registry, no network.

Usage

lean-pkg-extract COMMAND

Subcommands

• lean-pkg-extract plan: dry run: classify, check and inventory what an extract at COMMIT would contain

More from –help

examples:
  lean-pkg-extract plan --repo . --commit HEAD --manifest extract.json
  lean-pkg-extract plan --repo ~/paper --commit 0123abc --manifest extract.json --json
  lean-pkg-extract plan --repo . --commit v1.0 --manifest extract.json --report ../extract-plan.json

Dry run only: `plan` reads git objects at COMMIT and writes nothing (--report PATH, outside SRC, is the
one exception). The `write --output DIR` step comes next.
exit codes: 0 plan clean, 1 refused (every reason listed), 2 usage.
docs: https://lean-pkg.github.io/lean-pkg/extract.html

Details

See also lean-pkg-extract plan --repo SRC --commit COMMIT --manifest PATH, a separate console script that plans a public Lean-verification repository from a mixed working repository, read-only and registry-free: Extracting a public Lean repository.

lean-pkg-extract plan

dry run: classify, check and inventory what an extract at COMMIT would contain.

Usage

lean-pkg-extract plan --repo SRC --commit COMMIT --manifest PATH [--json]
                      [--report PATH]

Dry run: classify every file under the manifest’s roots at COMMIT (default deny), check paths, links, pins, dependencies, claims and imports, and print the inventory. Writes nothing.

Arguments and flags

Argument or flag	Description
--repo SRC	the source git repository (its top directory). Required.
--commit COMMIT	the source commit; recorded as a full SHA. Required.
--manifest PATH	the extract manifest, strict JSON, schema lean-pkg-extract/1. Required.
--json	JSON on stdout (schema lean-pkg-extract-plan/1)
--report PATH	also write the JSON plan (with the private excluded list) to PATH, outside SRC