lean_server.manager package

Submodules

lean_server.manager.proof_manager module

Manages the lifecycle of Lean proofs, from submission to execution and result retrieval.

class lean_server.manager.proof_manager.ProofManager(*, proof_database: ProofDatabase, lean_semaphore: Semaphore, background_tasks: set[Task])[source]

Bases: object

Handles the submission, execution, and tracking of Lean proofs.

This class coordinates with the database to store proof data and results. It uses a semaphore to limit concurrent proof executions and manages background tasks for running proofs asynchronously.

proof_database

An instance for interacting with the proof database.

Type:

ProofDatabase

lean_semaphore

A semaphore to limit concurrent Lean processes.

Type:

asyncio.Semaphore

background_tasks

A set of currently running background proof tasks.

Type:

set[asyncio.Task]

async get_result(proof_id: str) → LeanProofResult[source]

Retrieves the result of a proof from the database.

Parameters:

proof_id – The unique identifier of the proof.

Returns:

The result of the proof.

async run_proof(*, proof: LeanProof, config: LeanProofConfig) → LeanProofResult[source]

Executes a single Lean proof.

This method acquires a semaphore lock before running the proof to control concurrency. It updates the proof’s status in the database before and after execution. If the proof result already exists in the database, it skips execution and returns the stored result.

Parameters:

  • proof – The LeanProof object to execute.

  • config – The configuration for the proof execution.

Returns:

The result of the proof execution.

async submit_proof(*, proof: LeanProof, config: LeanProofConfig) → dict[str, str][source]

Submits a proof for execution.

If the proof already exists, its ID is returned immediately. Otherwise, it’s added to the database and a background task is created to run it.

Parameters:

  • proof – The LeanProof object to be executed.

  • config – The configuration for the proof execution.

Returns:

A dictionary containing the unique ID of the proof.

Module contents