The lema command

Every subcommand of the lema binary, with its flags, what it prints and how it exits.

lema is one Rust binary, built from crates/lema-cli/src/main.rs. It is both the server (lema serve) and its client, and it also runs commands that work on a store or a runtime output directly. This page lists every subcommand in that file at lema-lang HEAD 5a94951.

lema [--socket PATH] COMMAND [SUBCOMMAND] [FLAGS] [WORDS] [-- ARG ...]

Global options

The parser reads the command line as follows:

• A flag is found by name anywhere on the line, and the first occurrence counts. The exceptions are --ref, --release and --review on site build, which may repeat.
• A flag takes the next word as its value, except --codec, --reorder, --reset, --operator and --llms, which take none.
• build --standalone and release deployment --input take no value, but they are not in the parser’s list of flags without a value. The word after either one is therefore never read as a positional word.
• A list written ID,.. is split on commas, and empty items are dropped.
• Words that are neither flags nor flag values are positional: the command, its subcommand, and for run and test the program’s arguments.

Output and exit codes

A command prints its result on standard output, followed by a newline. Most print one canonical JSON value (sorted keys, no whitespace). init, verify-distribution and check-runtime print one line of text. run writes the program’s output bytes unchanged and puts its summary on standard error.

An error prints lema: <message> on standard error. When a server refuses a request, the message is the server’s error text.

Commands that open a store themselves take the store’s exclusive lock: actor, release (all but deployment), site build, build, test, run --release and the retired http-build. While a server holds it they fail with the store at DIR is in use.

Setup and checking

verify-distribution

lema verify-distribution DIR

Checks an extracted Lean distribution against the pinned manifest: the manifest’s own SHA-256, the exact set of files and symlinks, every file’s SHA-256, and that every file and directory belongs to root or the running user and is not writable by group or others. DIR holds extraction-manifest.json and lean-4.34.1-linux/. It takes no flags.

DIR: the pinned Lean distribution (FILES files, SYMLINKS symlinks; manifest c82b7b44dd02daae5aa46c3f7e0a1e564da1a183fd81c021f299370a51d297a5)

check-runtime

lema check-runtime --runtime CONFIG

Loads a runtime configuration as a native call would, then makes one small native call under the full controls: the proof theorem check_runtime : 1 + 1 = 2 := rfl, run by the pinned lean in a systemd scope and bubblewrap. The call writes to the configuration’s output like any native call (its ledger lines, work directory, log and records), and a fault there sets that output’s latch.

--runtime CONFIG is required: the runtime configuration file.

The exit code is 75 when the refusal is temporary: another native call held the lock for the whole 10-minute wait, a native systemd scope is still present, or the host is under pressure. Host pressure counts as temporary only on a machine with at least 7 GiB of total memory, the 6 GiB floor plus 1 GiB.

CONFIG: this machine can run the trusted runtime: a native call ran in SECONDSs (distribution DIR, output DIR)

init

lema init --store DIR [--axioms LIST]

Creates a store: the directory (mode 0700), store.json with the namespace and the axiom policy, an empty aliases.json, objects/ holding the namespace object, and receipts/. It refuses a directory that already holds store.json.

created store DIR (namespace NAMESPACE-ID)

Server and client calls

serve

lema [--socket PATH] serve --store DIR --runtime CONFIG

Runs the server. It opens the store and takes its lock, then loads the runtime and the module cache. If the cache does not hold the decoder module LemaCodebase, the server compiles it in one native call. When that call cannot run, the server still answers reads, and elaborate and submit try the compile again.

The server then binds the socket owner-only and answers requests until it is stopped. It replaces a stale socket, and refuses a path where a server still answers or that is not a socket. It prints lema: serving STORE on SOCKET on standard error. The protocol is on the server methods page.

call

lema [--socket PATH] call METHOD [--params JSON | --params-file FILE]

Sends one request and prints its result as canonical JSON.

Without either flag, params is {}.

info, ids, reverify

lema [--socket PATH] info
lema [--socket PATH] ids
lema [--socket PATH] reverify

Each sends the method of the same name with {} as its params. reverify with no roots replays every accepted object from scratch. They take no flags.

Execution

These commands take an execution manifest or an artifact built from one. Artifacts live under the runtime output’s artifacts/.

build

lema build --manifest FILE --store DIR --runtime CONFIG --name NAME [--backend lean|lean-native] [--lean DIR] [--cap NAME] [--standalone]

Builds the manifest’s artifact into artifacts/NAME. Every root must be accepted in the store, and the compiled roots must equal their accepted closure.

