leanclient
Interact with the Lean 4 language server in Python.
leanclient is a thin Python wrapper around the native Lean 4 language server. It enables interaction with a Lean 4 language server instance running in a subprocess.
Check out the documentation for more information.
Key Features
- Interact: Query and change lean files via the LSP.
- Thin wrapper: Directly expose the Lean Language Server.
- Fast: Typically more than 95% of time is spent waiting.
- Parallel: Easy batch processing of files using all your cores.
Quickstart
The best way to get started is to check out this minimal example in Google Colab:
Or try it locally:
-
Setup a new lean project or use an existing one. See the colab notebook for a basic Ubuntu setup.
-
Install the package:
pip install leanclient
# Or with uv:
uv pip install leanclient
- Example:
import leanclient as lc
# Start a new client, point it to your lean project root (where lakefile.toml is located).
PROJECT_PATH = "path/to/your/lean/project/root/"
client = lc.LeanLSPClient(PROJECT_PATH)
# Query a lean file in your project
file_path = "MyProject/Basic.lean"
diagnostics = client.get_diagnostics(file_path)
print(f"Found {len(diagnostics)} diagnostics")
# Use a SingleFileClient for simplified interaction with a single file.
sfc = client.create_file_client(file_path)
# Get symbols in the file (theorems, definitions, etc.)
symbols = sfc.get_document_symbols()
print(f"File contains {len(symbols)} symbols")
# Get hover information at a specific position
hover = sfc.get_hover(line=10, character=5)
if hover:
print(f"Hover info: {hover['contents']}")
# Make a change to the document.
change = lc.DocumentContentChange(
text="-- Adding a comment at the head of the file\n",
start=[0, 0],
end=[0, 0]
)
sfc.update_file(changes=[change])
# Verify the change (not written to disk, only in LSP memory)
content = sfc.get_file_content()
assert content.startswith("-- Adding a comment")
# Explore module hierarchy (requires .ilean files from built dependencies)
module = client.prepare_module_hierarchy(".lake/packages/mathlib/Mathlib/Init.lean")
imports = client.get_module_imports(module)
print(f"Module {module['name']} has {len(imports)} direct imports")
imported_by = client.get_module_imported_by(module)
print(f"Module is imported by {len(imported_by)} other modules")
Implemented LSP Interactions
See the documentation for more information on:
- Opening and closing files.
- Updating (adding/removing) code from an open file.
- Diagnostic information: Errors, warnings and information.
- Goals and term goal.
- Hover information.
- Document symbols (theorems, definitions, etc).
- Semantic tokens, folding ranges, and document highlights.
- Locations of definitions and type definitions.
- Locations of declarations and references.
- Completions, completion item resolve.
- Getting code actions, resolving them, then applying the edits.
- Get InfoTrees of theorems (includes rudimentary parsing).
- Module hierarchy: Get module info, imports, and reverse dependencies.
- Interactive diagnostics and widgets (experimental).
Missing LSP Interactions
- "Call hierarchy" is currently not reliable.
Might be implemented in the future:
workspace/symbol,workspace/didChangeWatchedFiles,workspace/applyEdit, ...textDocument/prepareRename,textDocument/rename$/lean/staleDependency
Potential Features
- Better Windows support
- Choose between
lean --serverandlake serve - Automatic testing (lean env setup) for non Debian-based systems
Documentation
Read the documentation at leanclient.readthedocs.io.
Run make docs to build the documentation locally.
Benchmarks
See documentation for more information.
Testing
make install # Installs python package and dev dependencies with uv
make test # Run all tests, also installs fresh lean env if not found
make test-profile # Run all tests with cProfile
Related Projects
Lean LSP Clients
Lean REPLs
- LeanDojo
- PyPantograph
- lean-repl-py
- repl
- minictx-eval
- LeanREPL
- LeanTool
- itp-interface
- LeanInteract
- LEAN SDK
- Kimina Lean Server
License & Citation
MIT licensed. See LICENSE for more information.
Citing this repository is highly appreciated but not required by the license.
@software{leanclient2025,
author = {Oliver Dressler},
title = {{leanclient: Python client to interact with the lean4 language server}},
url = {https://github.com/oOo0oOo/leanclient},
month = {1},
year = {2025}
}
1 maintainer
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Filter files by name, interpreter, ABI, and platform.
If you're not sure about the file name format, learn more about wheel file names.
Copy a direct link to the current filters
File details
Details for the file leanclient-0.13.0.tar.gz.
File metadata
- Download URL: leanclient-0.13.0.tar.gz
- Upload date:
- Size: 1.2 MB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via:
uv/0.7.15
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
dffba9499fc1467e2c17a49d184da36d744b171760d91887a572e5696aecb437
|
|
| MD5 |
1380696644f1fcabf2cec6886fa0e1c8
|
|
| BLAKE2b-256 |
1354f1d83a0917082c025f22004ba79dec2da0cbcc9456bc2c276cc5d71fd33c
|
File details
Details for the file leanclient-0.13.0-py3-none-any.whl.
File metadata
- Download URL: leanclient-0.13.0-py3-none-any.whl
- Upload date:
- Size: 60.7 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via:
uv/0.7.15
File hashes
| Algorithm | Hash digest | |
|---|---|---|
| SHA256 |
e4736f018dec00d91c443a8fc6eb998ec4f0114b495034f43cea5ee79ccd2a98
|
|
| MD5 |
a1f7fdfee7020af6372d45b950baefe3
|
|
| BLAKE2b-256 |
9b9a7e98a449f436132a5f47ad58ef8539ae1a1f7bf1d9145fcde28992565f49
|
