Build a capability app

Build an app manifest against the capability platform, test it in a deployment and link a standalone binary.

A capability app is a pure Core v2 program. It reaches the outside world only through the four primitives in lean/cap/LemaCap.lean (HTTPS, files, credentials and the clock), and it never calls them itself: the trusted runner, lean/cap/Runner.lean, carries out its commands. How programs reach the outside world explains the design. This guide builds the repository’s example, lean/exec/fanfiles-app.json.

Before you start

• A runtime configuration.
• A store that holds Core v2 and the example app. With prefix LemaDraft, publish lean/core/CoreV2.lean (seed salt lean/core, with the seeds of lean/core/seeds.json). Then publish lean/cap/AppCmd.lean followed by lean/cap/FanFiles.lean as one source (seed salt lean/cap/AppCmd), with Received.Prog, Received.call and Received.ret bound to Core v2’s Prog, Prog.call and Prog.ret. crates/lema-cli/tests/standalone.rs makes exactly these two requests.
• The server stopped. lema build and lema test open the store directly.
• A shell at the repository root.
• In the commands, $STORE is the store directory and $CONFIG your runtime configuration.

lean/exec/collector-app.json does not build yet, so use the FanFiles manifest.

1. Write the app as a task table

An app is a function Nat → ByteArray → Prog AppCmd AppReply ByteArray. Task 0, run on the input, is the main program, and its result is the run’s output:

/-- The application's task table: task 0 is the main program. -/
def app (task : Nat) (input : ByteArray) : Received.Prog AppCmd AppReply ByteArray :=
  if task = 1 then child input else main input

The commands in lean/cap/AppCmd.lean are https, file, credential and clock, which the primitives answer, and start, await, cancel and spawn, which run other tasks. The runner runs at most 48 sub-programs at once, nested at most 8 levels deep. A start past either limit runs nothing, and its await answers refused. The executable vocabulary refuses an app root that reaches a primitive directly.

2. Write the manifest

The entry kind is app, and the backends are lean (for development) and lean-native (for the standalone binary):

{
  "schema": "lema.exec/v1",
  "entry": {"kind": "app", "root": "LemaDraft.Cap.FanFiles.app"},
  "roots": {
    "LemaDraft.Cap.FanFiles.app": "5d2a20765405f0a4ca9fdbf42b1ce118d8a2849c9763a7517c85500b529e4edc"
  },
  "seeds": {
    "LemaDraft.Prog": "f93b9fc28eec562dc8edc12238872ee99ba072e080735a8ca7173e6e46d3bcf0",
    "LemaDraft.Cap.AppCmd": "62922af407cfd4fc673789fc177dc77c5a8dd31aaab0d35e9046058572835d4d",
    "LemaDraft.Cap.Awaited": "8551d5e6c0199a77adadfacae0fe727ece913300f666bb736d16778234c3da43"
  },
  "pieces": [
    {"source": "core/CoreV2.lean", "whole": false},
    {"source": "cap/AppCmd.lean", "whole": true},
    {"source": "cap/FanFiles.lean", "whole": true}
  ],
  "received": {
    "Prog": "LemaDraft.Prog",
    "call": "LemaDraft.Prog.call",
    "ret": "LemaDraft.Prog.ret"
  },
  "backends": ["lean", "lean-native"],
  "seconds": 60,
  "expect": {"output_sha256": "09fe70c0b9d996b6432b9c7a2b38119e661de1444b07496b6734fb98bcb6f00a"}
}

The fields are described in Execution manifests.

3. Build the shim library and the capability artifact

cargo build -p lema-cap
lema cap-build --runtime $CONFIG --name cap --staticlib target/debug/liblema_cap.a

cap-build makes two native calls. It compiles the tool’s copy of LemaCap.lean, then links the development library libLemaCap.so from it, the tool’s copy of lean/cap/glue.c and your liblema_cap.a. It prints status, the artifact’s directory and its id. A library built from other shim sources is refused (was not built from this tool's lema-cap sources): rebuild it with cargo build -p lema-cap.

4. Write the deployment directory

Create a directory that only you can read, holding lema-cap.json, and a state directory. Keep both outside the Lean distribution and the runtime’s output. Below, $DEPLOYMENT is the first directory:

{"schema": "lema.cap-config/v1", "origins": {}, "files": {"state_dir": "/path/to/state", "max_file_bytes": 4096, "max_list_entries": 8}}

state_dir must be an absolute path. FanFiles makes no HTTPS exchange, so origins is empty. Origins and credentials are described under “Configuration” in crates/lema-cap/FRAMES.md. The runner gives this file’s path to the shims in LEMA_CAP_CONFIG. The program itself reads no environment variable and no secret.

5. Test both modes

lema test --manifest lean/exec/fanfiles-app.json --store $STORE --runtime $CONFIG --name fan \
  --cap cap --deployment $DEPLOYMENT

lema test builds two artifacts:

• fan-lean, for development: lean --run interprets the module whose roots the build compared with the accepted objects, with the capability artifact’s libLemaCap.so loaded.
• fan-lean-native: the standalone binary.

It runs each once in the application sandbox, in the manifest’s order and sharing the state directory, then compares their outputs with each other and with expect. With a fresh state directory the output is four lines, 0 ok to 3 ok.

6. Build and run the standalone binary

lema build --manifest lean/exec/fanfiles-app.json --store $STORE --runtime $CONFIG --name fan-bin \
  --cap cap --standalone
lema run --runtime $CONFIG --artifact fan-bin --deployment $DEPLOYMENT

--standalone compiles a second module from the same pieces, importing only Init and LemaCap. Each of its declarations must have the same Lean.IR as in the first compile, except main and main._boxed, which have fixed texts. The build links it with the capability platform into the application fan-bin-app. lema run verifies the app artifact, the application and the capability artifact, then runs the app in the application sandbox. To release it, see Release an artifact.

Refusals you may see:

• an app entry builds against a capability artifact: --cap NAME (lema cap-build);
• --cap NAME --deployment DIR, from lema test given only one of them;
• an app artifact runs in a deployment: --deployment DIR;
• an app entry takes no arguments, only an input;
• a piece that mentions LemaRunner, refused before any native call;
• artifact file Run.olean changed, for an artifact edited after it was built.

What is checked, tested and assumed

The roots are checked: the pinned Lean 4.34.1 kernel accepted them into the store. The runner, the shims and the binaries are tested. Most of the shims’ tests in crates/lema-cap/tests run under the plain cargo test, and the native ones are gated. crates/lema-cli/tests/standalone.rs (LEMA_STANDALONE_RUNTIME) builds, tests and runs this app. Its build, test and run passed natively on 17 Oct 2026, as lean/exec/README.md and docs/architecture.md record. Assumed: rustls, ring, webpki-roots, the C compiler and linker, the Lean runtime and its task manager, the OS, the network, and that the emitted C matches the compared IR.