Skip to content

Basic Usage

This guide covers the fundamental operations and command types in LeanInteract.

Basic Command Execution

The most common operation in LeanInteract is executing Lean code directly using the Command class:

from lean_interact import LeanREPLConfig, LeanServer, Command

# Setup
config = LeanREPLConfig()
server = LeanServer(config)

# Run a simple theorem
print(server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id")))

CommandResponse(env=0)

The response contains:

  • Messages returned by Lean if any (errors, information, etc.)
  • An environment state (env) that can be used for subsequent commands.

Working with Environment States

Each command execution creates a new environment state. You can use this state in subsequent commands:

# First command creates environment state
response1 = server.run(Command(cmd="def x := 5"))

# Use environment state 0 for the next command
print(server.run(Command(cmd="#check x", env=response1.env)))

CommandResponse(env=2, messages=[Message(start_pos=Pos(column=0, line=1), end_pos=Pos(column=6, line=1), data='x : Nat', severity='info')])

Processing Lean Files

You can process entire Lean files using the FileCommand class:

from lean_interact import FileCommand

# Process a Lean file
response = server.run(FileCommand(path="myfile.lean"))

# With options to get more information about goals
response = server.run(FileCommand(path="myfile.lean", root_goals=True))

Available Options

Both Command and FileCommand support several options:

  • all_tactics: Get information about tactics used
  • declarations: Extract fine-grained information about declarations in the code
  • root_goals: Get information about goals in theorems and definitions
  • infotree: Get Lean infotree containing various informations from the Lean syntax tree
  • incrementality: Enable or disable incremental elaboration for this specific command.
  • set_options: Set Lean options for this command (see Set Options)
  • env: The environment from a previous command to be used as context. If env = None, starts from scratch.

Example with options:

response = server.run(Command(
    cmd="theorem ex (n : Nat) : n = 5 → n = 5 := by simp",
    all_tactics=True
))
print(response.tactics)  # Shows tactics used

[Tactic(proof_state=0, tactic='simp', used_constants=['instOfNatNat', 'imp_self._simp_1', 'Nat', 'of_eq_true', 'OfNat.ofNat', 'Eq'], start_pos=Pos(column=43, line=1), goals='n : Nat\n⊢ n = 5 → n = 5', end_pos=Pos(column=47, line=1))]

Working with Sorries

When Lean code contains sorry (incomplete proofs), LeanInteract returns information about these sorry:

response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := sorry"))
print(response.sorries[0])

Sorry(proof_state=1, start_pos=Pos(column=40, line=1), end_pos=Pos(column=45, line=1), goal='n : Nat\n⊢ n = 5 → n = 5')

This response will include a list of Sorry objects, each containing:

  • Position in the code
  • Goal to be proven
  • Proof state ID (can be used with ProofStep commands)

Error Handling

from lean_interact.interface import LeanError

try:
    response = server.run(Command(cmd="invalid Lean code"))
    if isinstance(response, LeanError):
        print("Command failed with fatal error(s):", response.message)
    else:
        print("Command succeeded:", response) # but the content may contain errors !!
except Exception as e:
    print(f"An error occurred: {e}")

Command succeeded: CommandResponse(env=5, messages=[Message(start_pos=Pos(column=0, line=1), end_pos=Pos(column=7, line=1), data='unexpected identifier; expected command', severity='error')])

Next Steps