Skip to content

Server API Reference

The Server module provides the backend infrastructure for running LeanFlow as a service. It wraps the Lean REPL in a HTTP server (FastAPI), managing a pool of worker processes to handle concurrent requests.

Server Class

The Server class is the main entry point. It initializes the worker pool, handles the request queue, and manages the lifecycle of persistent Lean environments.

leanflow.Server

Server that owns and configures the StateManager.

Example 
import asyncio
from leanflow import Server

async def main():
    server = await Server.create_from_yaml("server.yaml")
    try:
        result = await server.run("#eval 1 + 1")
        print(result)
    finally:
        await server.shutdown()

asyncio.run(main())

__init__(state_manager)

Initialize the server with a StateManager instance.

Parameters:

Name Type Description Default
state_manager StateManager

The initialized state manager.

 required

create_from_yaml(yaml_path) async classmethod

Asynchronously creates the Server by loading configuration from a YAML file.

This method waits for the StateManager to be fully initialized before returning.

Parameters:

Name Type Description Default
yaml_path Union[str, Path]

Path to the YAML configuration file.

 required

Returns:

Type Description
Server

The initialized Server instance.

run(command, env=None) async

Run command using the StateManager.

Parameters:

Name Type Description Default
command str

The Lean command to execute.

 required
env Optional[int]

The environment ID to run in.

 None

Returns:

Type Description
Union[Environment, LeanError]

The result of the command.

delete_environment(env_id) async

Delete environment using the StateManager.

Parameters:

Name Type Description Default
env_id int

The environment ID to delete.

 required

Returns:

Type Description
bool

True if deleted, False if not found.

shutdown() async

Shutdown the server by shutting down the StateManager.

Starting the Server

Command Line

leanflow-serve --config server.yaml

Configuration File (server.yaml)

The configuration file is split into two sections:

  • server: Controls HTTP server and worker settings.

  • repl: Passed directly to the underlying Lean REPL instances.

server:
  host: 0.0.0.0
  port: 8000
  workers: 10
  stateless: false

repl:
  lean_version: "4.24.0"
  require_mathlib: true
  timeout: 300
  # Optional: Shared header to run on startup for every worker
  header: |
    import Mathlib

Configuration Options

Option Type Default Description
server.host string localhost Host address to bind to
server.port int 8000 Port number
server.workers int 10 Number of REPL workers
server.stateless bool false Stateless mode
repl.lean_version string required Lean version to use
repl.require_mathlib bool true Whether to include Mathlib
repl.timeout int 300 Command timeout in seconds
repl.header string null Commands to run at startup

REST API Endpoints

Method Endpoint Description
GET /status Check server status
POST /run Execute a Lean command

POST /run

Request: 

{"command": "#eval 1 + 1", "env": null}

Response: 

{
  "result": {
    "env": 1,   // ID of the new resulting environment
    "messages": [
      {
        "severity": "info",
        "pos": {"line": 1, "column": 0},
        "data": "2"
      }
    ],
    "sorries": [],
    "goals": []
  }
}