The output is a JSON object with status ("built"), backend, directory, id, exec, closure_sha256, roots, policy, vocabulary, runner_vocabulary, runner_ir, ir, app_artifact, startup and guarantees (one {profile, verdict} per requested profile). When the captured IR inventory is not the manifest’s reviewed policy, no artifact is written and the command fails.

run

lema run --runtime CONFIG --artifact NAME [--release ID --store DIR --deployment FILE] [--manifest FILE] [--input FILE] [ARG ... | -- ARG ...]
lema run --runtime CONFIG --artifact NAME --deployment DIR [--release ID --store DIR] [--manifest FILE] [--input FILE]

Checks the artifact artifacts/NAME again and runs it once. An execution artifact runs in the sandbox with no network. An app artifact runs in the application sandbox, which shares the host’s network, inside its deployment directory. The program’s output goes to standard output as bytes. A summary goes to standard error:

lema: ran NAME (KIND, BACKEND, artifact ARTIFACT-ID) in SECONDSs as CALL; N output bytes (tested execution)

With --release, the ID is a 64-hex release ID recorded in the store and not withdrawn; a name is refused. Every binding of the release is re-derived before the run. Standard error first gets a line naming the selected release; when newer releases supersede it, the line says the run is a rollback. An execution artifact takes --deployment FILE only with --release. A capability application’s release (kind cap-app) has no run command.

The program’s arguments are the positional words after run followed by the words after --. Only a cli entry takes arguments. A vectors entry takes no input and no arguments, and an app entry takes only an input.

test

lema test --manifest FILE --store DIR --runtime CONFIG --name NAME [--lean DIR] [--input FILE] [--cap NAME --deployment DIR] [ARG ... | -- ARG ...]

Builds the manifest for each backend it lists (artifacts NAME-lean, NAME-lean-native), runs each once and compares the outputs byte for byte with each other, and with the manifest’s expect when it has one. It prints the report, which is labelled tested. A failed comparison is an error that carries the report.

--cap and --deployment are required together for an app entry and refused for any other.

cap-build

lema cap-build --runtime CONFIG --name NAME --staticlib PATH

Builds a capability artifact artifacts/NAME from the tool’s platform module and glue and the shim library, in two native calls: the module’s compile and the development library’s link.

The output is {"directory": …, "id": …, "status": "built"}.

Actors

Both commands open the store directly, so the server must be stopped.

actor add

lema actor add --store DIR --id ID [--operator]

Registers an actor and prints its new random token once. The store keeps only the token’s SHA-256, in actors.json. An existing actor is refused: tokens are not rotated in this version.

The output is {actor, note, operator, token}.

actor list

lema actor list --store DIR

Prints [{id, operator}], without token digests.

Projects

These commands are clients. Each builds one request and sends it to the server (snapshot sends two). Their records are described on the store records page.

ref create, publish-revision, adopt-policy and review send the actor’s token. They read it from the first line of --token-file FILE, or else from LEMA_ACTOR_TOKEN. There is no flag that takes the token itself.

snapshot

lema [--socket PATH] snapshot [--aliases PREFIX] [--roots ID,..] [--exports-file FILE] [--authoring ID,..] [--assets KIND=PATH,..]

Creates a binding map, then a snapshot over it.

The output is {bindings, created, snapshot}.

revision

lema [--socket PATH] revision create --after SNAPSHOT --intent TEXT [--parents REV,..] [--base REV] [--evidence-file FILE] [--obligations-file FILE] [--discharged-file FILE]
lema [--socket PATH] revision show REV
lema [--socket PATH] revision log REV [--limit N]

create records a revision, show prints one with its after-snapshot and the references that name it, and log prints a revision and its ancestors.

policy create

lema [--socket PATH] policy create --file FILE

Sends the JSON in FILE as the params of policy.create. --file is required.

ref

lema [--socket PATH] ref create --name NAME --policy POLICY --actor ID [--token-file FILE] [--idempotency-key K]
lema [--socket PATH] ref list [--prefix P]

create makes a project reference at the empty initial state under a policy of version 1; the actor must be an operator. list prints every reference, or with --prefix those whose names start with P, each with the revision, policy, policy version and generation that the next move expects.

publish-revision and adopt-policy

lema [--socket PATH] publish-revision --ref NAME --revision REV --expect-revision REV|none --expect-generation G --expect-policy-version V --actor ID [--reset] [--evidence ID,..] [--reviews ID,..] [--idempotency-key K] [--token-file FILE]
lema [--socket PATH] adopt-policy --ref NAME --policy POLICY --expect-revision REV|none --expect-generation G --expect-policy-version V --actor ID [--evidence ID,..] [--reviews ID,..] [--idempotency-key K] [--token-file FILE]

