Interface

Module: lean_interact.interface

This module provides the base classes and data models for interacting with the Lean REPL (Read-Eval-Print Loop). It defines the request and response structures used for sending commands to the Lean server and receiving results. These are aligned with the Lean REPL's API.

Command

Bases: BaseREPLQuery, CommandOptions

Command to be executed in the REPL.

cmd instance-attribute

cmd: str

The command to be executed.

env class-attribute instance-attribute

env: int | None = None

The environment to be used. If env = None, starts a new session (in which you can use import). If env is set, the command is executed in the given environment.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

all_tactics class-attribute instance-attribute

all_tactics: bool | None = None

If true, return all tactics used in the command with their associated information.

root_goals class-attribute instance-attribute

root_goals: bool | None = None

If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof.

infotree class-attribute instance-attribute

infotree: str | None = None

Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.

FileCommand

Bases: BaseREPLQuery, CommandOptions

Command for file operations in the REPL.

path instance-attribute

path: str

The path of the file to be operated on.

env class-attribute instance-attribute

env: int | None = None

The environment to be used. If env = None, starts a new session (in which you can use import). If env is set, the command is executed in the given environment.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

all_tactics class-attribute instance-attribute

all_tactics: bool | None = None

If true, return all tactics used in the command with their associated information.

root_goals class-attribute instance-attribute

root_goals: bool | None = None

If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof.

infotree class-attribute instance-attribute

infotree: str | None = None

Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.

ProofStep

Bases: BaseREPLQuery

Proof step in the REPL.

proof_state instance-attribute

proof_state: int

The proof state to start from.

tactic instance-attribute

tactic: str

The tactic to be applied.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

PickleEnvironment

Bases: BaseREPLQuery

Environment for pickling in the REPL.

env instance-attribute

env: int

The environment to be pickled.

pickle_to instance-attribute

pickle_to: str

The path to save the pickle file.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

UnpickleEnvironment

Bases: BaseREPLQuery

Environment for unpickling in the REPL.

unpickle_env_from instance-attribute

unpickle_env_from: str

The path to the pickle file.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

PickleProofState

Bases: BaseREPLQuery

Proof state for pickling in the REPL.

proof_state instance-attribute

proof_state: int

The proof state to be pickled.

pickle_to instance-attribute

pickle_to: str

The path to save the pickle file.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

UnpickleProofState

Bases: BaseREPLQuery

Environment for unpickling in the REPL.

unpickle_proof_state_from instance-attribute

unpickle_proof_state_from: str

The path to the pickle file containing the proof state to be unpickled.

env class-attribute instance-attribute

env: int | None = None

The environment to be used as a context for unpickling.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

CommandResponse

CommandResponse(**data)

Bases: BaseREPLResponse

Response to a command in the REPL.

Source code in src/lean_interact/interface.py

def __init__(self, **data):
    if self.__class__ == BaseREPLResponse:
        raise TypeError("BaseResponse cannot be instantiated directly")
    super().__init__(**data)

env instance-attribute

env: int

The new environment state after running the code in the command.

tactics class-attribute instance-attribute

tactics: list[Tactic] = Field(default_factory=list)

List of tactics in the code. Returned only if all_tactics is true.

infotree class-attribute instance-attribute

infotree: list[InfoTree] | None = None

The infotree of the code. Returned only if infotree is true.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

messages class-attribute instance-attribute

messages: list[Message] = Field(default_factory=list)

List of messages in the response.

sorries class-attribute instance-attribute

sorries: list[Sorry] = Field(default_factory=list)

List of sorries found in the submitted code.

get_errors

get_errors() -> list[Message]

Return all error messages

Source code in src/lean_interact/interface.py

def get_errors(self) -> list[Message]:
    """Return all error messages"""
    return [msg for msg in self.messages if msg.severity == "error"]

get_warnings

get_warnings() -> list[Message]

Return all warning messages

Source code in src/lean_interact/interface.py

def get_warnings(self) -> list[Message]:
    """Return all warning messages"""
    return [msg for msg in self.messages if msg.severity == "warning"]

has_errors

has_errors() -> bool

Check if response contains any error messages

Source code in src/lean_interact/interface.py

def has_errors(self) -> bool:
    """Check if response contains any error messages"""
    return any(msg.severity == "error" for msg in self.messages)

lean_code_is_valid

lean_code_is_valid(
    start_pos: Pos | None = None,
    end_pos: Pos | None = None,
    allow_sorry: bool = True,
) -> bool

Check if the submitted code is valid Lean code.

Source code in src/lean_interact/interface.py

