← Command reference · lean-pkg receipt · CLI overview

lean-pkg receipt systemd

a lower-tier receipt from a finished systemd –user service unit (run bounded with –run, or its saved properties), its verify log and its stdout seal.

Also spelled: lean-pkg receipt local (all aliases).

Usage

lean-pkg receipt systemd --unit U --log PATH --receipt-commit SHA [--stdout PATH]
                         [--stderr PATH] [--properties-file F] [--run]
                         [--memory-max BYTES] [--memory-swap-max BYTES]
                         [--cpu-quota PCT] [--runtime-max SPAN] [--setenv NAME=VALUE]
                         [--require-tools A,B,...] [--properties-out PATH]
                         [--redact REGEX] [--checker TEXT] [--repo DIR] [--out PATH]
                         [--compress-log] [--append-readme] [--readme-heading TEXT]
                         [--readme-line TEXT] [--tar-sha256 HEX] [common flags]
                         [-- CMD ...]

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

Arguments and flags

Argument or flag	Description
--unit U	the service unit (.service added when absent); job_id becomes systemd-user:<U>:<InvocationID>@<host label> (h- + 12 hex of the host name’s SHA-256). Required.
--log PATH	the raw verify log the unit writes; when it has no checker: line, –checker TEXT is required. Required.
--receipt-commit SHA	the verified commit; must exist in –repo (with –run: the checkout’s clean HEAD) (old spelling –commit, kept working). Required.
--stdout PATH	the unit’s stdout file: verify-log-sha256 = sha256(raw log), pre-manifest-sha256 = post-manifest-sha256 = sha256(lake-manifest.json at the commit), optional invocation-id = InvocationID; without it the log must carry its own seal. With –run the unit writes it
--stderr PATH	the unit’s stderr file; must be empty. With –run the unit writes it
--properties-file F	saved systemctl --user show U -p Id,LoadState,ActiveState,SubState,Result,InvocationID,ExecMainCode,ExecMainStatus,ExecMainStartTimestamp,ExecMainExitTimestamp,ExecMainStartTimestampMonotonic,ExecMainExitTimestampMonotonic,NRestarts,MemoryPeak,CPUUsageNSec,MemoryMax,MemorySwapMax,CPUQuotaPerSecUSec,RuntimeMaxUSec,OOMPolicy,RemainAfterExit output, captured before the unit was collected, plus a Hostname= line for the host it ran on
--run	start -- CMD ... as the bounded unit U (systemd-run –user, RemainAfterExit, WorkingDirectory=–repo), wait for it, capture its properties before stopping it; –log, –stdout, –stderr must not exist yet. The running lean-pkg’s own files must not change during the run (sealed as the receipt key producer)
--memory-max BYTES	–run: MemoryMax (default 8G)
--memory-swap-max BYTES	–run: MemorySwapMax (default 0, so the memory cap is an OOM kill, not swapping)
--cpu-quota PCT	–run: CPUQuota (default 400%)
--runtime-max SPAN	–run: RuntimeMaxSec (default 4h)
--setenv NAME=VALUE	–run: an extra environment variable for the unit (repeatable; PATH is passed; LAKE_CACHE_DIR=<fresh empty dir> and LAKE_ARTIFACT_CACHE=false unless named here)
--require-tools A,B,...	–run: executables the command needs (comma-separated, repeatable), each resolved with type -P in the unit’s PATH before the unit is created; a missing one refuses and nothing is run. The resolved paths and SHA-256 are printed (stderr) and in –json run_tools
--properties-out PATH	–run: where the captured properties go (default <log>.unit.properties)
--redact REGEX	also replace matches with <redacted> (repeatable); the checkout’s path, $HOME and /run/user/N/ are always redacted to <repo>, <HOME>, /run/user/<UID>/ instead
--checker TEXT	the exact checker command or mode (default: the log’s checker: line)
--repo DIR	the package checkout (default: the current directory)
--out PATH	receipt path (default <repo>/.lean-receipts/<commit12>-systemd-user-<U>-<InvocationID>-<host label>.json); the redacted log is written beside it as <commit12>-systemd-user-<U>-<InvocationID>-<host label>-verify.redacted.log
--compress-log	write the redacted log as deterministic gzip <…>-verify.redacted.log.gz (level 9, mtime 0, no file name) instead of the plain .log; report_sha256 stays the SHA-256 of the uncompressed log and the receipt gains report_compressed {format: gzip, sha256 of the .gz, bytes = decoded length, not the .gz size}; gate decompresses (bounded) and checks report_sha256. Restore: gzip -dc X.log.gz > X.log. Without it, a log over 90 MiB prints a WARN naming this flag
--append-readme	append the entry block to README.md beside the receipt (created if absent; an entry already naming the receipt is not repeated)
--readme-heading TEXT	the entry heading after the short commit (default: lower-tier receipt, systemd unit U)
--readme-line TEXT	an extra line at the end of the entry block (repeatable)
--tar-sha256 HEX	the frozen source tarball’s SHA-256, named in the entry block
-- CMD	with –run: the command the unit runs

Details

