Run the test suites

Run the plain checks anywhere, the pinned-Lean local checks where Lean is installed, and native suites on a runtime.

Lema’s checks come in three tiers. The plain tier needs only Rust. The local checks also run the pinned Lean, directly. The native suites run through the trusted runtime, and only when you name a runtime configuration for them.

The merge gate is the plain tier plus the local checks of the Lean a change touches. Native suites run only when something that could change acceptance changed, such as submitted Lean, trusted code, the toolchain, the pins, the identity rules or the suite itself (decision 0033).

Before you start

• A checkout set up as in Set up a machine for Lema. scripts/cloud-setup.sh installs the pinned Rust (1.98.0) and Lean, and writes ~/.lema/env.
• Node 20.19 or later, for the OpenSpec check.
• For native suites, a machine where lema check-runtime passes (step 4), and ~/.lema/env loaded so that $LEMA_RUNTIME_BASE is set.

1. Run the plain tier

cargo fmt --check
cargo clippy --workspace --all-targets
cargo test --workspace --exclude lema-backend --exclude lema-spike

These need no Lean and no runtime. Among them, crates/lema-core/tests/identity.rs pins object identities, which must never change silently. The parked Rust backend’s suites run only on request, with cargo test -p lema-backend -p lema-spike.

2. Validate the specifications

npm ci --ignore-scripts
npm run check

npm run check validates the OpenSpec specifications in openspec/ and nothing else.

3. Run the pinned-Lean local checks

LEMA_LOCAL_LEAN names the pinned lean binary, and ~/.lema/env sets it. Tests that read it run Lean directly, outside the sandbox and the store:

source ~/.lema/env
cargo test -p lema-cli --test contract_view_local -- --nocapture

A local check is “checked locally”, not accepted: nothing enters a store. Some other local checks take a distribution root instead: LEMA_STRUCTURES_LEAN_ROOT, or LEMA_CAP_LEAN_ROOT with LEMA_CAP_SMOKE=1 or LEMA_RUNNER_LOCAL=1. They are listed in Requirements and environment variables.

4. Check that the machine can run native suites

A fault latches the output it happens in, so give the check an output of its own:

mkdir -p ~/.lema/runs && mkdir -m 700 ~/.lema/runs/probe
jq --arg out "$HOME/.lema/runs/probe" '.output = $out' $LEMA_RUNTIME_BASE > ~/.lema/runs/probe.json
lema check-runtime --runtime ~/.lema/runs/probe.json

The command loads the runtime and makes one small native call under the full controls.

• Exit 0: the call ran.
• Exit 75: busy. Another call holds the lock (the command waits up to 10 minutes for it), or the host is loaded. If the message reports low available memory, free some: a call needs 6 GiB available.
• Any other failure names what differs, such as the pinned host files or the systemd user scopes. On such a machine the plain tier and the local checks still run, and native suites run elsewhere.

5. Give each native suite its own output

A supervision fault writes a HALTED latch in the output where it happens, and that stops later calls there. So give each suite run a runtime configuration with a fresh output. Copy the base configuration in $LEMA_RUNTIME_BASE and change output, for example:

{"schema": "lema.runtime-linux/v2", "distribution": "/path/to/dist", "output": "/home/you/.lema/runs/exec-1", "shared_lock": "/home/you/.lema/native.lock"}

Create the output directory with mode 0700 first. Keep distribution and shared_lock as they are in the base configuration.

6. Run a native suite

Each suite is enabled by an environment variable that names a runtime configuration:

LEMA_EXEC_RUNTIME=/home/you/.lema/runs/exec-1.json \
  cargo test -p lema-cli --test exec_manifest -- --test-threads=1 --nocapture

Run native suites with -- --test-threads=1 on a quiet host.

• Some suites also need a store variable, such as LEMA_JSON_CHECK_STORE.
• The capability suites need liblema_cap.a built first in the same profile (cargo build -p lema-cap), or named in LEMA_CAP_STATICLIB.
• The variables, one per suite, are in Requirements and environment variables. The README’s list also names suites of the HTTP v1 chain and the M3/M4 apps, which decision 0033 retires.

7. Read the result

A suite whose variable is unset returns at once, and cargo reports it as passed. Some suites then print a skipped line, which you see with --nocapture, but many print nothing. A skipped test is not native evidence, so check that the variable was set before you count a pass.

If a run halts, the output’s HALTED latch stops later calls until you resolve it. A failed scope cleanup latches the whole host instead, beside the shared lock. See Recover from a HALTED latch.

When a native suite backs a change, record the run in the pull request: the suite, commit, native calls, time and result.