publish-revision moves a reference to a revision under its active policy. adopt-policy moves it to the next version of its policy.

review

lema [--socket PATH] review --ref NAME --revision REV|--policy POLICY --decision approve|reject [--note TEXT] [--display DIGEST] --actor ID [--token-file FILE]

Records a review of a reference’s move under its active policy. Exactly one of --revision (for a publication or reset) and --policy (for an adoption) is given. --decision is approve or reject. --note adds text, and --display binds the digest of the approval view the reviewer read (from lema site build). --ref, --decision and --actor are required.

log

lema [--socket PATH] log --ref NAME [--limit N]
lema [--socket PATH] log --revision REV [--limit N]

Prints a reference’s recorded moves (newest first) or a revision’s ancestry. Exactly one of --ref and --revision is given.

report and merge

lema [--socket PATH] report --revision REV
lema [--socket PATH] report --ref NAME [--generation G]
lema [--socket PATH] report --after SNAPSHOT [--before SNAPSHOT]
lema [--socket PATH] merge --parents REV,REV,.. --base REV [--resolve-file FILE]

report prints a change report of a revision, of one recorded move of a reference, or between two snapshots. Exactly one of --revision, --ref and --after is given. --generation picks the move; the default is the latest. Without --before, the comparison starts from the empty state.

merge compares the parents’ after-snapshots with the base’s and stores a merge record. --parents and --base are required. --resolve-file is a JSON object of resolutions, with the fields exports, assets, renames and authoring.

Releases

lema release create     --store DIR --runtime CONFIG --artifact NAME --deployment FILE|DIR [--bundles ID,..] [--doc TEXT]
lema release show       --store DIR --release ID
lema release list       --store DIR
lema release verify     --store DIR --runtime CONFIG --release ID --artifact NAME [--deployment FILE|DIR] [--lean DIR]
lema release select     --store DIR --runtime CONFIG --release ID --artifact NAME --deployment FILE|DIR
lema release withdraw   --store DIR --release ID --reason TEXT
lema release supersede  --store DIR --release ID --by ID [--reason TEXT]
lema release deployment --deployment FILE|DIR [--input]

Each subcommand but deployment calls the release method of the same name on a store it opens itself (show calls release.get); deployment computes the digest without a store. The record is described on the store records page. All flags are checked before the store or runtime is opened. Only create, verify and select load the runtime, for its artifacts/. Paths are made absolute before the call. No subcommand makes a native call.

For an app artifact’s deployment directory, the digest is of its lema-cap.json. release deployment prints {sha256}, the deployment configuration’s digest. With --input it also prints input, the private configuration, which holds credential references and never their values.

Site

lema site build --store DIR --out DIR [--ref NAME ..] [--release ID ..] [--review REF=revision:ID|REF=policy:ID ..] [--llms] [--max-bytes N] [--max-files N] [--max-objects N] [--history N]

Writes static pages of the selected references, releases and pending reviews from a store it opens itself: plain HTML with no script, with Markdown and JSON beside each page. --out is a new or empty directory, or one a site was written to before.

Each limit is a positive integer. A site over --max-bytes, --max-files or --max-objects is refused. The output is {bytes, files, out, refs, releases, reviews}. Building the pages is described in build static inspection pages.

Retired commands still in the binary

Decision 0033 retires the HTTP v1 chain and the M3/M4 apps (kv, ledger, fanout) with the lema-host workers. These three commands still exist at HEAD. --backend rust is the Rust backend, on hold under decision 0029.

http-build

lema http-build --store DIR --runtime CONFIG --name NAME [--http DIR] [--variant list|bytes|web|kv|ledger|fanout] [--backend lean|lean-native|rust]

Builds the HTTP worker artifact from the accepted execution roots. --store, --runtime and --name are required. --http defaults to lean/http, --variant to list and --backend to lean.

http-matrix

lema http-matrix --runtime CONFIG --artifact NAME --out FILE [--modes M,..] [--http DIR] [--variant list|bytes]

Checks an artifact, then runs HTTP v1’s matrix modes against it, one worker each, and writes one result line per mode to --out, which must not exist. --modes defaults to every mode. The web and actor variants are refused.

host

lema host --runtime CONFIG --artifact NAME [--listen ADDR] [--workers N] [--codec] [--http DIR] [--variant list|bytes|web|kv|ledger|fanout] [--mailbox N] [--state DIR] [--snapshot-every N] [--reorder]

Checks an artifact, then serves it through the execution host until standard input closes; connection reports go to standard output. --listen defaults to 127.0.0.1:8080. --mailbox, --state and --snapshot-every are for the actor apps only, and --reorder for kv only.

Related

• Server methods
• Runtime configuration
• Requirements and environment variables