leanclient

https://leanclient.readthedocs.io/en/latest/
Admin
leanclient is a Python library that provides a thin wrapper around the native Lean language server...
Tokens:3,915
Snippets:31
Trust Score:9.6
Update:1 month ago
Show doc for...
Tokens:
Raw
### Install leanclient with pip

Source: https://leanclient.readthedocs.io/en/latest/_sources/index.rst.txt

Install the leanclient package using pip. This is the second step in the quickstart setup.

```bash
pip install leanclient
```

--------------------------------

### Install leanclient and use LeanLSPClient to query and update Lean files

Source: https://leanclient.readthedocs.io/en/latest/index.html

Install leanclient with pip, then start a LeanLSPClient, query goals, update a file, and inspect the LSP's view of the document. The Python example shows the core API: LeanLSPClient, create_file_client, get_goal, get_term_goal, DocumentContentChange, update_file, and get_file_content. Note that file changes are not written to disk.

```bash
pip install leanclient

```

```python
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())

```

--------------------------------

### Use leanclient to query and modify Lean files

Source: https://leanclient.readthedocs.io/en/latest/_sources/index.rst.txt

Python example showing how to start a LeanLSPClient, query goals, create a SingleFileClient, update a file, and check the LSP's view of the document. Requires a Lean project root with lakefile.toml.

```python
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())
```

--------------------------------

### Parallel processing with LeanClientPool

Source: https://leanclient.readthedocs.io/en/latest/_sources/benchmarks.rst.txt

Process multiple files in parallel using a LeanClientPool with multiple separate Lean language servers. Configure num_workers per CPU cores and batch_size for parallel file opening (faster but uses more memory).

```python
def count_tokens(client):
  return len(client.get_semantic_tokens())

with LeanClientPool(PROJECT_PATH, num_workers=4) as pool:
  results = pool.map(count_tokens, files, batch_size=4)
```
Tokens:
Raw