lean_runner.client package

Subpackages

• lean_runner.client.aio package
  • Submodules
  • lean_runner.client.aio.client module
    • AsyncLeanClient
      • AsyncLeanClient.close()
      • AsyncLeanClient.get_result()
      • AsyncLeanClient.submit()
      • AsyncLeanClient.verify()
      • AsyncLeanClient.verify_all()
  • Module contents

Submodules

lean_runner.client.client module

class lean_runner.client.client.LeanClient(base_url: str)

Bases: object

A client for interacting with the Lean Server API.

This client provides both synchronous and asynchronous methods for making API calls. The asynchronous client is available via the aio attribute.

close()

Closes the client session.

get_result(proof: Proof) → ProofResult

Retrieves the result of a proof submission.

Parameters:

proof – A Proof object.

Returns:

A ProofResult object.

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

Submits a proof to the /prove/submit endpoint synchronously.

Parameters:

• proof – The proof content. Can be: - A string containing the proof. - A Path object pointing to a file containing the proof. - A string path to a file containing the proof.

• config – An optional dictionary for proof configuration.

Returns:

A Proof object representing the submitted job.

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

Sends a proof to the /prove/check endpoint synchronously.

Parameters:

• proof – The proof content. Can be: - A string containing the proof. - A Path object pointing to a file containing the proof. - A string path to a file containing the proof.

• config – An optional dictionary for proof configuration.

Returns:

A dictionary containing the server’s response.

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

Verifies a collection of proofs concurrently using a thread pool.

This function is designed to be memory-efficient. It yields results as they are completed, making it suitable for very large collections of proofs.

Parameters:

• proofs – An 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.

• progress_bar – Whether to display a progress bar.

Yields:

ProofResult – The result of each verification as it completes.

Module contents