Welcome to leanclient’s Documentation

Overview

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 github repository 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 easiest way to get started is to check out this minimal example in Google Colab:

Open in 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

  1. 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=0, 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=0, character=5)
print(result)

# 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])

# Check the document content as seen by the LSP (changes are not written to disk).
print(sfc.get_file_content())

Contents