Server methods

The request protocol of lema serve and every method it answers, with parameters and results.

lema serve owns one store and one runtime configuration and answers requests on a Unix socket. The dispatch is Server::handle in crates/lema-cli/src/main.rs; the methods it hands on are in crates/lema-store and crates/lema-http/src/release.rs. This page describes them at lema-lang HEAD 5a94951. From the command line, any method is sent with lema call METHOD (the CLI reference).

Protocol

A client opens one connection per request. It writes one JSON object, shuts down its write side, and reads one JSON response.

{"method": "find", "params": {"prefix": "app."}}

{"ok":true,"result":{"app.main":{"generation":1,"id":"…"}}}

A refused request is answered with {"ok": false, "error": "<message>"}. Responses are canonical JSON: sorted keys, no whitespace.

The socket is created with the process’s file mode mask set to 077, so it is owner-only from the start, and the server checks that its mode grants nothing to group or others. Every client therefore runs as the store’s OS user. At start the server replaces a stale socket file, and refuses a path where a server still answers or that is not a socket.

Conventions

• An ID is 64 lowercase hexadecimal digits. Object IDs are defined on the objects page.
• A reference is {id} or {id, role}: an object, or one role of it (for example a structure’s constructor).
• Every method that moves an alias names what it expects the alias to hold. expect: null means the name must be new. expect: {id, role?} means it must name that reference, and expect: {id, role?, generation} adds the generation, as find returns it. replace uses its own fields, expected and expected_generation.
• overwrite: true in place of expect applies the change whatever the alias holds, and the history records it as an overwrite. A missing or stale expectation is refused.
• idempotency_key is a string of 1 to 256 bytes without control characters. alias, submit/import, publish, replace, ref.create, ref.publish and ref.adopt accept it. It is bound to sha256("LEMA-PUBLICATION-v1\0" ‖ operation ‖ "\0" ‖ canonical JSON of the params without the key). A retry with the same key and the same params returns the first response and applies nothing; the same key with other params is refused. Keys never expire and are shared by every client of the store.
• actor and token authenticate ref.create, ref.publish, ref.adopt and review.create. The token is compared with the SHA-256 the store keeps, and is never recorded.
• Only elaborate, submit/import, publish, executable and reverify can make native calls. Every other method reads or writes the store without Lean.
• The bundle, project, report, review and release methods refuse unknown fields.

Objects and aliases

info

Reports the store and the server. It takes no params.

ids

Returns every stored object ID, as a list. It takes no params.

get

Returns stored objects, each re-validated against its ID. Its one param, ids, is required: a list of IDs. The result maps each ID to its object.

show

Returns one object with what the store knows about it. Its one param, id, is required: an object ID.

find

Returns aliases by name prefix. Its one param, prefix, is optional; without it every alias is returned. The result maps each name to {id, role?, generation}: the form an expectation takes.

deps

Returns every object ID that an object links to directly: its namespace, statement, template, binding, proofs, realizations and generated family where present, and the references inside its expressions and family entries. Its one param, id, is required: an object ID.

dependents

Returns the stored objects that link directly to an object. Its one param, id, is required: an object ID.

alias

Creates or moves one alias.

submit and import

Accepts a draft by kernel replay, whole or not at all. import is the same method under another name.

Expectations are checked before any native call and again when the changes apply. The closure is replayed source-free by the pinned Lean 4.34.1 kernel, incrementally through the module cache, within the store’s axiom policy above the fixed floor. All alias changes of the request apply together in one history line.

export

Returns the accepted objects reachable from roots, for transfer to another store. Its one param, roots, is required: a list of IDs. The result maps each ID in the closure to its object. It is refused when any object of the closure is not accepted. Receipts are not exported; a receiving store replays the objects.

Authoring and checking

elaborate

Turns restricted Lean into an untrusted draft of canonical objects. Nothing is stored. The source’s rules are on the authoring rules page.

Each receive item binds every export N of its bundle as Received.<as>.N, or as Received.N without as. rename maps an export name to the name it takes, and prefix is another spelling of as. A derived seed is sha256("lema.seed/v1\0" ‖ seed_salt ‖ "\0" ‖ name).

