lean_dojo.interaction.dojo

class lean_dojo.interaction.dojo.CommandState(id: int, message: str | None = None)[source]

Bases: object

id: int

message: str | None = None

class lean_dojo.interaction.dojo.Dojo(entry: Theorem | Tuple[LeanGitRepo, Path, int], timeout: int = 600, additional_imports: List[str] = [])[source]

Bases: object

Gym-like environment for programmatic interaction with Lean through tactics or commands.

additional_imports: List[str]

entry: Theorem | Tuple[LeanGitRepo, Path, int]

file_path: Path

has_timedout: bool = False

is_crashed: bool = False

is_successful: bool | None = None

modified_file: TextIO

repo: LeanGitRepo

run_cmd(state: CommandState, command: str) → CommandState | LeanError[source]

run_tac(state: TacticState, tactic: str) → TacticState | ProofFinished | LeanError | ProofGivenUp[source]

property uses_commands: bool

property uses_tactics: bool

exception lean_dojo.interaction.dojo.DojoCrashError[source]

Bases: Exception

property is_out_of_memory: bool

exception lean_dojo.interaction.dojo.DojoInitError[source]: Bases: Exception

exception lean_dojo.interaction.dojo.DojoTacticTimeoutError[source]: Bases: Exception

class lean_dojo.interaction.dojo.LeanError(error: str)[source]

Bases: object

error: str

class lean_dojo.interaction.dojo.ProofFinished(tactic_state_id: int, message: str | None = None)[source]

Bases: object

message: str | None = None

tactic_state_id: int

class lean_dojo.interaction.dojo.ProofGivenUp[source]: Bases: object

class lean_dojo.interaction.dojo.TacticState(pp: str, id: int, message: str | None = None)[source]

Bases: object

goals: List[Goal]

id: int

message: str | None = None

property num_goals: int

pp: str

lean_dojo.interaction.dojo.kill_descendants(pid: int) → None[source]