leanclient 0.1.0b1

Interact with the Lean theorem prover language server

leanclient

leanclient is a thin 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 99% of time is spent waiting.
• Parallel: Easy batch processing of files using all your cores.

Currently in Beta

Not compatible with Lean 4.15.0 (stable) yet.

• The API is almost stable.
• There are missing features.
• Needs more testing with different setups.
• Any feedback is appreciated!

Next Features

• Documentation: Tutorial & examples
• Publishing on pipy

Potential Features

• Virtual files (no actual file on disk), only in-memory in lsp and client
• Use document versions to handle evolving file states
• Automatic lean env setup for non Debian-based systems
• Parallel implementation (multiple requests in-flight) like multilspy
• Allow interaction before waitForDiagnostics returns

Missing LSP Methods

Might be implemented in the future:

• callHierarchy/incomingCalls, callHierarchy/outgoingCalls, ...
• $/lean/rpc/connect, $/lean/rpc/call, $/lean/rpc/release, $/lean/rpc/keepAlive
• workspace/symbol, workspace/didChangeWatchedFiles, workspace/applyEdit, ...
• textDocument/prepareRename, textDocument/rename
• $/lean/ileanInfoUpdate, $/lean/ileanInfoFinal, $/lean/importClosure, $/lean/staleDependency

Run Tests

# 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

Documentation

Read the documentation at leanclient.readthedocs.io.

Run make docs to build the documentation locally.

License

MIT

Citing this repository is highly appreciated but not required by the license.