Skip to content

Interface API

This page documents the interface classes used to communicate with the Lean REPL.

Commands

Command

lean_interact.interface.Command

Bases: BaseREPLQuery, CommandOptions

Command to be executed in the REPL. Attributes: cmd: The command to be executed. env: The environment to be used (optional). 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. all_tactics: If true, return all tactics used in the command with their associated information. root_goals: If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof. infotree: Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.

Source code in lean_interact/interface.py 
43
44
45
46
47
48
49
50
51
52
53
54
55
class Command(BaseREPLQuery, CommandOptions):
    """Command to be executed in the REPL.
    Attributes:
        cmd: The command to be executed.
        env: The environment to be used (optional). 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.
        all_tactics: If true, return all tactics used in the command with their associated information.
        root_goals: If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof.
        infotree: Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.
    """

    cmd: Annotated[str, Field(min_length=1)]
    env: int | None = None

FileCommand

lean_interact.interface.FileCommand

Bases: BaseREPLQuery, CommandOptions

Command for file operations in the REPL. Attributes: path: The path of the file to be operated on. all_tactics: If true, return all tactics used in the command with their associated information. root_goals: If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof. infotree: Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.

Source code in lean_interact/interface.py 
58
59
60
61
62
63
64
65
66
67
class FileCommand(BaseREPLQuery, CommandOptions):
    """Command for file operations in the REPL.
    Attributes:
        path: The path of the file to be operated on.
        all_tactics: If true, return all tactics used in the command with their associated information.
        root_goals: If true, return root goals, i.e. initial goals of all declarations in the command, even if they already have a proof.
        infotree: Return syntax information. Should be "full", "tactics", "original", or "substantive". Anything else is ignored.
    """

    path: Annotated[str, Field(min_length=1)]

ProofStep

lean_interact.interface.ProofStep

Bases: BaseREPLQuery

Proof step in the REPL. Attributes: proof_state: The proof state to start from. tactic: The tactic to be applied.

Source code in lean_interact/interface.py 
70
71
72
73
74
75
76
77
78
class ProofStep(BaseREPLQuery):
    """Proof step in the REPL.
    Attributes:
        proof_state: The proof state to start from.
        tactic: The tactic to be applied.
    """

    proof_state: Annotated[int, Field(alias="proofState")]
    tactic: Annotated[str, Field(min_length=1)]

PickleEnvironment

lean_interact.interface.PickleEnvironment

Bases: BaseREPLQuery

Environment for pickling in the REPL. Attributes: env: The environment to be used. pickle_to: The path to save the pickle file.

Source code in lean_interact/interface.py 
81
82
83
84
85
86
87
88
89
class PickleEnvironment(BaseREPLQuery):
    """Environment for pickling in the REPL.
    Attributes:
        env: The environment to be used.
        pickle_to: The path to save the pickle file.
    """

    env: int
    pickle_to: Annotated[str, Field(min_length=1, alias="pickleTo")]

UnpickleEnvironment

lean_interact.interface.UnpickleEnvironment

Bases: BaseREPLQuery

Environment for unpickling in the REPL. Attributes: unpickle_env_from: The path to the pickle file.

Source code in lean_interact/interface.py 
92
93
94
95
96
97
98
class UnpickleEnvironment(BaseREPLQuery):
    """Environment for unpickling in the REPL.
    Attributes:
        unpickle_env_from: The path to the pickle file.
    """

    unpickle_env_from: Annotated[str, Field(min_length=1, alias="unpickleEnvFrom")]

PickleProofState

lean_interact.interface.PickleProofState

Bases: BaseREPLQuery

Proof state for pickling in the REPL. Attributes: proof_state: The proof state to be pickled. pickle_to: The path to save the pickle file.

Source code in lean_interact/interface.py 
101
102
103
104
105
106
107
108
109
class PickleProofState(BaseREPLQuery):
    """Proof state for pickling in the REPL.
    Attributes:
        proof_state: The proof state to be pickled.
        pickle_to: The path to save the pickle file.
    """

    proof_state: Annotated[int, Field(alias="proofState")]
    pickle_to: Annotated[str, Field(min_length=1, alias="pickleTo")]

UnpickleProofState

lean_interact.interface.UnpickleProofState

Bases: BaseREPLQuery

Environment for unpickling in the REPL. Attributes: unpickle_proof_state_from: The path to the pickle file.

Source code in lean_interact/interface.py 
112
113
114
115
116
117
118
119
class UnpickleProofState(BaseREPLQuery):
    """Environment for unpickling in the REPL.
    Attributes:
        unpickle_proof_state_from: The path to the pickle file.
    """

    unpickle_proof_state_from: Annotated[str, Field(min_length=1, alias="unpickleProofStateFrom")]
    env: int | None = None

Responses

BaseREPLResponse

lean_interact.interface.BaseREPLResponse

Bases: REPLBaseModel

Base class for all Lean responses. Attributes: messages: List of messages in the response. sorries: List of sorries found in the submitted code.

Source code in lean_interact/interface.py 
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
class BaseREPLResponse(REPLBaseModel):
    """Base class for all Lean responses.
    Attributes:
        messages: List of messages in the response.
        sorries: List of sorries found in the submitted code.
    """

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

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

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

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

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

    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)

get_errors()

Return all error messages

Source code in lean_interact/interface.py 
216
217
218
def get_errors(self) -> list[Message]:
    """Return all error messages"""
    return [msg for msg in self.messages if msg.severity == "error"]

get_warnings()

Return all warning messages

Source code in lean_interact/interface.py 
220
221
222
def get_warnings(self) -> list[Message]:
    """Return all warning messages"""
    return [msg for msg in self.messages if msg.severity == "warning"]

