lean_server.database package

Submodules

lean_server.database.proof module

This module provides a database interface for storing and managing Lean proofs.

class lean_server.database.proof.ProofDatabase(database_path: str, timeout: int)[source]

Bases: object

Handles all database operations related to Lean proofs.

This class manages an SQLite database to store proof information, including the proof code, configuration, results, and status. It uses aiosqlite for asynchronous database access.

sql_path

The file path to the SQLite database.

Type:

str

timeout

The timeout in seconds for database connections.

Type:

int

async static calc_proof_hash(lean_code: str) → str[source]

Calculates the xxhash 64-bit hash of the Lean code.

Parameters:

lean_code – The Lean code to hash.

Returns:

The hex digest of the hash.

async clean_db(*, seconds: int = 0)[source]

Clean the database by removing old records older than 24 hours.

async create_table()[source]

Creates the necessary tables in the database if they don’t already exist.

async fetch(query: str, batch_size: int = 100) → AsyncIterator[dict][source]

Fetch data from the database using a Producer/Consumer pattern for efficient batch processing.

Parameters:

  • query – SQL query string to execute

  • batch_size – Number of rows to fetch per batch

Yields:

dict – Each row as a dictionary with column names as keys

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

Retrieves the result of a proof from the database.

It first checks the status and then retrieves the full result if the proof is finished or has an error.

Parameters:

proof_id – The ID of the proof.

Returns:

A LeanProofResult object.

async insert_hash(*, proof: LeanProof) → None[source]

Inserts the hash of a proof’s code into the ‘hash’ table.

Parameters:

proof – The LeanProof object.

async insert_proof(*, proof: LeanProof, config: LeanProofConfig, result: LeanProofResult) → str[source]

Inserts a completed proof’s data into the ‘proof’ table.

Parameters:

  • proof – The LeanProof object.

  • config – The configuration used for the proof.

  • result – The result of the proof execution.

Returns:

The ID of the inserted proof.

async proof_exists(*, proof: LeanProof) → str | None[source]

Checks if a proof with the same code already exists in the database.

Parameters:

proof – The LeanProof object.

Returns:

The ID of the existing proof if found, otherwise None.

async result_exists(*, proof_id: str) → bool[source]

Checks if a result for a given proof ID exists in the ‘proof’ table.

Parameters:

proof_id – The ID of the proof.

Returns:

True if the result exists, False otherwise.

async update_status(*, proof_id: str, status: LeanProofStatus)[source]

Updates the status of a proof in the ‘status’ table.

Parameters:

  • proof_id – The ID of the proof.

  • status – The new status of the proof.

Module contents