leanclient 0.1.0b9

Interact with the Lean theorem prover language server

leanclient

Interact with the lean4 language server in Python.

leanclient is a thin Python wrapper around the native Lean language server. It enables interaction with a Lean 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.
• Synchronous: Requests block until a response is received.
• 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

3. In your python code:

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"
result = client.get_goal(file_path, line=1, character=2)
print(result)

# Use a SingleFileClient for simplified interaction with a single file.
sfc = client.create_file_client(file_path)
result = sfc.get_term_goal(line=1, character=2)
print(result)

# Use a LeanClientPool for easy parallel processing multiple files.
files = ["MyProject/Basic.lean", "Main.lean"]

# Define a function that takes a SingleFileClient as its only parameter.
def count_tokens(client: lc.SingleFileClient):
    return len(client.get_semantic_tokens())

with lc.LeanClientPool(PROJECT_PATH, num_workers=8) as pool:
    results = pool.map(count_tokens, files)

    # Or use pool.submit() for increased control.
    futures = [pool.submit(count_tokens, path) for path in files]
    res_fut = [f.get() for f in futures]

print(results)

Currently in Beta

• Needs more testing with different setups.
• Any feedback is appreciated!

Implemented LSP Interactions

See the documentation for more information on:

• Opening, updating and closing files.
• Diagnostic information: Errors, warnings etc
• 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.

Missing LSP Interactions

• Call hierarchy is currently not reliable.

Might be implemented in the future:

• textDocument/codeAction
• 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

• Choose between lean --server and lake serve
• Parallel implementation (multiple requests in-flight) like multilspy
• Automatic testing (lean env setup) for non Debian-based systems
• Use document versions to handle evolving file states
• Allow interaction before waitForDiagnostics returns

Documentation

Read the documentation at leanclient.readthedocs.io.

Run make docs to build the documentation locally.

Benchmarks

See documentation for more information.

Testing

# python3 -m venv venv  # Or similar: Create environment
make install            # Installs python package and dev dependencies
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

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