Set Lean Options from Python (set_option)

Pass Lean options per request using the set_options field on Command and FileCommand. This mirrors Lean's set_option commands and allows customizing elaboration or pretty-printing on a per-request basis.

Shape

• set_options 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",
    set_options=[(["pp", "raw"], True)],
)))

CommandResponse(messages=[Message(end_pos=Pos(column=6, line=2), 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', start_pos=Pos(column=0, line=2), severity='info')], env=0)

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

Note

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