Write a runtime configuration

Point native calls at the pinned Lean distribution, an owner-only output directory and a shared lock, with an optional call budget.

A runtime configuration is a small JSON file that you own, kept outside the repository. lema serve, check-runtime, build, run and test take it as --runtime. Every field is listed in the runtime configuration reference.

Before you start

• A distribution that passes lema verify-distribution, with its path in DIST. If you ran scripts/cloud-setup.sh, that path is in $LEMA_DIST; otherwise see Install the pinned Lean by hand.
• A host that meets the requirements, including the pinned bwrap and systemd-run --user with delegated cgroups.

Steps

1. Create the output directory, readable only by you:

   OUT=$HOME/.lema/runs/first
   mkdir -p $HOME/.lema/runs
   mkdir -m 700 "$OUT"

   The runtime writes everything about its native calls here: the ledger ledger.jsonl, each call’s log and records, work directories, the module cache (modules/) and built artifacts (artifacts/).

2. Create the shared lock file. You need one per machine:

   touch $HOME/.lema/native.lock
   chmod 644 $HOME/.lema/native.lock

   Each native call holds this lock while it runs, and waits up to 600 seconds to get it. Give every configuration on the machine the same lock, so that their calls wait for each other instead of being refused.

3. Write the configuration. Paths must be absolute and contain no ... JSON does not expand ~ or $HOME, so write the paths out. This is how scripts/cloud-setup.sh writes its configurations:

   CONFIG=$HOME/.lema/first.json
   printf '{"schema":"lema.runtime-linux/v2","distribution":"%s","output":"%s","shared_lock":"%s"}\n' \
     "$DIST" "$OUT" "$HOME/.lema/native.lock" > "$CONFIG"
   chmod 644 "$CONFIG"

   The file holds exactly these four fields, plus call_budget if you add one. The output must not overlap the distribution, and the lock and the configuration must not be inside it.

4. Optionally, cap the number of native calls with call_budget, a non-negative integer. Only schema v2 takes it:

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

   The budget counts every call ever recorded in this output’s ledger. Once it is used up, native calls are refused with native call budget 40 exhausted. lema --socket $SOCK info reports native_calls_used and native_call_budget.

5. Check that the machine can run native calls. The check makes one real native call and records it in the configuration’s output, so give it a configuration of its own:

   PROBE=$HOME/.lema/probe.json
   mkdir -m 700 $HOME/.lema/runs/probe
   printf '{"schema":"lema.runtime-linux/v2","distribution":"%s","output":"%s","shared_lock":"%s"}\n' \
     "$DIST" "$HOME/.lema/runs/probe" "$HOME/.lema/native.lock" > "$PROBE"
   chmod 644 "$PROBE"
   lema check-runtime --runtime "$PROBE"

   It exits 0 when the call ran. It exits 75 when the machine is busy (another call holds the lock, or the host is loaded): try again later. Any other refusal exits 1 with a message that names what differs.

6. Start the server with the configuration ($STORE is your store directory and $SOCK the socket to create):

   lema serve --store $STORE --runtime $CONFIG --socket $SOCK

   Loading hashes the whole distribution again, so the server takes a while to start.

One output per suite run

Treat a configuration as a base, and give each native suite run a copy with a fresh output. A fault latches the output it happens in, and the budget counts one output’s ledger, so separate outputs keep each run’s records, faults and budget apart. A fresh output also starts with an empty module cache, so its first call that needs the decoder module (LemaCodebase) compiles it again.

Do not edit a configuration while a server uses it. Before every native call, the runtime compares the file’s SHA-256 with the one it loaded and refuses with runtime configuration changed. Write a new file and restart the server instead.

Refusals