# Lean Client
A Python client for the Lean Server API.
This package provides a simple, asynchronous `LeanClient` to interact with the `lean-server`.
## 📦 Installation
### As a Standalone Package
To install this package from PyPI (once published):
```bash
pip install lean-client
```
### For Development
This package is part of a monorepo. For development, follow the setup instructions in the [root README](../../README.md). The recommended installation command within the dev container is:
```bash
# This installs the client in editable mode
uv pip install -e .
```
## 🚀 Usage
The client is asynchronous and designed to be used with `asyncio`.
### Basic Usage
Here is a basic usage example:
```python
import asyncio
from lean_client import LeanClient
async def main():
# Assumes the server is running on http://localhost:8000
# The client can be used as an async context manager.
async with LeanClient("http://localhost:8000") as client:
proof_to_check = "def my_theorem : 1 + 1 = 2 := rfl"
# Optional configuration can be passed as a dictionary.
config = {"timeout": 60}
print(f"Checking proof: '{proof_to_check}'")
result = await client.check_proof(proof_to_check, config=config)
print("\nServer response:")
print(result)
if __name__ == "__main__":
# To run the example, save it as a file (e.g., `test_client.py`)
# and run `python test_client.py` in a terminal where the server is running.
asyncio.run(main())
```
### File Support
The client supports multiple ways to provide proof content:
1. **String content directly**:
```python
proof_content = "theorem test : 1 + 1 = 2 := by rfl"
result = await client.check_proof(proof_content)
```
2. **File path as string**:
```python
result = await client.check_proof("path/to/proof.lean")
```
3. **Path object**:
```python
from pathlib import Path
proof_file = Path("path/to/proof.lean")
result = await client.check_proof(proof_file)
```
### Complete Example with File
```python
import asyncio
from pathlib import Path
from lean_client import LeanClient
async def check_proof_from_file():
async with LeanClient("http://localhost:8000") as client:
# Create a test Lean file
proof_file = Path("test_proof.lean")
proof_content = """
theorem test_theorem : 1 + 1 = 2 := by
rw [add_comm]
rw [add_zero]
rfl
"""
# Write content to file
with open(proof_file, 'w', encoding='utf-8') as f:
f.write(proof_content)
try:
# Check proof from file
result = await client.check_proof(proof_file, config={"timeout": 30})
print(f"Proof check result: {result}")
finally:
# Clean up
if proof_file.exists():
proof_file.unlink()
if __name__ == "__main__":
asyncio.run(check_proof_from_file())
```
## 📚 API Reference
### LeanClient
The main client class for interacting with the Lean Server.
#### `__init__(base_url: str)`
Initialize the client with the server's base URL.
#### `async check_proof(proof: Union[str, Path, os.PathLike], config: dict[str, Any] | None = None) -> dict[str, Any]`
Send a proof to the server for checking.
**Parameters:**
- `proof`: The proof content. Can be:
- A string containing the proof
- A Path object pointing to a file containing the proof
- A string path to a file containing the proof
- `config`: Optional configuration dictionary for the proof check
**Returns:**
- A dictionary containing the server's response
#### `async close()`
Close the client session.
#### `async __aenter__()` and `async __aexit__()`
Async context manager support for automatic session management.
Raw data
{
"_id": null,
"home_page": null,
"name": "lean-runner",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.12",
"maintainer_email": null,
"keywords": "lean, lean-client, lean-server, theorem prover",
"author": null,
"author_email": "Pu Fanyi <FPU001@e.ntu.edu.sg>",
"download_url": "https://files.pythonhosted.org/packages/65/db/833a0d976c02a4de23703d47fb3eb8974b75978b54193ce88d763c2c472a/lean_runner-0.0.1.dev4.tar.gz",
"platform": null,
"description": "# Lean Client\n\nA Python client for the Lean Server API.\n\nThis package provides a simple, asynchronous `LeanClient` to interact with the `lean-server`.\n\n## \ud83d\udce6 Installation\n\n### As a Standalone Package\nTo install this package from PyPI (once published):\n```bash\npip install lean-client\n```\n\n### For Development\nThis package is part of a monorepo. For development, follow the setup instructions in the [root README](../../README.md). The recommended installation command within the dev container is:\n```bash\n# This installs the client in editable mode\nuv pip install -e .\n```\n\n## \ud83d\ude80 Usage\n\nThe client is asynchronous and designed to be used with `asyncio`.\n\n### Basic Usage\n\nHere is a basic usage example:\n\n```python\nimport asyncio\nfrom lean_client import LeanClient\n\nasync def main():\n # Assumes the server is running on http://localhost:8000\n # The client can be used as an async context manager.\n async with LeanClient(\"http://localhost:8000\") as client:\n proof_to_check = \"def my_theorem : 1 + 1 = 2 := rfl\"\n\n # Optional configuration can be passed as a dictionary.\n config = {\"timeout\": 60}\n\n print(f\"Checking proof: '{proof_to_check}'\")\n result = await client.check_proof(proof_to_check, config=config)\n\n print(\"\\nServer response:\")\n print(result)\n\nif __name__ == \"__main__\":\n # To run the example, save it as a file (e.g., `test_client.py`)\n # and run `python test_client.py` in a terminal where the server is running.\n asyncio.run(main())\n```\n\n### File Support\n\nThe client supports multiple ways to provide proof content:\n\n1. **String content directly**:\n```python\nproof_content = \"theorem test : 1 + 1 = 2 := by rfl\"\nresult = await client.check_proof(proof_content)\n```\n\n2. **File path as string**:\n```python\nresult = await client.check_proof(\"path/to/proof.lean\")\n```\n\n3. **Path object**:\n```python\nfrom pathlib import Path\nproof_file = Path(\"path/to/proof.lean\")\nresult = await client.check_proof(proof_file)\n```\n\n### Complete Example with File\n\n```python\nimport asyncio\nfrom pathlib import Path\nfrom lean_client import LeanClient\n\nasync def check_proof_from_file():\n async with LeanClient(\"http://localhost:8000\") as client:\n # Create a test Lean file\n proof_file = Path(\"test_proof.lean\")\n proof_content = \"\"\"\ntheorem test_theorem : 1 + 1 = 2 := by\n rw [add_comm]\n rw [add_zero]\n rfl\n\"\"\"\n\n # Write content to file\n with open(proof_file, 'w', encoding='utf-8') as f:\n f.write(proof_content)\n\n try:\n # Check proof from file\n result = await client.check_proof(proof_file, config={\"timeout\": 30})\n print(f\"Proof check result: {result}\")\n finally:\n # Clean up\n if proof_file.exists():\n proof_file.unlink()\n\nif __name__ == \"__main__\":\n asyncio.run(check_proof_from_file())\n```\n\n## \ud83d\udcda API Reference\n\n### LeanClient\n\nThe main client class for interacting with the Lean Server.\n\n#### `__init__(base_url: str)`\nInitialize the client with the server's base URL.\n\n#### `async check_proof(proof: Union[str, Path, os.PathLike], config: dict[str, Any] | None = None) -> dict[str, Any]`\nSend a proof to the server for checking.\n\n**Parameters:**\n- `proof`: The proof content. Can be:\n - A string containing the proof\n - A Path object pointing to a file containing the proof\n - A string path to a file containing the proof\n- `config`: Optional configuration dictionary for the proof check\n\n**Returns:**\n- A dictionary containing the server's response\n\n#### `async close()`\nClose the client session.\n\n#### `async __aenter__()` and `async __aexit__()`\nAsync context manager support for automatic session management.\n",
"bugtrack_url": null,
"license": null,
"summary": "A Python client for the Lean Theorem Prover Server API.",
"version": "0.0.1.dev4",
"project_urls": {
"Repository": "https://github.com/pufanyi/lean-server"
},
"split_keywords": [
"lean",
" lean-client",
" lean-server",
" theorem prover"
],
"urls": [
{
"comment_text": null,
"digests": {
"blake2b_256": "05062438e0fa1e6af7c60d1b7c2c59e96a79b2c613756c77eadb265a1863e437",
"md5": "d02a51ce40c973599e306e1f8a1f822a",
"sha256": "9dfc620e7b0cac0cf66463d3a574d7ccd4a15dc4ceef5f22c295f61866132078"
},
"downloads": -1,
"filename": "lean_runner-0.0.1.dev4-py3-none-any.whl",
"has_sig": false,
"md5_digest": "d02a51ce40c973599e306e1f8a1f822a",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.12",
"size": 8633,
"upload_time": "2025-08-09T03:35:08",
"upload_time_iso_8601": "2025-08-09T03:35:08.264966Z",
"url": "https://files.pythonhosted.org/packages/05/06/2438e0fa1e6af7c60d1b7c2c59e96a79b2c613756c77eadb265a1863e437/lean_runner-0.0.1.dev4-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": null,
"digests": {
"blake2b_256": "65db833a0d976c02a4de23703d47fb3eb8974b75978b54193ce88d763c2c472a",
"md5": "7ec03ec2cd764134c04754cf92534c41",
"sha256": "598b3836717531ccb9a3c03b34d782b0956b0b6f34c8111b27ab2dc359da9e95"
},
"downloads": -1,
"filename": "lean_runner-0.0.1.dev4.tar.gz",
"has_sig": false,
"md5_digest": "7ec03ec2cd764134c04754cf92534c41",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.12",
"size": 8050,
"upload_time": "2025-08-09T03:35:09",
"upload_time_iso_8601": "2025-08-09T03:35:09.935511Z",
"url": "https://files.pythonhosted.org/packages/65/db/833a0d976c02a4de23703d47fb3eb8974b75978b54193ce88d763c2c472a/lean_runner-0.0.1.dev4.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2025-08-09 03:35:09",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "pufanyi",
"github_project": "lean-server",
"github_not_found": true,
"lcname": "lean-runner"
}
JSON
