lean_server.proof package

Submodules

lean_server.proof.lean module

This module defines the LeanProof class for executing Lean proofs.

class lean_server.proof.lean.LeanProof(*, proof_id: str | None = None, proof: str, config: Config)

Bases: object

Represents a Lean proof that can be executed.

This class encapsulates the Lean code for a proof and provides a method to execute it as a subprocess. It handles communication with the Lean process, including timeouts and error handling.

lean_code

The Lean code of the proof.

Type:

str

proof_id

A unique identifier for the proof.

Type:

str

config

The application configuration.

Type:

Config

async execute(config: LeanProofConfig) → LeanProofResult

Executes the Lean proof as a subprocess.

This method runs the Lean executable, sends the proof code to it, and waits for the result. It handles timeouts, process errors, and JSON parsing of the output.

Parameters:

config – The configuration for this specific proof execution.

Returns:

A LeanProofResult object containing the status and result of the proof execution.

lean_server.proof.proto module

class lean_server.proof.proto.LeanProofConfig(*, all_tactics: bool = False, ast: bool = False, tactics: bool = False, premises: bool = False, timeout: float = 300.0, memory_limit_mb: int = 8192)

Bases: BaseModel

Configuration for a Lean proof request.

all_tactics: bool

ast: bool

memory_limit_mb: int

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

premises: bool

tactics: bool

timeout: float

class lean_server.proof.proto.LeanProofResult(*, success: bool | None = None, status: LeanProofStatus, result: dict | None = None, error_message: str | None = None)

Bases: BaseModel

The result of a Lean proof request.

error_message: str | None

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

result: dict | None

status: LeanProofStatus

success: bool | None

class lean_server.proof.proto.LeanProofStatus(*values)

Bases: Enum

The status of a Lean proof.

ERROR = 'error'

FINISHED = 'finished'

PENDING = 'pending'

RUNNING = 'running'

Module contents