def lean_code_is_valid(
    self,
    start_pos: Pos | None = None,
    end_pos: Pos | None = None,
    allow_sorry: bool = True,
) -> bool:
    """Check if the submitted code is valid Lean code."""
    # check only the messages intersecting the code
    errors = [
        message
        for message in self.messages
        if message_intersects_code(message, start_pos, end_pos) and message.severity == "error"
    ]
    sorries = [message for message in self.sorries if message_intersects_code(message, start_pos, end_pos)] + [
        message
        for message in self.messages
        if message_intersects_code(message, start_pos, end_pos) and message.data == "declaration uses 'sorry'"
    ]
    return not errors and (allow_sorry or not sorries)

ProofStepResponse

ProofStepResponse(**data)

Bases: BaseREPLResponse

Response to a proof step in the REPL.

Source code in src/lean_interact/interface.py

def __init__(self, **data):
    if self.__class__ == BaseREPLResponse:
        raise TypeError("BaseResponse cannot be instantiated directly")
    super().__init__(**data)

proof_status instance-attribute

proof_status: str

The proof status of the whole proof. Possible values: Completed, Incomplete, Error. It may contain additional information, e.g. Incomplete: contains sorry.

proof_state instance-attribute

proof_state: int

The proof state after the proof step.

goals class-attribute instance-attribute

goals: list[str] = Field(default_factory=list)

List of goals after the proof step.

traces class-attribute instance-attribute

traces: list[str] = Field(default_factory=list)

List of traces in the proof step.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

messages class-attribute instance-attribute

messages: list[Message] = Field(default_factory=list)

List of messages in the response.

sorries class-attribute instance-attribute

sorries: list[Sorry] = Field(default_factory=list)

List of sorries found in the submitted code.

get_errors

get_errors() -> list[Message]

Return all error messages

Source code in src/lean_interact/interface.py

def get_errors(self) -> list[Message]:
    """Return all error messages"""
    return [msg for msg in self.messages if msg.severity == "error"]

get_warnings

get_warnings() -> list[Message]

Return all warning messages

Source code in src/lean_interact/interface.py

def get_warnings(self) -> list[Message]:
    """Return all warning messages"""
    return [msg for msg in self.messages if msg.severity == "warning"]

has_errors

has_errors() -> bool

Check if response contains any error messages

Source code in src/lean_interact/interface.py

def has_errors(self) -> bool:
    """Check if response contains any error messages"""
    return any(msg.severity == "error" for msg in self.messages)

lean_code_is_valid

lean_code_is_valid(
    start_pos: Pos | None = None,
    end_pos: Pos | None = None,
    allow_sorry: bool = True,
) -> bool

Check if the submitted code is valid Lean code.

Source code in src/lean_interact/interface.py

def lean_code_is_valid(
    self,
    start_pos: Pos | None = None,
    end_pos: Pos | None = None,
    allow_sorry: bool = True,
) -> bool:
    """Check if the submitted code is valid Lean code."""
    # check only the messages intersecting the code
    errors = [
        message
        for message in self.messages
        if message_intersects_code(message, start_pos, end_pos) and message.severity == "error"
    ]
    sorries = [message for message in self.sorries if message_intersects_code(message, start_pos, end_pos)] + [
        message
        for message in self.messages
        if message_intersects_code(message, start_pos, end_pos) and message.data == "declaration uses 'sorry'"
    ]
    return not errors and (allow_sorry or not sorries)

LeanError

Bases: REPLBaseModel

Represents an error in the Lean REPL.

message class-attribute instance-attribute

message: str = ''

The error message.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

Message

Bases: REPLBaseModel

Message in the REPL.

start_pos instance-attribute

start_pos: Pos

The starting position of the message.

end_pos class-attribute instance-attribute

end_pos: Pos | None = None

The ending position of the message.

severity instance-attribute

severity: Literal['error', 'warning', 'info', 'trace']

The severity of the message. Possible values: error, warning, info, trace.

data instance-attribute

data: str

The data associated with the message.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

Pos

Bases: REPLBaseModel

Position in the Lean code.

line instance-attribute

line: int

The line number of the position.

column instance-attribute

column: int

The column number of the position.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

Range

Bases: REPLBaseModel

Range of a Syntax object.

synthetic instance-attribute

synthetic: bool

Whether the syntax is synthetic or not.

start instance-attribute

start: Pos

The starting position of the syntax.

finish instance-attribute

finish: Pos

The ending position of the syntax.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

Sorry

Bases: REPLBaseModel

Sorry message in the REPL.

start_pos class-attribute instance-attribute

start_pos: Pos | None = None

The starting position of the sorry message.

end_pos class-attribute instance-attribute

end_pos: Pos | None = None

The ending position of the sorry message.

