leanclient 0.7.0

Interact with the Lean theorem prover language server

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:

1. Setup a new lean project or use an existing one. See the colab notebook for a basic Ubuntu setup.

2. Install the package:

pip install leanclient
# Or with uv:
uv pip install leanclient

3. 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.

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

Internal Lean methods:

• $/lean/rpc/connect, $/lean/rpc/call, $/lean/rpc/release, $/lean/rpc/keepAlive
• Interactive diagnostics
• $/lean/staleDependency

Potential Features

• Better Windows support
• Choose between lean --server and lake 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

• vscode-lean4
• lean-client-js
• lean-client-python
• communicating-with-lean

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}
}