← Command reference · lean-pkg repo · CLI overview

lean-pkg repo export

export the gate-bound commit’s tree (or –from-tree SRCDIR) as a NEW single-commit repository at DIR, then move the package there (release NAME --fresh-repo DIR is the same).

Also spelled: lean-pkg lease release NAME --fresh-repo DIR, lean-pkg release NAME --fresh-repo DIR (all aliases).

Usage

lean-pkg repo export [--remote URL] [--keep-receipts] [--source-commit SHA]
                     [--from-tree SRCDIR] [--agent AGENT] [--reason REASON] [--dry-run]
                     [common flags] NAME DIR

[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
DIR	the new repository (must not exist, or be empty): internal files and the patterns file dropped, public-safety scanned; then the package is relocated there (repo move): evidence cleared, provenance note added
--remote URL	git remote add origin URL, and set the record’s repo
--keep-receipts	copy .lean-receipts/ from the source HEAD (they do not bind to the new commit)
--source-commit SHA	export this commit instead of the gate-bound one
--from-tree SRCDIR	export the working tree at SRCDIR (a hand-cleaned tree, not a commit; .gitignore honoured in a checkout) instead of the gate-bound commit
--agent AGENT	lease holder, if one is live
--reason REASON	free-text reason stored with the event
--dry-run	stage and scan, print the plan; nothing written

Details

Form	What it does	Key flags
repo export NAME DIR	a fresh-history public export (unrelated to leases; see Publishing a package incubated beside private work): git archive of the gate-bound commit (the recorded gate receipt’s commit, or --source-commit SHA), package directory only, unpacked into a staging directory beside DIR without .lean-pkg-private-patterns, the public-safety internal paths (approvals/, notes/, drafts/, scratch/, *.priv, *.private) and .lean-receipts/ (copied from the source HEAD with --keep-receipts; they do not bind to the new commit), each dropped path listed; then the public-safety scan of the staged tree and of the author and committer identity the export commit will carry (git’s identity for a new repository; a host-like address, user@hostname or a local TLD, is an export-commit-identity hit unless declared) (any blocking hit refuses, nothing written: “the exported tree of SHA12 has N public-safety hit(s); nothing written”; warn-only hits are listed in the plan as “0 blocking hit(s), N warning(s) (FAMILIES)” and do not refuse); then DIR becomes a new repository with one commit on main, message “fresh-history export of SHA12; receipts and gate must be re-run on this commit” plus source commit: and export date: lines, and origin set by --remote URL; then the registry entry is relocated as by update NAME --path DIR --reason "fresh-history release" (events relocated, status-changed; gate and comparator evidence cleared, verified-private becomes gate-pending, other private statuses unchanged) and a dated note (--append-note format, signed by --agent, else lean-pkg) keeps the old receipt paths and the source commit; --remote also sets repo (event updated). Refused: a public, upstreamed or archived package, DIR non-empty or inside the source repository, no gate receipt without --source-commit, another agent’s live lease, no git committer identity. Prints the next commands (public-safety, push, gate, lean-pkg receipt comparator --prepare, comparator, publish --dry-run --public-safety, promote). --dry-run stages and scans in a temporary directory and prints the plan (export path, dropped paths, the commit message, the registry change, the next commands); nothing is written. --json: source_commit, export_path, excluded[] {path, reason}, kept_receipts, commit_message, new_commit (null on a dry run), remote, public_safety, relocation, next_commands[], public_allow {file, carried, lines[]}. The allow: lines of .lean-pkg-private-patterns (only those; never a block or warn line) are carried into a committed .lean-pkg-public-allow in the export (merged with one the tree already has; the plan prints public allow: N allow line(s) ... carried), so the new repository’s own public-safety keeps exempting what the export scan exempted; an allow line a private block pattern (the patterns file’s, a registry-derived name) matches refuses the export, naming its line number, nothing written	DIR [--remote URL] [--keep-receipts] [--source-commit SHA] [--agent A] [--reason TEXT] [--dry-run]
repo export NAME DIR --from-tree SRCDIR	as repo export NAME DIR, but exports the working tree at SRCDIR, not a commit: a tree cleaned by hand (files removed or edited) that is not a commit of the source repository, which stays untouched. In a git checkout the files are those git ls-files --cached --others --exclude-standard lists (SRCDIR’s .gitignore applies, uncommitted edits and untracked files are exported); otherwise every file but .git/ and .lake/. Same exclusions, same scan (the commit message is scanned too, since it names SRCDIR’s basename; a blocking hit refuses: “the working tree SRCDIR has N public-safety hit(s); nothing written”), same single commit, message “fresh-history export of working tree BASENAME; receipts and gate must be re-run on this commit” plus source commit: none (hand-cleaned tree), source package commit for provenance: SHA (the gate-bound commit, or none) and export date:. The package’s patterns file applies when its checkout has one, else SRCDIR’s. Refused also: SRCDIR not a directory, DIR inside SRCDIR, nothing left to export, --source-commit. --json adds from_tree, provenance_commit; source_commit is null	DIR --from-tree SRCDIR [--remote URL] [--keep-receipts] [--agent A] [--reason TEXT] [--dry-run]

Examples

Plan a fresh single-commit public repository from the gated tree; nothing is written.

lean-pkg repo export my-proof ../my-proof-public --dry-run