Server#
Class which manages a Pantograph instance. All calls to the kernel uses this interface.
- class pantograph.server.Server(imports: List[str] = ['Init'], project_path: str | None = None, lean_path: str | None = None, options: Dict[str, Any] = {}, core_options: List[str] = [], timeout: int = 60, buffer_limit: int | None = 1000000, _sync_init: bool = True)#
Main interaction instance with Pantograph.
Asynchronous and synchronous versions are provided for each function.
- check_compile(code: str, new_constants: bool = False, read_header: bool = False)#
Check if some Lean code compiles
- async check_compile_async(code: str, new_constants: bool = False, read_header: bool = False)#
Check if some Lean code compiles
- check_track(src: str, dst: str) CheckTrackResult#
Checks if dst file conforms to the specifications in src
- async check_track_async(src: str, dst: str) CheckTrackResult#
Checks if dst file conforms to the specifications in src
- async classmethod create(imports: List[str] = ['Init'], project_path: str | None = None, lean_path: str | None = None, options: Dict[str, Any] = {}, core_options: List[str] = [], timeout: int = 120, buffer_limit: int | None = 1000000, start: bool = True) Server#
timeout: Amount of time to wait for execution (in seconds) maxread: Maximum number of characters to read (especially important for large proofs and catalogs)
- env_add(name: str, levels: list[str], t: str, v: str, is_theorem: bool = True)#
Adds a definition to the environment.
NOTE: May have to accept additional parameters if the definition contains universe mvars.
- async env_add_async(name: str, levels: list[str], t: str, v: str, is_theorem: bool = True)#
Adds a definition to the environment.
NOTE: May have to accept additional parameters if the definition contains universe mvars.
- env_catalog(module_prefix: str | None = None, invert_filter: bool = False) list[str]#
Print all symbols in environment.
- async env_catalog_async(module_prefix: str | None = None, invert_filter: bool = False) list[str]#
Print all symbols in environment.
- env_inspect(name: str, print_value: bool = False, print_dependency: bool = False) Dict#
Print the type and dependencies of a constant.
- async env_inspect_async(name: str, print_value: bool = False, print_dependency: bool = False) Dict#
Print the type and dependencies of a constant.
- env_load(path: str)#
Load the current environment from a file
- async env_load_async(path: str)#
Load the current environment from a file
- env_module_read(module: str) dict#
Reads the content from one Lean module including what constants are in it.
- async env_module_read_async(module: str) dict#
Reads the content from one Lean module including what constants are in it.
- env_parse(src: str, category: str = 'tactic') Tuple[str, str]#
Parse an input using a syntax category’s parser. Returns the parsed component and the tail.
- async env_parse_async(src: str, category: str = 'tactic') Tuple[str, str]#
Parse an input using a syntax category’s parser. Returns the parsed component and the tail.
- env_save(path: str)#
Save the current environment to a file
- async env_save_async(path: str)#
Save the current environment to a file
- expr_type(expr: str) str#
Evaluate the type of a given expression. This gives an error if the input expr is ill-formed.
- async expr_type_async(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.
- async gc_async()#
Garbage collect deleted goal states to free up memory.
- goal_continue(target: GoalState, branch: GoalState) GoalState#
After finish searching target, resume search on branch
- async goal_continue_async(target: GoalState, branch: GoalState) GoalState#
After finish searching target, resume search on branch
- goal_load(path: str) GoalState#
Load a goal state from a file.
User is responsible for keeping track of the environment.
- async goal_load_async(path: str) GoalState#
Load a goal state from a file.
User is responsible for keeping track of the environment.
- async goal_start_async(expr: str) GoalState#
Create a goal state with one root goal, whose target is expr
- goal_subsume(state: ~pantograph.expr.GoalState, goal: ~pantograph.expr.Goal, candidates: list[~pantograph.expr.Goal], src_state: ~pantograph.expr.GoalState | None = None) -> (<enum 'Subsumption'>, typing.Optional[pantograph.expr.GoalState], typing.Optional[pantograph.expr.Goal])#
Detect subsumption by candidate goals
The candidate goals must all exist in src_state. If src_state is not provided, they must exist in state. Returns a new goal state if a subsumption does not lead to a cycle, and the subsumptor if there is any subsumption happening.
- async goal_subsume_async(state: ~pantograph.expr.GoalState, goal: ~pantograph.expr.Goal, candidates: list[~pantograph.expr.Goal], src_state: ~pantograph.expr.GoalState | None = None) -> (<enum 'Subsumption'>, typing.Optional[pantograph.expr.GoalState], typing.Optional[pantograph.expr.Goal])#
Detect subsumption by candidate goals
The candidate goals must all exist in src_state. If src_state is not provided, they must exist in state. Returns a new goal state if a subsumption does not lead to a cycle, and the subsumptor if there is any subsumption happening.
- goal_tactic(state: GoalState, tactic: str | TacticHave | TacticLet | TacticExpr | TacticDraft | TacticMode, site: Site = Site(goal_id=None, auto_resume=None)) GoalState#
Execute a tactic on goal_id of state
- async goal_tactic_async(state: GoalState, tactic: str | TacticHave | TacticLet | TacticExpr | TacticDraft | TacticMode, site: Site = Site(goal_id=None, auto_resume=None)) GoalState#
Execute a tactic on goal_id of state
- is_automatic()#
Check if the server is running in automatic mode
- load_definitions(snippet: str)#
Loads definitions in some Lean code and update the environment.
Existing goal states will not automatically inherit said definitions.
- async load_definitions_async(snippet: str)#
Loads definitions in some Lean code and update the environment.
Existing goal states will not automatically inherit said definitions.
- load_header(header: str)#
Loads the environment from a header. Set imports to [] during server creation to use this function.
- async load_header_async(header: str)#
Loads the environment from a header. Set imports to [] during server creation to use this function.
- load_sorry(src: str, binder_name: str | None = None, ignore_values: bool = False) list[SearchTarget]#
Condense search target into goals
- async load_sorry_async(src: str, binder_name: str | None = None, ignore_values: bool = False) list[SearchTarget]#
Condense search target into goals
- refactor_search_target(code: str, core_options: list[str] = []) str#
Combine multiple sorry`s into one `sorry using subtyping. It only supports flat dependency structures.
This feature is experimental and depends on the round-trip capabilities of the delaborator.
- async refactor_search_target_async(code: str, core_options: list[str] = []) str#
Combine multiple sorry`s into one `sorry using subtyping. It only supports flat dependency structures.
This feature is experimental and depends on the round-trip capabilities of the delaborator.
- restart()#
Restart the server
- async restart_async()#
Restart the server
- tactic_invocations(file_name: str | Path) list[CompilationUnit]#
Collect tactic invocation points in file, and return them.
- async tactic_invocations_async(file_name: str | Path) list[CompilationUnit]#
Collect tactic invocation points in file, and return them.
- pantograph.server.get_version() str#
Returns the current Pantograph version for diagnostics purposes.