goal instance-attribute

goal: str

The proof goal at the sorry location.

proof_state class-attribute instance-attribute

proof_state: int | None = None

The proof state associated to the sorry.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

Tactic

Bases: REPLBaseModel

Tactic in the REPL.

start_pos instance-attribute

start_pos: Pos

The starting position of the tactic.

end_pos instance-attribute

end_pos: Pos

The ending position of the tactic.

goals instance-attribute

goals: str

The goals associated with the tactic.

tactic instance-attribute

tactic: str

The applied tactic.

proof_state class-attribute instance-attribute

proof_state: int | None = None

The proof state associated with the tactic.

used_constants instance-attribute

used_constants: list[str]

The constants used in the tactic.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

InfoTree

Bases: REPLBaseModel

An InfoTree representation of the Lean code.

node instance-attribute

node: Node

The root node of the InfoTree, which can be a TacticNode, CommandNode, TermNode, or None.

kind instance-attribute

kind: Literal[
    "TacticInfo",
    "TermInfo",
    "PartialTermInfo",
    "CommandInfo",
    "MacroExpansionInfo",
    "OptionInfo",
    "FieldInfo",
    "CompletionInfo",
    "UserWidgetInfo",
    "CustomInfo",
    "FVarAliasInfo",
    "FieldRedeclInfo",
    "ChoiceInfo",
    "DelabTermInfo",
]

The kind of the InfoTree.

children class-attribute instance-attribute

children: list[Self] = Field(default_factory=list)

Children of the InfoTree, which are also InfoTrees.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

dfs_walk

dfs_walk() -> Generator[Self, None, None]

Walk the InfoTree using Depth-First-Search.

Returns:

Type	Description
None	Yields the subsequent InfoTree.

Source code in src/lean_interact/interface.py

def dfs_walk(self) -> Generator[Self, None, None]:
    """
    Walk the InfoTree using Depth-First-Search.

    Returns:
        Yields the subsequent InfoTree.
    """
    # Had to do this iteratively, because recursively is slow and exceeds recursion depth
    stack = deque([self])

    while stack:
        first = stack.popleft()
        yield first
        stack.extendleft(first.children)

leaves

leaves() -> Generator[Self, None, None]

Get the InfoTree leaves of the Depth-First-Search

Returns:

Type	Description
None	Yield the leaves of the InfoTree.

Source code in src/lean_interact/interface.py

def leaves(self) -> Generator[Self, None, None]:
    """
    Get the InfoTree leaves of the Depth-First-Search

    Returns:
        Yield the leaves of the InfoTree.
    """
    for tree in self.dfs_walk():
        if not tree.children:
            yield tree

commands

commands() -> Generator[Self, None, None]

Get all InfoTrees that represent commands

Returns:

Type	Description
None	Yields the command nodes of the InfoTree.

Source code in src/lean_interact/interface.py

def commands(self) -> Generator[Self, None, None]:
    """
    Get all InfoTrees that represent commands

    Returns:
        Yields the command nodes of the InfoTree.
    """
    for tree in self.dfs_walk():
        if tree.kind != "CommandInfo":
            continue
        assert isinstance(tree.node, CommandNode)
        yield tree

variables

variables() -> Generator[Self, None, None]

Get children corresponding to variable expressions.

Returns:

Type	Description
None	Yields the variable nodes of the InfoTree.

Source code in src/lean_interact/interface.py

def variables(self) -> Generator[Self, None, None]:
    """
    Get children corresponding to variable expressions.

    Returns:
        Yields the variable nodes of the InfoTree.
    """
    for tree in self.commands():
        if tree.node.elaborator != "Lean.Elab.Command.elabVariable":  # type: ignore
            continue
        yield tree

theorems

theorems() -> Generator[Self, None, None]

Get children corresponding to theorems (including lemmas).

Returns:

Type	Description
None	Yields the theorems of the InfoTree.

Source code in src/lean_interact/interface.py

def theorems(self) -> Generator[Self, None, None]:
    """
    Get children corresponding to theorems (including lemmas).

    Returns:
         Yields the theorems of the InfoTree.
    """
    for tree in self.commands():
        if tree.node.stx.kind != "Lean.Parser.Command.declaration":  # type: ignore
            continue
        if tree.node.stx.arg_kinds[-1] != "Lean.Parser.Command.theorem":  # type: ignore
            continue
        yield tree

docs

docs() -> Generator[Self, None, None]

Get children corresponding to DocStrings.

Returns:

Type	Description
None	Yields the InfoTree nodes representing Docstrings.

Source code in src/lean_interact/interface.py

