# 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`.
Raw data
{
"_id": null,
"home_page": null,
"name": "lmms-lean-server",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.12",
"maintainer_email": null,
"keywords": "lean, lean-server, theorem prover, fastapi",
"author": null,
"author_email": "Pu Fanyi <FPU001@e.ntu.edu.sg>",
"download_url": "https://files.pythonhosted.org/packages/4f/f2/ae63dd6d39c4f891d669beed57d30cdf0691787f68764eafb71fd2da7aef/lmms_lean_server-0.0.1.dev4.tar.gz",
"platform": null,
"description": "# Lean Server Package\n\nThis package contains the core `lean-server` application, a FastAPI-based server that provides a REST API for interacting with the Lean prover.\n\n## \ud83d\udcd6 Overview\n\nThe 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.\n\nThe main API endpoint is:\n- `POST /prove/check`: Accepts a `proof` and an optional `config` to run a proof.\n\n## \u2699\ufe0f Configuration\n\nThe server's behavior can be configured via `config.yaml`. Key settings include:\n- Server host and port.\n- Lean process configuration.\n- Proof checking timeouts.\n\n## \ud83d\ude80 Running the Server\n\nThis package is intended to be run within the development container.\n\n1. **Navigate to the Dev Container**:\n Follow the instructions in the [root README](../../README.md) to set up the development environment.\n\n2. **Install Dependencies**:\n In the container's terminal, install the package in editable mode:\n ```bash\n uv pip install -e .\n ```\n (Note: The root setup installs this automatically).\n\n3. **Start the Server**:\n The `pyproject.toml` file defines a script entry point. You can start the server with the following command:\n ```bash\n lean-server\n ```\n By default, it should be available at `http://localhost:8000`.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "A FastAPI-based server to interact with the Lean Theorem Prover.",
"version": "0.0.1.dev4",
"project_urls": {
"Homepage": "https://github.com/pufanyi/lean-server",
"Repository": "https://github.com/pufanyi/lean-server"
},
"split_keywords": [
"lean",
" lean-server",
" theorem prover",
" fastapi"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "53faead69cc4b1f3198eebcade2325bbe5c7ee6839196df6ac1fcb58cfd65238",
"md5": "7277710bb5b0471744c25d79ac3939c3",
"sha256": "c825cc2f5a537e5e670d2e8992190eece249e50e81ca9a44464f19ae2723ddec"
},
"downloads": -1,
"filename": "lmms_lean_server-0.0.1.dev4-py3-none-any.whl",
"has_sig": false,
"md5_digest": "7277710bb5b0471744c25d79ac3939c3",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.12",
"size": 10605,
"upload_time": "2025-08-06T05:24:11",
"upload_time_iso_8601": "2025-08-06T05:24:11.402522Z",
"url": "https://files.pythonhosted.org/packages/53/fa/ead69cc4b1f3198eebcade2325bbe5c7ee6839196df6ac1fcb58cfd65238/lmms_lean_server-0.0.1.dev4-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "4ff2ae63dd6d39c4f891d669beed57d30cdf0691787f68764eafb71fd2da7aef",
"md5": "2d09f6f3ce881a2b74fa9ba617f91705",
"sha256": "c6fbf1ee7828d1aefd6cc288ebec60f4b79718aee2e68f5ec582519b17268753"
},
"downloads": -1,
"filename": "lmms_lean_server-0.0.1.dev4.tar.gz",
"has_sig": false,
"md5_digest": "2d09f6f3ce881a2b74fa9ba617f91705",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.12",
"size": 8520,
"upload_time": "2025-08-06T05:24:12",
"upload_time_iso_8601": "2025-08-06T05:24:12.527991Z",
"url": "https://files.pythonhosted.org/packages/4f/f2/ae63dd6d39c4f891d669beed57d30cdf0691787f68764eafb71fd2da7aef/lmms_lean_server-0.0.1.dev4.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-06 05:24:12",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "pufanyi",
"github_project": "lean-server",
"github_not_found": true,
"lcname": "lmms-lean-server"
}
JSON