Form	What it does	Key flags
receipt systemd	the same receipt from a finished systemd –user service unit, for checks run locally in a capped unit; reads and writes no registry. The unit’s terminal state comes from one of: --run -- CMD ... (lean-pkg starts CMD as the transient unit U with systemd-run --user --unit=U -p RemainAfterExit=yes -p WorkingDirectory=<repo> -p OOMPolicy=stop -p MemoryMax=8G -p MemorySwapMax=0 -p CPUQuota=400% -p RuntimeMaxSec=4h (--memory-max, --memory-swap-max, --cpu-quota, --runtime-max change the caps; a value must be finite), the unit’s stdout and stderr going to --stdout / --stderr, PATH and every --setenv NAME=VALUE passed; --require-tools A,B,... (repeatable) first resolves each project-declared executable with type -P in the unit’s PATH before the unit is created, prints each resolved path, real path and SHA-256 to stderr (--json run_tools {required, resolved[] {name, path, realpath, sha256}, missing}) and refuses, running nothing, when one is missing; RemainAfterExit keeps the finished unit loaded, so lean-pkg polls systemctl --user show U until it is terminal, captures its properties and this host’s name to --properties-out (default <log>.unit.properties, kept even when the receipt is refused) and only then stops and resets the unit; --log, --stdout, --stderr must not exist yet, and the checkout must be at --commit with no tracked change and no untracked file under the package directory before the run and still after it; untracked means listed by git ls-files --others --exclude-standard, less .lean-receipts/, .lake/ and the run’s own output files; files git ignores are not checked, so they are not bound), --properties-file F (systemctl --user show U -p Id,LoadState,ActiveState,SubState,Result,InvocationID,ExecMainCode,ExecMainStatus,ExecMainStartTimestamp,ExecMainExitTimestamp,ExecMainStartTimestampMonotonic,ExecMainExitTimestampMonotonic,NRestarts,MemoryPeak,CPUUsageNSec,MemoryMax,MemorySwapMax,CPUQuotaPerSecUSec,RuntimeMaxUSec,OOMPolicy,RemainAfterExit saved before the unit was collected, plus a Hostname= line for the host it ran on; exactly these properties are read, RemainAfterExit and the resource ones optional, so a capture without RemainAfterExit stays valid; MainPID is not exported), else systemctl --user show U now on this host. Unit checks (every failure listed, any one refuses: exit 1, nothing written to .lean-receipts): LoadState=loaded (a --collect unit read after it finished is not found), Id is U (.service added), a 32-hex InvocationID, terminal (ActiveState failed or inactive, or active with SubState=exited; activating, running, deactivating refuse) with an exited main process, Result=success (oom-kill, timeout, signal, core-dump, exit-code are named), ExecMainCode exited with ExecMainStatus 0 (killed or dumped: the signal is named), NRestarts 0, a host name. Then every receipt slurm check: the stdout seal or the in-log fallback, an optional stdout invocation-id line equal to the InvocationID, an empty --stderr, the toolchain, Mathlib rev, sorry count, axioms, checker and the optional commit:, job-id: (the job_id or the InvocationID), generated-at: lines, and the public-safety scan after redacting the checkout’s absolute path to <repo>, $HOME to <HOME>, /run/user/N/ to /run/user/<UID>/ and every --redact. job_id is systemd-user:<U>:<InvocationID>@<host label>, the label being h- and the first 12 hex digits of the SHA-256 of the lower-cased host name (the running system’s, or the Hostname= line’s); the host name itself is never written. Writes, beside the receipt and the redacted log, <c12>-<slug>-unit.properties (the recognised properties only, in a fixed order, host last as its label; its SHA-256 is the additive receipt key unit_properties_sha256), and prints the README entry (unit, invocation, host, Result, exit, runtime, CPU, memory peak, the caps, a - Unit properties: line). --json as receipt slurm with unit {id, invocation_id, host, active_state, sub_state, result, exec_main_code, exec_main_status, runtime_usec, cpu_usage_nsec, memory_peak, memory_max, memory_swap_max, cpu_quota_per_sec, runtime_max, remain_after_exit}, properties and ran in place of sacct; usage errors exit 2. A --run interrupted while waiting (SIGINT, SIGTERM, SIGHUP) leaves the unit running, keeps its temporary LAKE_CACHE_DIR while the unit may still run (removed once it is gone or finished), writes nothing, exits 128 + the signal number and prints the recovery command (the same command without --run) with a WARN that recovery skips the source-unchanged-during-the-run check. Details: Receipts and trust	--unit U --log PATH --commit SHA [--properties-file F \| --run [--memory-max B] [--memory-swap-max B] [--cpu-quota PCT] [--runtime-max SPAN] [--setenv NAME=VALUE]... [--require-tools A,B,...]... [--properties-out PATH] -- CMD ...] [--stdout PATH] [--stderr PATH] [--checker TEXT] [--repo DIR] [--redact REGEX]... [--out PATH] [--compress-log] [--append-readme [--readme-heading T] [--readme-line T]... [--tar-sha256 HEX]] [--json]
receipt local	an alias of receipt systemd: the same flags, checks and output	as receipt systemd

Examples

Run a light verify script locally in a capped systemd –user unit and write the same lower-tier receipt as receipt slurm.

lean-pkg receipt systemd --unit audit-gate --commit "$(git rev-parse HEAD)" \
  --log gate/verify.log --stdout gate/unit.out --stderr gate/unit.err \
  --checker "gate.sh (lake build; #print axioms)" --run -- bash gate.sh gate/verify.log