Build a native executable

Compile an execution manifest's accepted closure into a native executable linked by leanc, then run it in the sandbox.

An execution manifest builds with one of two backends. lean runs the compiled module under lean --run, in Lean’s IR interpreter. lean-native compiles the same module to C and links it with the pinned distribution’s leanc. This guide builds the lean-native executable of lean/exec/sha256-digest.json.

Before you start

• A runtime configuration.
• A store in which every root of the manifest is accepted. For lean/exec/sha256-digest.json, publish lean/std/Sha256Spec.lean (prefix LemaDraft, seed salt lean/std/Sha256Spec), then lean/std/Sha256Exec.lean (seed salt lean/std/Sha256Exec) with Received.digest and Received.msg448 bound to the specification’s, as crates/lema-cli/tests/exec_manifest.rs does. For a guided first build, see Build and run a program.
• The server stopped. lema build and lema test open the store directly.
• A shell at the repository root. Pieces are read from lean/, or from the directory --lean DIR names.
• In the commands, $STORE is the store directory and $CONFIG your runtime configuration.

1. Check that the manifest lists the backend

"backends": ["lean", "lean-native"],

Without --backend, lema build uses the first backend the manifest lists. A backend the manifest does not list is refused (does not list the lean-native backend).

2. Build

lema build --manifest lean/exec/sha256-digest.json --store $STORE --runtime $CONFIG \
  --name sha-digest-native --backend lean-native

The build makes three native calls, named after --name:

1. sha-digest-native: one Lean call elaborates the module, writes Run.olean, exports the roots and writes the module’s C (Run.c).
2. sha-digest-native-launcher: compiles the fixed launcher to Launcher.c.
3. sha-digest-native-link: the distribution’s leanc links worker with its own clang, ld.lld and sysroot. Nothing from the host’s compilers is used.

Before it writes the artifact, the build checks that:

• the roots compile to exactly their accepted closure;
• the compiled IR passes the executable vocabulary;
• every constant the executable evaluates at startup is reached by the roots;
• every profile the manifest asks for holds.

It prints a JSON summary with "status": "built", the backend, the artifact’s directory (under artifacts/ in the configuration’s output) and its ID.

3. Run it

lema run --runtime $CONFIG --artifact sha-digest-native --input FILE -- hello

lema run verifies every file of the artifact against its manifest, then runs worker once in the sandbox, with no network. The program’s output goes to standard output, and a summary line (backend, artifact ID, time, output size) goes to standard error. A cli entry takes an input of at most 64 MiB and the words after --. A vectors entry takes neither. Add --manifest FILE to also require that the artifact was built from that manifest.

4. Compare with the default backend

lema test --manifest lean/exec/sha256-digest.json --store $STORE --runtime $CONFIG \
  --name sha-digest-test --input FILE -- hello

lema test builds every listed backend (artifacts sha-digest-test-lean and sha-digest-test-lean-native), runs each once and compares the outputs byte for byte. When the manifest has expect.output_sha256, it compares against that too.

When a build is refused

A constant evaluated at startup that the roots do not reach is refused by name. Make it a root with its accepted ID, or remove it from the pieces.

What is checked, tested and assumed

The roots are checked: the store accepted them with receipts from the pinned Lean 4.34.1 kernel. The executable’s behaviour is tested: crates/lema-cli/tests/exec_manifest.rs (LEMA_EXEC_RUNTIME) builds and runs both backends, and lean/exec/README.md records that it passed natively on 16 and 17 Oct 2026. leanc, clang, ld.lld, the Lean runtime, glibc and Linux are assumed, like Lean’s compiler.

Limits of the native path:

• A vectors or cli executable still imports Lean, because the exporter shares its compilation, so it is about 120 MB.
• lean --run’s --memory=4096 has no counterpart in the executable. Its memory is bounded only by the scope’s 4 GiB limit, and running out kills the scope.
• A constant the roots reach is evaluated when the executable starts, before main.

The README also describes lema http-build --backend lean-native, which builds workers for the HTTP v1 chain. Decision 0033 retires that chain, so build programs from an execution manifest instead.