lean_runner.client.aio package

Submodules

lean_runner.client.aio.client module

class lean_runner.client.aio.client.AsyncLeanClient(base_url: str, timeout: float = 300.0)[source]

Bases: object

An asynchronous client for interacting with the Lean Server API.

async close()[source]

Closes the httpx client session.

async get_result(proof: Proof) → ProofResult[source]

Gets the result of a proof by its task ID.

Parameters:

proof – A Proof object containing the task ID.

Returns:

A ProofResult object containing the proof result.

async submit(proof: str | Path | PathLike | Path, config: ProofConfig | None = None) → Proof[source]

Submits a proof asynchronously.

This method sends the proof to the server’s /prove/submit endpoint and immediately returns a Proof object containing the task ID. The result can be retrieved later using the get_result method with this ID.

Parameters:

  • proof – The proof content, which can be a string, Path, or os.PathLike

  • object.

  • config – The proof configuration.

Returns:

A Proof object representing the submitted task.

async verify(proof: str | Path | PathLike | Path, config: ProofConfig | None = None) → ProofResult[source]

Verifies a proof asynchronously.

This method sends the proof to the server’s /prove/check endpoint and waits for the server to return the verification result. This is a blocking call that waits for the verification to complete.

Parameters:

  • proof – The proof content, which can be a string, Path, or os.PathLike

  • object.

  • config – The proof configuration.

Returns:

A ProofResult object containing the verification result.

async verify_all(proofs: Iterable[str | Path | PathLike | Path] | AsyncIterable[str | Path | PathLike | Path], config: ProofConfig | None = None, total: int | None = None, max_workers: int = 128, progress_bar: bool = True) → AsyncIterable[ProofResult][source]

Verifies a collection of proofs concurrently using a producer-consumer model.

This function is designed to be memory-efficient. It uses a bounded queue to prevent the producer from reading the entire iterator into memory, making it suitable for very large collections of proofs.

Parameters:

  • proofs – An iterable or async iterable of proofs to verify.

  • config – The proof configuration.

  • total – The total number of proofs (for the progress bar). If not provided, it’s inferred from len(proofs) if available.

  • max_workers – The maximum number of concurrent verification tasks (consumers).

  • progress_bar – Whether to display a progress bar.

Yields:

ProofResult – The result of each verification as it completes.

Module contents