def docs(self) -> Generator[Self, None, None]:
    """
    Get children corresponding to DocStrings.

    Returns:
         Yields the InfoTree nodes representing Docstrings.
    """
    for tree in self.commands():
        if tree.node.elaborator != "Lean.Elab.Command.elabModuleDoc":  # type: ignore
            continue
        yield tree

namespaces

namespaces() -> Generator[Self, None, None]

Get children corresponding to namespaces.

Returns:

Type	Description
None	Yields the InfoTree nodes for namespaces.

Source code in src/lean_interact/interface.py

def namespaces(self) -> Generator[Self, None, None]:
    """
    Get children corresponding to namespaces.

    Returns:
         Yields the InfoTree nodes for namespaces.
    """
    for tree in self.commands():
        if tree.node.elaborator != "Lean.Elab.Command.elabNamespace":  # type: ignore
            continue
        yield tree

pp_up_to

pp_up_to(end_pos: Pos) -> str

Get the pretty-printed string of the InfoTree up to a given position.

Source code in src/lean_interact/interface.py

def pp_up_to(self, end_pos: Pos) -> str:
    """
    Get the pretty-printed string of the InfoTree up to a given position.
    """
    if self.node is None:
        raise ValueError("InfoTree node is None, cannot pretty-print!")
    if end_pos > self.node.stx.range.finish or end_pos < self.node.stx.range.start:
        raise ValueError("end_pos has to be in bounds!")
    if self.node.stx.pp is None:
        raise ValueError("InfoTree node has no pretty-printed string!")
    lines = self.node.stx.pp.splitlines(keepends=True)
    result = []
    for line_idx in range(end_pos.line + 1 - self.node.stx.range.start.line):
        line = lines[line_idx]
        if line_idx == end_pos.line - self.node.stx.range.start.line:
            line = line[: end_pos.column]
        result.append(line)
    return "".join(result)

theorem_for_sorry

theorem_for_sorry(sorry: Sorry) -> Self | None

Get the theorem InfoTree for a given sorry, if found in this tree.

Parameters:

Name	Type	Description	Default
sorry	Sorry	The sorry to search a theorem for	required

Returns:

Type	Description
Self | None	The found InfoTree, if found, else None

Source code in src/lean_interact/interface.py

def theorem_for_sorry(self, sorry: Sorry) -> Self | None:
    """
    Get the theorem InfoTree for a given sorry, if found in this tree.

    Args:
        sorry: The sorry to search a theorem for

    Returns:
        The found InfoTree, if found, else None
    """
    found = None
    for tree in self.theorems():
        thm_range = tree.node.stx.range  # type: ignore
        # Sorry inside
        if sorry.start_pos is None or sorry.end_pos is None:
            continue
        if sorry.start_pos < thm_range.start or sorry.end_pos > thm_range.finish:
            continue
        assert found is None
        found = tree
    return found

TacticNode

Bases: BaseNode

A tactic node of the InfoTree.

name instance-attribute

name: str | None

The name of the tactic, if available.

goals_before class-attribute instance-attribute

goals_before: list[str] = Field(
    default_factory=list, alias="goalsBefore"
)

Goals before tactic application.

goals_after class-attribute instance-attribute

goals_after: list[str] = Field(
    default_factory=list, alias="goalsAfter"
)

Goals after tactic application.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

stx instance-attribute

stx: Syntax

The syntax object of the node.

CommandNode

Bases: BaseNode

A command node of the InfoTree.

elaborator instance-attribute

elaborator: str

The elaborator used to elaborate the command.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

stx instance-attribute

stx: Syntax

The syntax object of the node.

TermNode

Bases: BaseNode

A term node of the InfoTree.

is_binder class-attribute instance-attribute

is_binder: bool = Field(alias='isBinder')

Whether the node is a binder or not.

expr instance-attribute

expr: str

The expression string of the term node.

expected_type class-attribute instance-attribute

expected_type: str | None = Field(
    default=None, alias="expectedType"
)

The expected type of the term node, if available.

elaborator instance-attribute

elaborator: str | None

The elaborator used for the term node, if available.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)

stx instance-attribute

stx: Syntax

The syntax object of the node.

Syntax

Bases: REPLBaseModel

Lean Syntax object.

pp instance-attribute

pp: str | None

The pretty-printed string of the syntax.

range instance-attribute

range: Range

The range of the syntax.

kind instance-attribute

kind: str

The kind of the syntax..

arg_kinds class-attribute instance-attribute

arg_kinds: list[str] = Field(
    default_factory=list, alias="argKinds"
)

The kinds of the arguments of the syntax.

model_config class-attribute instance-attribute

model_config = ConfigDict(
    frozen=True, extra="allow", populate_by_name=True
)