leanclient

What it is and what it does

leanclient is a thin Python wrapper around the Lean 4 language server, enabling programmatic interaction with Lean files and projects. It exposes LSP operations like querying diagnostics, retrieving document symbols (theorems, definitions), getting hover information, updating file content in memory, and exploring module hierarchies through dependency graphs. The package is designed for batch processing and automation tasks where you need to interact with Lean code from Python without building a full IDE.

The package depends on orjson for JSON serialization, psutil for system monitoring, and tqdm for progress indication. It requires Python 3.10 or later and expects a Lean project with a lakefile.toml to be present. Most operations are implemented, though call hierarchy is noted as unreliable and some workspace-level operations remain unimplemented.

Use it for:

• Batch-process multiple Lean files to extract diagnostics, symbols, or type information for analysis or documentation generation.
• Automate theorem proving workflows by programmatically querying goals, hover info, and code actions within a Lean project.
• Build tooling that inspects module dependencies and reverse-dependency graphs to understand Lean library structure.
• Integrate Lean verification into Python-based research or testing pipelines that need to check Lean code correctness.
• Develop IDE-like features or editor plugins that delegate Lean interactions to a subprocess via this client.

Worth the install?

AI-flagged interpretation of the facts on this page — verify before relying

Interact with a Lean 4 language server running in a subprocess via Python, querying and modifying Lean files through the Language Server Protocol.

Yes, if you need programmatic access to Lean 4 from Python and have a working Lean project environment. The package is permissively licensed, has low install friction, and is actively maintained. However, it is very new (first release January 2025), so expect potential API changes and incomplete feature coverage; the Windows support caveat and experimental status of some features warrant caution in production use.

Install

leanclient on PyPI

pip install leanclient

uv add leanclient

poetry add leanclient

Installing leanclient

Before you install

Low install friction with a pure Python wheel and only three runtime dependencies (orjson, psutil, tqdm). Repository is active with recent commits and no archived status, though the project is very new (first release January 2025).

License in practice

MIT licensed under permissive terms, allowing free use, modification, and distribution with minimal restrictions.

Quickstart

pip install leanclient

import leanclient as lc

PROJECT_PATH = "path/to/your/lean/project/root/"
client = lc.LeanLSPClient(PROJECT_PATH)
diagnostics = client.get_diagnostics("MyProject/Basic.lean")
print(f"Found {len(diagnostics)} diagnostics")

Requires a working Lean 4 project with lakefile.toml in the specified PROJECT_PATH; Lean 4 and lake must be installed and accessible on the system.

Verify before relying

• Whether Lean 4 and a working Lean project setup are required prerequisites beyond Python 3.10.
• Performance characteristics on Windows, given the documentation mentions 'Better Windows support' as a potential future feature.
• Stability of experimental features like interactive diagnostics and widgets.

Package facts

Evidence: leanclient-0.13.0-py3-none-any.whl

Tags

More Software Development packages