Server

Class which manages a Pantograph instance. All calls to the kernel uses this interface.

class pantograph.server.Server(imports=['Init'], project_path=None, lean_path=None, options={}, core_options=['maxHeartbeats=0', 'maxRecDepth=100000'], timeout=120, maxread=1000000)

Main interaction instance with Pantograph

expr_type(expr: str) → str

Evaluate the type of a given expression. This gives an error if the input expr is ill-formed.

gc()

Garbage collect deleted goal states to free up memory.

goal_conv_begin(state: GoalState, goal_id: int) → GoalState

Start conversion tactic mode on one goal

goal_conv_end(state: GoalState) → GoalState

Exit conversion tactic mode on all goals

goal_start(expr: str) → GoalState

Create a goal state with one root goal, whose target is expr

goal_tactic(state: GoalState, goal_id: int, tactic: str | TacticHave | TacticLet | TacticCalc | TacticExpr) → GoalState

Execute a tactic on goal_id of state

is_automatic()

Check if the server is running in automatic mode

load_sorry(content: str) → list[CompilationUnit]

Executes the compiler on a Lean file. For each compilation unit, either return the gathered sorry s, or a list of messages indicating error.

tactic_invocations(file_name: str | Path) → list[CompilationUnit]

Collect tactic invocation points in file, and return them.

exception pantograph.server.ServerError

Indicates a logical error in the server.

exception pantograph.server.TacticFailure

Indicates a tactic failed to execute

class pantograph.server.TestServer(methodName='runTest')

pantograph.server.get_lean_path(project_path)

Extracts the LEAN_PATH variable from a project path.