lean_runner.proof package

Submodules

lean_runner.proof.proto module

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

Bases: Enum

The status of a Lean proof verification.

ERROR = 'error'

FINISHED = 'finished'

PENDING = 'pending'

RUNNING = 'running'

class lean_runner.proof.proto.Proof(*, id: str)

Bases: BaseModel

Represents a proof task submitted to the server.

id: str

model_config: ClassVar[ConfigDict] = {}

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

class lean_runner.proof.proto.ProofConfig(*, 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 proof verification 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_runner.proof.proto.ProofResult(*, success: bool | None = None, status: LeanProofStatus, result: dict | None = None, error_message: str | None = None)

Bases: BaseModel

The result of a proof verification.

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

Module contents