lean_runner package

Subpackages

• lean_runner.client package
  • Subpackages
    • lean_runner.client.aio package
      • Submodules
      • lean_runner.client.aio.client module
      • Module contents
  • Submodules
  • lean_runner.client.client module
    • LeanClient
      • LeanClient.close()
      • LeanClient.get_result()
      • LeanClient.submit()
      • LeanClient.verify()
      • LeanClient.verify_all()
  • Module contents
• lean_runner.proof package
  • Submodules
  • lean_runner.proof.proto module
    • LeanProofStatus
      • LeanProofStatus.ERROR
      • LeanProofStatus.FINISHED
      • LeanProofStatus.PENDING
      • LeanProofStatus.RUNNING
    • Proof
      • Proof.id
      • Proof.model_config
    • ProofConfig
      • ProofConfig.all_tactics
      • ProofConfig.ast
      • ProofConfig.memory_limit_mb
      • ProofConfig.model_config
      • ProofConfig.premises
      • ProofConfig.tactics
      • ProofConfig.timeout
    • ProofResult
      • ProofResult.error_message
      • ProofResult.model_config
      • ProofResult.result
      • ProofResult.status
      • ProofResult.success
  • Module contents

Module contents

class lean_runner.AsyncLeanClient(base_url: str, timeout: float = 300.0)

Bases: object

An asynchronous client for interacting with the Lean Server API.

async close()

Closes the httpx client session.

async get_result(proof: Proof) → ProofResult

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

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

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]

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.

class lean_runner.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.