Set Lean Options from Python (set_option)

You can pass Lean options per request using the setOptions field on Command and FileCommand. This mirrors Lean’s set_option commands and lets you customize elaboration or pretty-printing on a per-request basis.

Shape

• setOptions is a list of pairs (Name, DataValue)
• Name is a list of components, e.g. ["pp", "unicode"]
• DataValue can be bool | int | str | Name

Example:

from lean_interact import Command, LeanServer, LeanREPLConfig

server = LeanServer(LeanREPLConfig())
print(server.run(Command(
    cmd="variable (n : Nat)\n#check n+0=n",
    setOptions=[(["pp", "raw"], True)],
)))

CommandResponse(messages=[Message(start_pos=Pos(line=2, column=0), severity='info', data='Eq.{1} Nat (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) _uniq.4 (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) _uniq.4 : Prop', end_pos=Pos(line=2, column=6))], env=0)

LeanInteract will also merge your setOptions with its own defaults when enabled (e.g., it may add (["Elab","async"], True) to enable parallel elaboration). Your explicitly provided options are appended and forwarded with the request.

Note

Options apply only to the single request you send; pass them again for subsequent calls