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
server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := id"))

CommandResponse(env=0)

The response contains:

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

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
server.run(Command(cmd="#check x", env=response1.env))

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

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
  • root_goals: Get information about goals in theorems and definitions
  • infotree: Get Lean infotree containing various informations about declarations and tactics

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._proof_1', 'Nat', 'of_eq_true', 'OfNat.ofNat', 'Eq'], start_pos=Pos(line=1, column=43), goals='n : Nat\n⊢ n = 5 → n = 5', end_pos=Pos(line=1, column=47))]

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(start_pos=Pos(line=1, column=40), proof_state=1, goal='n : Nat\n⊢ n = 5 → n = 5', end_pos=Pos(line=1, column=45))

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

It's good practice to handle errors that might occur during execution:

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(line=1, column=0), data='unexpected identifier; expected command', severity='error', end_pos=Pos(line=1, column=7))])

Next Steps

Now that you understand basic operations, you can: