← Command reference · lean-pkg lease · CLI overview

lean-pkg lease claim

CAS lease on a package (24h default TTL).

Also spelled: lean-pkg claim, lean-pkg lease NAME (all aliases).

Usage

lean-pkg lease claim --workspace WORKSPACE --agent AGENT [--ttl HOURS] [--reason REASON]
                     [--contact TEXT] [--force] [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
--workspace WORKSPACE	Required.
--agent AGENT	Required.
--ttl HOURS	lease TTL, 1..8760 (default: 24 for a new claim; a holder’s re-claim keeps the lease’s current ttl_hours; above 8760: exit 2)
--reason REASON
--contact TEXT	address of the holding session (e.g. an amsg address such as lab-desk/n14-paper or @lean-ops), stored in the lease and shown by leases/status; one line, at most 200 characters; a holder’s re-claim without it keeps the lease’s
--force	override a live lease; requires –reason

Details

Form	What it does	Key flags
claim NAME (alias lease NAME)	compare-and-swap lease, 24 h default for a new claim; the holder’s re-claim refreshes it and keeps its TTL unless --ttl is given (event claim-refreshed, with the reason when given). --contact TEXT stores the holding session’s address in the lease (lease.contact, e.g. an amsg address such as lab-desk/n14-paper or @lean-ops; see Lease holders); a holder’s re-claim with it replaces the contact, without it keeps it; the events claimed, claim-forced and claim-refreshed carry contact when the lease has one. A contact is one line of at most 200 characters (empty, a newline or another control character, or longer: exit 2, nothing written). --ttl is 1 to 8760 hours (one year); a larger value exits 2 with nothing written	--workspace W --agent A [--ttl HOURS] [--reason] [--contact TEXT] [--force]

JSON output

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

• claim (exit 0): event, expires_at, lease, name, notes, ok

Examples

Take the 24-hour lease before working on the package, so other agents see who holds it.

lean-pkg lease claim my-proof --workspace laptop --agent alice --reason "chapter 2"

Sample output:

my-proof: lease claimed for alice@laptop until 2026-10-18T14:24:32+00:00

The same, with an address where others can reach the holding session.

lean-pkg lease claim my-proof --workspace laptop --agent alice --contact lab-desk/my-session