Before any native call the server checks every binding. A name bound twice, an unknown bundle, a target that is not accepted, or a role its object lacks is refused. The server then replays any received object that no module holds yet into a new module, which is a native call only when there is such an object. It adds one Lean alias per binding, runs the exporter in one sandboxed call with a 300-second limit, and builds the objects.

publish

Runs elaborate and then submit inside the server, so a client never holds the draft.

The submitted roots are the IDs of the draft’s names that have no role. Each alias must name an object the submission reaches, or one already accepted. Expectations and the authoring shape are checked before the first native call, and the whole authoring bundle before the submission’s native call; only its write follows acceptance.

view

Renders accepted objects in the contract syntax.

The result maps each requested name to {text, names}, or to {error} when the object cannot be shown. In names, each name in the text maps to {id, role?} for a stored object or {lean: name} for one of Lean’s constants. view does not check its output; the round-trip tests do.

executable

Compiles restricted Lean from source alone and checks what the compiled code reaches. It makes one sandboxed native call (600 seconds).

The IR closure of the roots must pass the executable vocabulary (crates/lema-check/src/vocabulary.rs), and the roots’ whole object closure must be accepted. The result has roots (name to ID), objects (the closure’s size), declarations, externs, vocabulary (the vocabulary’s digest), call and claim. With profiles it also has guarantees, one receipt per profile, and guarantee_records, the ID of each receipt stored as a guarantee record. A violated or unsupported profile is reported in its receipt, not refused.

reverify

Replays accepted objects from scratch in one native call (600 seconds), with no modules, and compares the result with the store. Its one param, roots, is optional: a list of IDs whose closure is replayed. Without it, every accepted object is replayed. The closure may hold at most 20,000 objects; a larger store is replayed in parts with roots. Each kernel receipt’s axiom footprint must equal the fresh one, and every other object must be used directly by a declaration replayed in the same call. Any difference is an error.

Evolution

replace

Moves an alias from one implementation to another, only with an accepted proof of exactly the replacement claim. One history line records the move and its witness.

Every field but name is an object ID, and every one of them must be accepted. Without relation, the claim is contract S T expected target representation. With it, the claim is relation a1 … ak contract expected target representation, possibly over parameters. The contract, implementations, relation, claim and proof must have no universe parameters. The result is the witness: name, old, new, contract, claim, proof, representation, namespace and scope, and with a relation also relation and prefix (the leading arguments), and parameters when the claim has any.

Contract evolution

The params of refine and correct are IDs of accepted objects, and correct refuses a proof. Each records one history line. A refine witness’s shape is predicate (∀ x…, new x… → old x…, with parameters) or protocol (Refines new old Rel, with relation and state_relation). A correct witness’s clients are the accepted declarations that must re-prove. evolution reads its result from the history.

Bundles

In bundle.create, each of exports is {name, id, role?} and must be accepted with that role, and each of from_aliases is an alias name or {alias, name}. Aliases are resolved once, at creation; the result’s exports is a count. In bundle.list, exports and helpers are counts; names: true lists export names, and helpers: true with names includes helpers.

Projects

The records these methods write are described on the store records page. A project reference’s expectation is expect: {revision, generation, policy_version}, all three required: the revision ID or null, and two positive integers, as ref.list returns them.

kind is one of binding-map, authoring, snapshot, revision, policy, guarantee, merge and review. Every limit is 1 to 10,000, default 100. ref.create needs an operator and a policy of version 1. ref.publish is authorized by the reference’s active policy, which must also admit the revision. ref.adopt is authorized by the active policy too, and the reference’s revision must meet the incoming policy. Both checks run in the same call as the move, and a refusal writes nothing.

Reports, merges and reviews

None of these is a kernel check: they read receipts and witnesses that replay, replace, refine and correct wrote.

Releases

These methods run on the server’s store and on the runtime’s artifacts/ directory; lema release runs the same code on a store it opens itself. They make no native call. artifact names a directory under artifacts/, and every path is absolute. deployment is a deployment configuration file, or for an app artifact’s release its deployment directory.

A release’s status is {recorded, withdrawn, superseded_by, supersedes, selectable}.

Related

• The lema command
• Store records
• Objects and identity