Start a store and a server

Create a store with the default axiom policy, run the server on a Unix socket, and ask it what the store holds.

By the end of this tutorial you will have a new store, a server answering on a socket, and a runtime configuration of your own. The next three tutorials use all three.

You need:

• Set up a machine for Lema done, with LEMA_NATIVE=yes;
• ~/.lema/env loaded in every terminal you use;
• two terminals: one for the server, one for your requests.

Name the three paths

The tutorials from here on use three variables. Write them to a file you can load in any terminal:

mkdir -p ~/lema-tutorial
cat > ~/lema-tutorial/env <<'EOF'
export STORE=$HOME/lema-tutorial/store
export SOCK=$HOME/lema-tutorial/lema.sock
export CONFIG=$HOME/lema-tutorial/runtime.json
EOF
source ~/lema-tutorial/env

$STORE is the store directory, which lema init creates below. $SOCK is the Unix socket the server will listen on. $CONFIG is your runtime configuration, which you write next. Every file the tutorials create goes under ~/lema-tutorial/.

Write the runtime configuration

Copy the base configuration from setup and give it an output directory of its own:

mkdir -m 700 ~/lema-tutorial/output
jq --arg out ~/lema-tutorial/output '.output = $out' $LEMA_RUNTIME_BASE > $CONFIG
cat $CONFIG

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

The distribution and the shared lock are the base’s, so your calls still take turns with every other native call on the machine. The output is new. Everything the server’s native calls write goes there: the ledger, a work directory and a log for each call, the module cache, and later the build artifacts. If a fault latches this output, it stops only the calls of these tutorials.

Create the store

lema init --store $STORE

created store /home/you/lema-tutorial/store (namespace 4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a)

A store is a directory that holds objects under their IDs, aliases (names that point at IDs), and a receipt for each object the pinned Lean 4.34.1 kernel has accepted. A new store holds one object, the namespace. It pins Lean 4.34.1 and its git hash, and every other object names it.

You gave no --axioms, so the store has the default axiom policy: a proof may use Lean’s three standard axioms, propext, Quot.sound and Classical.choice. Some axioms, such as sorryAx, are refused by every store whatever its policy; they make up the fixed floor. A store keeps the policy it was created with. Axiom policy and the fixed floor gives the rules.

Start the server

In your second terminal, load both files and start the server:

source ~/.lema/env
source ~/lema-tutorial/env
lema serve --store $STORE --runtime $CONFIG --socket $SOCK

lema: serving /home/you/lema-tutorial/store on /home/you/lema-tutorial/lema.sock

The server takes a while to start. It checks the whole Lean distribution again, then makes its first native call to build the decoder module, LemaCodebase. That is the Lean code that turns stored objects back into Lean declarations when the server checks them. It is built once per module cache, so later starts with this output skip that call. If the call cannot run, the server prints the decoder module is not built yet and still answers reads.

Leave the server running. While it runs, it holds the store’s lock, so no other process can write the store, and it makes every native call itself. It answers one JSON request per connection on the socket, one request at a time, and only your user can open the socket.

Ask what the store holds

The same lema program is also the client. Back in your first terminal, ask the server to describe the store:

lema --socket $SOCK info | jq .

The client sends one request, the info method, and prints the server’s answer as one line of JSON. jq . spreads it out:

{
  "accepted": 0,
  "aliases": 0,
  "allowed_axioms": [
    "Classical.choice",
    "Quot.sound",
    "propext"
  ],
  "modules": 1,
  "namespace": "4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a",
  "native_call_budget": null,
  "native_calls_used": 1,
  "objects": 1,
  "tooling_sha256": "…"
}

The tooling_sha256 value is shortened here. It identifies the checking tools, and every receipt records it. The other fields:

• objects is 1 and accepted is 0: the namespace is stored, and it is accepted together with your first proof in the next tutorial.
• allowed_axioms is the store’s axiom policy.
• modules is the decoder module the server built when it started, and native_calls_used counts that one call in your output’s ledger.
• native_call_budget is null because your configuration sets no call_budget.

Now list the stored IDs:

lema --socket $SOCK ids

["4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a"]

The only ID is the namespace’s. info and ids are shortcuts for lema --socket $SOCK call info and call ids. Every other method goes through lema --socket $SOCK call METHOD, with its parameters in --params JSON or --params-file FILE, and the next tutorial uses both. If the server refuses a request, the client prints the error and exits with status 1. Server methods lists the methods, and The lema command lists the commands.

Next

Keep the server running and publish your first proof.