Requirements and environment variables
What a machine needs to build lema and to make native calls, and every environment variable the tools and test suites read.
Building lema, running cargo test and the pinned-Lean local checks need only the toolchains below. Native calls (every acceptance by the pinned Lean 4.34.1 kernel, and every build and run of an artifact) also need the host below, and lema check-runtime reports whether a machine has it. Setting a machine up is the set-up tutorial.
Host
| Requirement | Detail |
|---|---|
| Operating system | Linux on x86_64. Target x86_64-unknown-linux-gnu, host kind linux-x86_64-bwrap-systemd-scope-v1. |
| Sandbox | bubblewrap at /usr/bin/bwrap. |
| Scopes | systemd-run --user and systemctl --user at /usr/bin, with the cpu, memory and pids cgroup controllers delegated to the user manager. The runtime reads /sys/fs/cgroup/user.slice/user-UID.slice/user@UID.service/cgroup.controllers before each call. |
| Pressure information | /proc/meminfo, /proc/pressure/memory and /proc/pressure/cpu. |
| Memory | At least 6 GiB available before each call. Each call runs in 4 GiB with no swap. |
| Disk | At least 4 GiB free on the runtime output’s file system and on the shared lock’s. |
| File system layout | Merged /usr: /bin and /sbin link to usr/bin, /lib and /lib64 to usr/lib, and /usr/lib/libcap.so.2 to libcap.so.2.78. |
The limits are described in full on the runtime configuration page.
Pinned host files
Twelve host files are pinned by SHA-256 in crates/lema-check/src/pins.rs (HOST_PINS): the sandbox and systemd tools and the shared libraries that Lean, bubblewrap and the systemd tools link. Each must be a regular file owned by root, not writable by group or others, with this digest. They are the files of the project’s trusted runner host, in Arch Linux’s merged-/usr layout.
| Path | SHA-256 |
|---|---|
/usr/bin/bwrap | 7c44…4762 |
/usr/bin/systemd-run | e14f…6339 |
/usr/bin/systemctl | afe9…3255 |
/usr/lib/ld-linux-x86-64.so.2 | d011…1bfb |
/usr/lib/libc.so.6 | e221…ffff |
/usr/lib/libm.so.6 | 9651…999d |
/usr/lib/libpthread.so.0 | 839b…31ab |
/usr/lib/libdl.so.2 | 9b38…d03c |
/usr/lib/librt.so.1 | e06e…e5f8 |
/usr/lib/libcap.so.2.78 | 5a9c…c6a1 |
/usr/lib/libgcc_s.so.1 | e618…716a |
/usr/lib/systemd/libsystemd-shared-261.2-1.so | a913…d6f5 |
At HEAD 5a94951 a mismatch refuses loading the runtime and every native call, with host executable/library drift: PATH. A package update on the host therefore stops native calls until the pins are reviewed and updated. Receipts record the pins’ digest as host_pins_sha256 in their checker block. Decision 0033 plans to record the pins rather than enforce them, keeping the ownership checks; that change is not in the code yet.
Toolchains
Rust
Rust 1.98.0, pinned by rust-toolchain.toml. scripts/cloud-setup.sh installs it through rustup with the rustfmt and clippy components. cargo build --release builds target/release/lema.
Lean
The pinned Lean distribution is the official Lean 4.34.1 Linux archive, extracted read-only with the committed manifest beside it.
| Item | Value |
|---|---|
| Version | 4.34.1 |
| Git hash | 5045d0056413266e57c625dcd7c365b10e377c52 |
| Archive | lean-4.34.1-linux.tar.zst |
| Archive SHA-256 | 47bf4bbd78f70c2e9670598ab7124d92b6efb7330ff33e5fbb4030f6fd72e4e4 |
| Manifest | toolchain/lean-4.34.1-linux.extraction-manifest.json (schema lema.lean-distribution/v1), copied into the distribution as extraction-manifest.json |
| Manifest SHA-256 | c82b7b44dd02daae5aa46c3f7e0a1e564da1a183fd81c021f299370a51d297a5 |
bin/lean SHA-256 | e8baaa71855a616dc351028f3ad2200051b0671f423a1696a100e809302d5550 |
| Contents | the directory lean-4.34.1-linux/, 17,738 files and 12 symlinks |
https://github.com/leanprover/lean4/releases/download/v4.34.1/lean-4.34.1-linux.tar.zstEvery file and directory of the distribution must belong to root or the running user and must not be writable by group or others. lema verify-distribution DIR checks a distribution against these pins, and so does every load of a runtime. Installing it by hand is covered in install the pinned Lean.
Build tools
scripts/cloud-setup.sh needs curl, tar, zstd, git and a C compiler (cc). When one is missing and apt-get is available as root or through sudo, it installs curl, ca-certificates, tar, zstd, git and build-essential. It also tries to install bubblewrap when bwrap is missing, and carries on if that fails.
Environment variables
Client and actors
| Variable | Read by | Meaning |
|---|---|---|
LEMA_SOCKET | every command that uses a socket | The server’s socket when --socket is not given. Without either: lema.sock in the current directory. |
LEMA_ACTOR_TOKEN | ref create, publish-revision, adopt-policy, review | The acting actor’s token when --token-file is not given. The token is never taken from the command line. |
Setup
scripts/cloud-setup.sh reads three optional variables.
| Variable | Meaning |
|---|---|
LEMA_HOME | Where toolchains, runtime configurations and env go. Default: ~/.lema. |
LEMA_DIST | An absolute path to an extracted distribution to use instead of downloading one. It must hold the committed manifest as extraction-manifest.json. |
LEMA_SETUP_PREBUILD | 0 skips prebuilding the workspace’s tests. |
It writes $LEMA_HOME/env, a file to source, which sets:
| Variable | Value |
|---|---|
PATH | Adds ~/.cargo/bin and Cargo’s target/release. |
LEMA_DIST | The distribution the script checked, by default $LEMA_HOME/toolchains/lean-4.34.1-linux-x86_64. |
LEMA_LOCAL_LEAN | The pinned lean binary in that distribution. |
LEMA_NATIVE | yes, busy or no: what lema check-runtime reported (exit 0, 75 or anything else). |
LEMA_RUNTIME_BASE | $LEMA_HOME/runtime.json, the base runtime configuration (output $LEMA_HOME/evidence, lock $LEMA_HOME/native.lock). |
The setup’s own check-runtime call runs in a fresh output under $LEMA_HOME/checks/.
Set by the runtime
Inside the application sandbox, LEMA_CAP_CONFIG names the deployment directory’s lema-cap.json, which the capability shims read.
Local checks without the runtime
These run the pinned toolchain directly, with no scope, lock or ledger. What they show is tested, not native acceptance.
| Variable | Meaning | Read by |
|---|---|---|
LEMA_LOCAL_LEAN | The pinned lean binary. | crates/lema-cli/tests/contract_view_local.rs, fueled_call_graph.rs |
LEMA_CAP_SMOKE | 1 runs the capability boundary’s smoke test, with LEMA_CAP_LEAN_ROOT. | crates/lema-cap/tests/smoke.rs |
LEMA_CAP_LEAN_ROOT | The distribution root holding bin/lean and bin/leanc. | smoke.rs, crates/lema-cap/tests/runner.rs |
LEMA_RUNNER_LOCAL | 1 runs the runner’s boundary suite locally, with LEMA_CAP_LEAN_ROOT. | crates/lema-cap/tests/runner.rs |
LEMA_STRUCTURES_LEAN_ROOT | The distribution root holding bin/lean: checks lean/std/ReceivedStructuresCheck.lean. | crates/lema-check/tests/structure_emulation.rs |
LEMA_CAP_STATICLIB | The path of liblema_cap.a. Without it, the tests use the one cargo build -p lema-cap wrote in the same profile’s target directory. | smoke.rs, runner.rs, crates/lema-cap/tests/native.rs, crates/lema-cli/tests/standalone.rs |
Native suites
A native suite runs only when its variable names a runtime configuration. Each run gets its own output, because a fault latches the output it happens in. README.md runs them with -- --test-threads=1 on a quiet host. Test files are under crates/.
The last column marks suites of retired or on-hold parts. Decision 0033 retires the HTTP v1 chain in lean/http, the HTTP v2 server in lean/web, the M3/M4 apps kv, ledger and fanout, and the lema-host execution host, with roughly 23 native suites. Decision 0029 puts the Rust backend on hold. The files of these suites are still in the tree at HEAD. A suite that only takes the HTTP v1 draft as an input (LEMA_SCALE_HTTP_DRAFT) is not marked.
| Variable | Runs | Companions | Retired or on hold |
|---|---|---|---|
LEMA_RUNTIME | lema-check/tests/native.rs: native calls on an ordinary output, with a small leanc link | ||
LEMA_FAULT_RUNTIME | lema-check/tests/native.rs: a deliberate timeout | ||
LEMA_WORKER_FAULT_RUNTIME | lema-check/tests/native.rs: a worker fault | ||
LEMA_WORKER_STALL_RUNTIME | lema-check/tests/native.rs: a worker that stops reading | ||
LEMA_WORKER_FLOOD_RUNTIME | lema-check/tests/native.rs: a worker that floods its output | ||
LEMA_REPLAY_RUNTIME | lema-check/tests/replay.rs: kernel replay of canonical objects | ||
LEMA_MODULES_RUNTIME | lema-check/tests/incremental.rs: incremental replay through modules, on a fresh output | ||
LEMA_E2E_RUNTIME | lema-cli/tests/e2e.rs: Core, then a client through Received.*, then queries | ||
LEMA_DATA_RUNTIME | lema-cli/tests/data.rs, families.rs: fixed-width integers and money, single self-recursive families | ||
LEMA_BYTES_RUNTIME | lema-cli/tests/bytes.rs: lean/data/Bytes.lean and the forbidden-API list | ||
LEMA_CORE_V2_RUNTIME | lema-cli/tests/core_v2.rs: Core v2 | LEMA_SCALE_HTTP_DRAFT | |
LEMA_HANDLES_RUNTIME | lema-cli/tests/handles.rs: handle-map contracts | ||
LEMA_SUMS_RUNTIME | lema-cli/tests/sums.rs: effect sums | ||
LEMA_ACTOR_RUNTIME | lema-cli/tests/actor.rs: a certified actor with a bounded mailbox | ||
LEMA_ESCROW_RUNTIME | lema-cli/tests/escrow.rs: the escrow protocol | ||
LEMA_DURABLE_RUNTIME | lema-cli/tests/durable.rs: durable actors | ||
LEMA_PARALLEL_RUNTIME | lema-cli/tests/parallel.rs: programs over disjoint handles | ||
LEMA_TICKETS_RUNTIME | lema-cli/tests/tickets.rs: tickets and spawned tasks | ||
LEMA_CHANNELS_RUNTIME | lema-cli/tests/channels.rs: session channels | ||
LEMA_REPLACE_V2_RUNTIME | lema-cli/tests/replace_v2.rs: checked replacement with a Core v2 claim | ||
LEMA_REUSE_RUNTIME | lema-cli/tests/reuse.rs: minimal parametric reuse | ||
LEMA_RECEIVED_RUNTIME | lema-cli/tests/received_families.rs: received families | ||
LEMA_RECEIVED_STRUCTURES_RUNTIME | lema-cli/tests/received_structures.rs: received structures, about 11 calls | ||
LEMA_BUNDLE_RUNTIME | lema-cli/tests/bundles.rs: bundles | ||
LEMA_PROTECTED_RUNTIME | lema-cli/tests/protected.rs: protected references, about 15 calls | ||
LEMA_VIEW_RUNTIME | lema-cli/tests/contract_view.rs: the contract view’s round trip | LEMA_SCALE_HTTP_DRAFT | |
LEMA_STD_TEXT_RUNTIME | lema-cli/tests/std_text.rs: Std.Text | ||
LEMA_STD_MAP_RUNTIME | lema-cli/tests/std_map.rs: Std.Map | ||
LEMA_STD_JSON_RUNTIME | lema-cli/tests/std_json.rs: Std.Json part 1 | ||
LEMA_STD_FIXED_RUNTIME | lema-cli/tests/std_fixed.rs: fixed-point arithmetic | ||
LEMA_STD_INTERVAL_RUNTIME | lema-cli/tests/std_interval.rs: rescaling, square root, intervals | ||
LEMA_STD_SHA256_RUNTIME | lema-cli/tests/std_sha256.rs: the SHA-256 specification | ||
LEMA_STD_BYTES_RUNTIME | lema-cli/tests/std_bytes.rs: Std.Bytes | ||
LEMA_STD_SHA256_IMPL_RUNTIME | lema-cli/tests/std_sha256_impl.rs: Std.Sha256 | ||
LEMA_STD_HMAC_RUNTIME | lema-cli/tests/std_hmac.rs: HMAC-SHA256 | ||
LEMA_STD_SIGV4_RUNTIME | lema-cli/tests/std_sigv4.rs: AWS Signature Version 4 | ||
LEMA_JSON_RUNTIME | lema-cli/tests/json.rs, then json_runs.rs: the JSON codec | LEMA_JSON_STORE (for json_runs.rs) | |
LEMA_JSON_NUMBERS_RUNTIME | lema-cli/tests/json_numbers.rs: JSON numbers | LEMA_JSON_NUMBERS_STORE | |
LEMA_JSON_GRAMMAR_RUNTIME | lema-cli/tests/json_grammar.rs: the JSON grammar | LEMA_JSON_GRAMMAR_STORE | |
LEMA_JSON_CHECK_RUNTIME | lema-cli/tests/json_check.rs: the JSON check program, about 9 calls | LEMA_JSON_CHECK_STORE | |
LEMA_EXEC_RUNTIME | lema-cli/tests/exec_manifest.rs: lema build, run and test in both backends, about 27 calls | ||
LEMA_RELEASE_RUNTIME | lema-cli/tests/release.rs: a release created, verified, selected, run and withdrawn, about 11 calls | ||
LEMA_SITE_RUNTIME | lema-cli/tests/site.rs: lema site build on real receipts, about 10 calls | ||
LEMA_CAP_RUNTIME | lema-cap/tests/native.rs: the capability platform, six calls | LEMA_CAP_STATICLIB | |
LEMA_RUNNER_RUNTIME | lema-cap/tests/runner.rs: the runner’s boundary suite, six calls | LEMA_CAP_STATICLIB | |
LEMA_STANDALONE_RUNTIME | lema-cli/tests/standalone.rs: a capability app built, tested, run and released, about 19 calls | LEMA_CAP_STATICLIB | |
LEMA_SCALE_RUNTIME | lema-cli/tests/scale.rs: one store accepting Core, a client and the migrated HTTP proofs, a restart, reverify | LEMA_SCALE_HTTP_DRAFT | |
LEMA_HTTP_RUNTIME | lema-http/tests/native.rs: the HTTP artifact build and matrix modes | LEMA_HTTP_STORE | retired: HTTP v1 |
LEMA_LEAN_NATIVE_RUNTIME | lema-http/tests/native_lean.rs: the lean-native backend on the HTTP artifacts | LEMA_HTTP_STORE | retired: HTTP v1 |
LEMA_HTTP_BYTES_RUNTIME | lema-cli/tests/http_bytes.rs: the byte-array HTTP parser | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v1 |
LEMA_REPLACE_RUNTIME | lema-cli/tests/replace.rs: checked replacement of the HTTP v1 parser | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v1 |
LEMA_HANDLE_DRIVER_RUNTIME | lema-cli/tests/handle_driver.rs: the HTTP driver on handle contracts | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v1 |
LEMA_INTERLEAVED_RUNTIME | lema-cli/tests/interleaved.rs: interleaved HTTP connections | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v1 |
LEMA_WEB_RUNTIME | lema-cli/tests/web.rs: HTTP v2 | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v2 (lean/web) |
LEMA_KEEP_RUNTIME | lema-cli/tests/keep_alive.rs: keep-alive | LEMA_SCALE_HTTP_DRAFT | retired: HTTP v2 (lean/web) |
LEMA_KV_RUNTIME | lema-cli/tests/kv.rs: the item store app | LEMA_KV_STORE, LEMA_SCALE_HTTP_DRAFT | retired: kv app |
LEMA_LEDGER_RUNTIME | lema-cli/tests/ledger.rs: the sharded ledger | LEMA_SCALE_HTTP_DRAFT | retired: ledger app |
LEMA_FANOUT_RUNTIME | lema-cli/tests/fanout.rs: the fan-out app | LEMA_SCALE_HTTP_DRAFT | retired: fanout app |
LEMA_HOST_RUNTIME | lema-host/tests/: native.rs and replace.rs, web.rs, kv.rs, ledger_app.rs, fanout_app.rs | LEMA_HTTP_STORE, LEMA_WEB_STORE, LEMA_KV_STORE, LEMA_LEDGER_STORE or LEMA_FANOUT_STORE; LEMA_HOST_BACKEND (lean-native or rust) | retired: lema-host |
LEMA_SCALING_RUNTIME | lema-host/tests/scaling.rs: throughput and latency measurements, with no target | retired: lema-host | |
LEMA_BACKEND_RUNTIME | lema-http/tests/backend_native.rs: one Rust execution artifact | LEMA_BACKEND_STORE, LEMA_BACKEND_VARIANT (list, bytes, web or kv) | on hold: Rust backend |
LEMA_BACKEND_VECTORS_RUNTIME | lema-cli/tests/backend_vectors.rs: runtime vectors published and replayed | on hold: Rust backend | |
LEMA_BACKEND_JSON_RUNTIME | lema-cli/tests/backend_vectors.rs: JSON and framing vectors | LEMA_BACKEND_JSON_STORE | on hold: Rust backend |
LEMA_BACKEND_BENCH_RUNTIME | lema-host/tests/backend_measurements.rs: Lean and Rust artifacts measured in one session, with no target | LEMA_HTTP_STORE | on hold: Rust backend |
A *_STORE companion names a store a previous suite left, and LEMA_SCALE_HTTP_DRAFT names the migrated HTTP v1 draft. A few gated suites read variables that README.md does not list: LEMA_EVOLVE_RUNTIME (evolve.rs), LEMA_FUELED_RUNTIME (fueled_call_graph.rs), LEMA_REPLACE_GENERIC_RUNTIME (replace_generic.rs), LEMA_STD_CANONICAL_RUNTIME (std_canonical.rs), LEMA_STD_FINITE64_RUNTIME (std_finite64.rs), LEMA_STD_SHA256_UNBOXED_RUNTIME (std_sha256_unboxed.rs), LEMA_EXEC_SHA256_UNBOXED_RUNTIME (exec_sha256_unboxed.rs) and LEMA_CAP_PUBLISH_RUNTIME (cap_publish.rs), all under crates/lema-cli/tests/. Running the suites is covered in run the test suites.
Written against lema-lang at commit 5a94951, 17 Oct 2026.