lean_server.app package¶

Submodules¶

This module defines the command-line argument parser for the Lean server.

lean_server.app.args.parse_args() → Namespace[source]¶

Parses command-line arguments for the Lean server.

This module defines the database API endpoints for the FastAPI application.

lean_server.app.db.launch_db_router(app: FastAPI)[source]¶

Mounts the database-related API endpoints to the FastAPI application.

This module defines the lifespan manager for the FastAPI application.

lean_server.app.lifespan.get_lifespan(*, config: Config)[source]¶

Returns an asynchronous context manager for the application’s lifespan.

This function sets up resources on startup and cleans them up on shutdown. It initializes the database, proof manager, and other application state.

This module defines the proof-related API endpoints for the FastAPI application.

lean_server.app.prove.launch_prove_router(app: FastAPI)[source]¶

Mounts the proof-related API endpoints to the FastAPI application.

This module is the main entry point for launching the Lean server.

lean_server.app.serve.launch(*, config: Config) → FastAPI[source]¶

Creates and configures the FastAPI application.

This function initializes the FastAPI app, sets up the lifespan manager, and mounts the API routers.

lean_server.app.serve.main()[source]¶

The main entry point for the server.

This function parses command-line arguments, loads the configuration, launches the FastAPI application, and starts the Uvicorn server.