has_errors()

Check if response contains any error messages

Source code in lean_interact/interface.py 
224
225
226
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(start_pos=None, end_pos=None, allow_sorry=True)

Check if the submitted code is valid Lean code.

Source code in lean_interact/interface.py 
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
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)

CommandResponse

lean_interact.interface.CommandResponse

Bases: BaseREPLResponse

Response to a command in the REPL. Attributes: env: The environment state after running the code in the command tactics: List of tactics in the code. Returned only if all_tactics is true. infotree: The infotree of the code. Returned only if infotree is true. messages: List of messages in the response. sorries: List of sorries found in the submitted code.

Source code in lean_interact/interface.py 
249
250
251
252
253
254
255
256
257
258
259
260
261
class CommandResponse(BaseREPLResponse):
    """Response to a command in the REPL.
    Attributes:
        env: The environment state after running the code in the command
        tactics: List of tactics in the code. Returned only if `all_tactics` is true.
        infotree: The infotree of the code. Returned only if `infotree` is true.
        messages: List of messages in the response.
        sorries: List of sorries found in the submitted code.
    """

    env: int
    tactics: list[Tactic] = Field(default_factory=list)
    infotree: list | None = None

ProofStepResponse

lean_interact.interface.ProofStepResponse

Bases: BaseREPLResponse

Response to a proof step in the REPL. Attributes: proof_status: The proof status of the whole proof. Possible values: Completed, Incomplete, Error. proof_state: The proof state after the proof step. goals: List of goals after the proof step. traces: List of traces in the proof step. messages: List of messages in the response. sorries: List of sorries found in the submitted code.

Source code in lean_interact/interface.py 
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
class ProofStepResponse(BaseREPLResponse):
    """Response to a proof step in the REPL.
    Attributes:
        proof_status: The proof status of the whole proof. Possible values: `Completed`, `Incomplete`, `Error`.
        proof_state: The proof state after the proof step.
        goals: List of goals after the proof step.
        traces: List of traces in the proof step.
        messages: List of messages in the response.
        sorries: List of sorries found in the submitted code.
    """

    proof_status: Annotated[str, Field(alias="proofStatus")]
    proof_state: Annotated[int, Field(alias="proofState")]
    goals: list[str] = Field(default_factory=list)
    traces: list[str] = Field(default_factory=list)

Helper Classes

Message

lean_interact.interface.Message

Bases: REPLBaseModel

Message in the REPL. Attributes: start_pos: The starting position of the message. end_pos: The ending position of the message. severity: The severity of the message. data: The data associated with the message.

Source code in lean_interact/interface.py 
140
141
142
143
144
145
146
147
148
149
150
151
152
class Message(REPLBaseModel):
    """Message in the REPL.
    Attributes:
        start_pos: The starting position of the message.
        end_pos: The ending position of the message.
        severity: The severity of the message.
        data: The data associated with the message.
    """

    start_pos: Annotated[Pos, Field(alias="pos")]
    end_pos: Annotated[Pos | None, Field(alias="endPos")] = None
    severity: Literal["error", "warning", "info", "trace"]
    data: str

Sorry

lean_interact.interface.Sorry

Bases: REPLBaseModel

Sorry message in the REPL. Attributes: start_pos: The starting position of the sorry message. end_pos: The ending position of the sorry message. goal: The proof goal at the sorry location. proof_state: The proof state associated to the sorry.

Source code in lean_interact/interface.py 
155
156
157
158
159
160
161
162
163
164
165
166
167
class Sorry(REPLBaseModel):
    """Sorry message in the REPL.
    Attributes:
        start_pos: The starting position of the sorry message.
        end_pos: The ending position of the sorry message.
        goal: The proof goal at the sorry location.
        proof_state: The proof state associated to the sorry.
    """

    start_pos: Annotated[Pos | None, Field(alias="pos")] = None
    end_pos: Annotated[Pos | None, Field(alias="endPos")] = None
    goal: str
    proof_state: Annotated[int | None, Field(alias="proofState")] = None

Pos

lean_interact.interface.Pos

Bases: REPLBaseModel

Source code in lean_interact/interface.py 
125
126
127
128
129
130
131
132
133
134
135
136
137
class Pos(REPLBaseModel):
    line: int
    column: int

    def __le__(self, other: "Pos") -> bool:
        if self.line < other.line:
            return True
        if self.line == other.line:
            return self.column <= other.column
        return False

    def __lt__(self, other: "Pos") -> bool:
        return self <= other and not self == other

Tactic

lean_interact.interface.Tactic

Bases: REPLBaseModel

Tactic in the REPL. Attributes: start_pos: The starting position of the tactic. end_pos: The ending position of the tactic. goals: The goals associated with the tactic. tactic: The applied tactic. proof_state: The proof state associated with the tactic. used_constants: The constants used in the tactic.

Source code in lean_interact/interface.py 
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
class Tactic(REPLBaseModel):
    """Tactic in the REPL.
    Attributes:
        start_pos: The starting position of the tactic.
        end_pos: The ending position of the tactic.
        goals: The goals associated with the tactic.
        tactic: The applied tactic.
        proof_state: The proof state associated with the tactic.
        used_constants: The constants used in the tactic.
    """

    start_pos: Annotated[Pos, Field(alias="pos")]
    end_pos: Annotated[Pos, Field(alias="endPos")]
    goals: str
    tactic: str
    proof_state: Annotated[int | None, Field(alias="proofState")] = None
    used_constants: Annotated[list[str], Field(default_factory=list, alias="usedConstants")]