Metadata-Version: 2.4
Name: lmms-lean-server
Version: 0.0.1.dev4
Summary: A FastAPI-based server to interact with the Lean Theorem Prover.
Author-email: Pu Fanyi <FPU001@e.ntu.edu.sg>
License: MIT
Project-URL: Repository, https://github.com/pufanyi/lean-server
Project-URL: Homepage, https://github.com/pufanyi/lean-server
Keywords: lean,lean-server,theorem prover,fastapi
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Classifier: Operating System :: OS Independent
Classifier: Framework :: FastAPI
Requires-Python: >=3.12
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: pydantic>=2.11.7
Requires-Dist: pyyaml>=6.0.2
Requires-Dist: loguru>=0.7.2
Requires-Dist: fastapi>=0.116.1
Requires-Dist: uvicorn>=0.35.0
Requires-Dist: rich>=14.1.0
Requires-Dist: aiosqlite>=0.21.0
Requires-Dist: python-multipart>=0.0.20
Requires-Dist: aiohttp>=3.12.15
Requires-Dist: uuid-utils>=0.11.0
Requires-Dist: datasets>=4.0.0
Dynamic: license-file

# Lean Server Package

This package contains the core `lean-server` application, a FastAPI-based server that provides a REST API for interacting with the Lean prover.

## 📖 Overview

The server is designed to be run inside the Docker environment provided at the root of this monorepo. It exposes endpoints to perform proof checking and other Lean-related tasks.

The main API endpoint is:
- `POST /prove/check`: Accepts a `proof` and an optional `config` to run a proof.

## ⚙️ Configuration

The server's behavior can be configured via `config.yaml`. Key settings include:
- Server host and port.
- Lean process configuration.
- Proof checking timeouts.

## 🚀 Running the Server

This package is intended to be run within the development container.

1.  **Navigate to the Dev Container**:
    Follow the instructions in the [root README](../../README.md) to set up the development environment.

2.  **Install Dependencies**:
    In the container's terminal, install the package in editable mode:
    ```bash
    uv pip install -e .
    ```
    (Note: The root setup installs this automatically).

3.  **Start the Server**:
    The `pyproject.toml` file defines a script entry point. You can start the server with the following command:
    ```bash
    lean-server
    ```
    By default, it should be available at `http://localhost:8000`.
