Set up a machine for Lema

Install the pinned Rust and Lean from a lema-lang checkout, then find out whether this machine can run native calls.

By the end of this tutorial you will have Rust, the pinned Lean 4.34.1 and a release build of lema installed, and a file of environment variables to load in each shell. You will also know whether this machine can run the native runtime that the other four tutorials need.

You need:

• a checkout of lema-lang (the repository is private, so these pages assume you have one);
• Linux on x86_64;
• apt-get with root or passwordless sudo, or else curl, tar, zstd, git and a C compiler already installed;
• jq 1.6 or later, which these tutorials use to write JSON requests.

What the runtime needs

Each time Lema runs Lean, to read your source or to check it with the pinned Lean 4.34.1 kernel, it makes a native call. In a native call the pinned lean binary runs in a bubblewrap sandbox, inside a systemd user scope with fixed limits. For that, the machine needs:

• /usr/bin/bwrap (bubblewrap) and systemd-run --user, with the cpu, memory and pids cgroup controllers delegated to your user manager;
• the twelve host files pinned by SHA-256 in crates/lema-check/src/pins.rs: the bubblewrap and systemd binaries and the libraries they and Lean link, in Arch Linux’s merged /usr layout;
• at least 6 GiB of memory available when a call starts (each call is limited to 4 GiB), and 4 GiB of free disk where the call writes.

The host files must match their pins exactly. On another Linux distribution, or after one of those packages is updated, they differ and the runtime refuses to run. The setup script can install packages with apt-get, but that does not make a Debian or Ubuntu machine pass. You can still install everything below on such a machine, and the script tells you at the end which case you are in. Requirements has the full list.

Run the setup script

From the root of your checkout, run:

scripts/cloud-setup.sh

The script reads its pins from the checkout, then:

1. Installs curl, tar, zstd, git and the build tools with apt-get if any are missing. It also installs bubblewrap if it can, and carries on if it cannot.
2. Installs Rust 1.98.0, the version rust-toolchain.toml pins, through rustup.
3. Builds lema in release mode. This comes before Lean because lema verify-distribution is the command that checks the Lean download.
4. Downloads the Lean 4.34.1 archive, compares its SHA-256 with the pin, and installs it read-only under ~/.lema/toolchains/ once lema verify-distribution accepts it.
5. Prebuilds the workspace’s tests.
6. Writes a base runtime configuration, makes one native call to find out whether the runtime works here, and writes ~/.lema/env.

The native call in step 6 can wait up to 10 minutes if another native call holds the machine’s lock. You can run the script again at any time: it keeps a toolchain that already passes, needs no secrets, and writes nothing inside the repository except Cargo’s target directory. Everything it installs goes under ~/.lema, and these tutorials assume that location.

The last two lines report the result. On this page and the next ones, /home/you stands for your home directory:

== done: source /home/you/.lema/env
   Rust 1.98.0; Lean /home/you/.lema/toolchains/lean-4.34.1-linux-x86_64 (verified); native runtime: yes

The last word is yes, busy or no. You will come back to it in a moment.

Load the environment

Load the file the script wrote:

source ~/.lema/env

Do this in every new shell you use for Lema. The file sets five variables:

Check that lema is on your path and that the distribution is the pinned one:

lema verify-distribution $LEMA_DIST

/home/you/.lema/toolchains/lean-4.34.1-linux-x86_64: the pinned Lean distribution (17738 files, 12 symlinks; manifest c82b7b44dd02daae5aa46c3f7e0a1e564da1a183fd81c021f299370a51d297a5)

The command compared every file of the distribution with the manifest committed in toolchain/.

Read the runtime result

echo $LEMA_NATIVE

• yes: one native call ran under the full controls: the systemd scope, the sandbox and the pinned lean. You can follow all five tutorials on this machine.
• busy: the call was refused for a reason that may pass. Another native call was running (native calls run one at a time per machine), or the host was short of memory or under load. Wait, then run the check again as in the next section. If the message says available memory is low, free some first, because waiting alone may not help.
• no: the runtime cannot run on this machine. The script printed the refusal, which names what differs. Finish this tutorial, then read If the answer is no.

Run the check yourself

The script wrote a base runtime configuration, which LEMA_RUNTIME_BASE names:

{"schema":"lema.runtime-linux/v2","distribution":"/home/you/.lema/toolchains/lean-4.34.1-linux-x86_64","output":"/home/you/.lema/evidence","shared_lock":"/home/you/.lema/native.lock"}

Every native call writes into its configuration’s output directory: a line in the ledger, ledger.jsonl, before and after the call, plus a work directory and a log. If supervision fails during a call, the runtime writes a HALTED latch there and refuses every later call with that output until you resolve it. So treat this file as a base, and give each run a copy with an output of its own. The copies keep the same shared_lock, so their calls still take turns. Runtime configuration describes every field.

Make a copy with a fresh output and run the check with it:

CHECK=$HOME/.lema/checks/manual-$(date +%s)
mkdir -m 700 $CHECK
jq --arg out $CHECK '.output = $out' $LEMA_RUNTIME_BASE > $CHECK.json
lema check-runtime --runtime $CHECK.json
echo "exit status $?"

The output directory is created with mode 700, because the runtime refuses an output that another user can write to. lema check-runtime loads the runtime as a native call would, checking the configuration, the pinned host files and the whole distribution. Then the pinned lean checks a one-line theorem, 1 + 1 = 2, under the full controls. The exit status gives the result:

On a machine whose bubblewrap is not the pinned build, the result looks like this:

lema: host executable/library drift: /usr/bin/bwrap
exit status 1

If the answer is no

You can still run two kinds of checks on this machine. The Rust tests need no Lean:

cargo test --workspace --exclude lema-backend --exclude lema-spike

The pinned-Lean local checks also run, because they use LEMA_LOCAL_LEAN directly, outside the sandbox. One of them is the contract view’s round trip:

cargo test -p lema-cli --test contract_view_local

These are developer checks, and nothing they do is accepted into a store. Run the test suites lists them all.

You cannot follow tutorials 2 to 5 on this machine. lema serve checks the same pinned host files when it starts, and every publish, test and build is a native call. Each of those pages shows the output of every step, so you can read them now and run them later on a machine that reports yes.

Next

With LEMA_NATIVE=yes, go on to Start a store and a server.