API Reference¶

This section contains the complete API reference for Pytanque.

Client Module¶

exception pytanque.client.PetanqueError(code, message)[source]¶

Bases: Exception

Exception raised for Petanque-specific errors.

Parameters:

codeint: Error code from the Petanque server.
messagestr: Error description from the server.

Attributes:

codeint: Error code.
messagestr: Error description.

Examples

>>> from pytanque import Pytanque, PetanqueError
>>> try:
...     with Pytanque("127.0.0.1", 8765) as client:
...         state = client.start("./nonexistent.v", "theorem")
... except PetanqueError as e:
...     print(f"Petanque error {e.code}: {e.message}")

__init__(code, message)[source]¶

class pytanque.client.Pytanque(host, port)[source]¶

Bases: object

Petanque client to communicate with the Rocq theorem prover using JSON-RPC over a simple socket.

The Pytanque class provides a high-level interface for interactive theorem proving with Rocq/Coq through the Petanque server. It supports context manager protocol for automatic connection management.

Key features include: - Execute tactics and commands with the run() method - Access proof states with feedback containing all Rocq messages - Parse AST of commands with ast() and ast_at_pos() - Navigate file positions with get_state_at_pos() and get_root_state() - Inspect goals, premises, and proof state information

Parameters:

hoststr: The hostname or IP address of the Petanque server.
portint: The port number of the Petanque server.

Attributes:

hoststr: Server hostname.
portint: Server port number.
idint: Current request ID for JSON-RPC.
socketsocket.socket: TCP socket for server communication.

Examples

>>> from pytanque import Pytanque
>>> with Pytanque("127.0.0.1", 8765) as client:
...     # Start a proof
...     state = client.start("./examples/foo.v", "addnC")
...
...     # Execute commands and check feedback
...     state = client.run(state, "induction n.", verbose=True)
...     for level, msg in state.feedback:
...         print(f"Rocq message: {msg}")
...
...     # Get AST of a command
...     ast = client.ast(state, "auto")
...     print("AST:", ast)
...
...     # Get state at specific position in file
...     pos_state = client.get_state_at_pos("./examples/foo.v", line=3, character=0)
...     print(f"State at position: {pos_state.st}")

__init__(host, port)[source]¶

Initialize a new Pytanque client instance.

Parameters:

hoststr: The hostname or IP address of the Petanque server.
portint: The port number of the Petanque server.

Examples

>>> client = Pytanque("127.0.0.1", 8765)
>>> client.connect()

ast(state, text)[source]¶

Get the Abstract Syntax Tree (AST) of a command parsed at a given state.

Parameters:

stateState: The proof state providing the parsing context.
textstr: The command text to parse (e.g., “induction n”, “Search nat”).

Returns:

dict: The AST representation of the parsed command.

Raises:

PetanqueError: If the text cannot be parsed in the given state context.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...
...     # Get AST for a tactic
...     ast = client.ast(state, "induction n.")
...     print("Tactic AST:", ast)
...
...     # Get AST for a search command
...     ast = client.ast(state, "Search nat.")
...     print("Search AST:", ast)
...
...     # Get AST for a complex expression
...     ast = client.ast(state, "fun x => x + 1.")
...     print("Expression AST:", ast)

ast_at_pos(file, line, character)[source]¶

Get the Abstract Syntax Tree (AST) at a specific position in a file.

Parameters:

filestr: Path to the Rocq/Coq file.
lineint: Line number (0-based indexing).
characterint: Character position within the line (0-based indexing).

Returns:

dict: The AST representation of the syntax element at the specified position.

Raises:

PetanqueError: If the position is invalid or the file cannot be parsed.
ValueError: If the file path is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     # Get AST at specific position in file
...     ast = client.ast_at_pos("./examples/foo.v", line=5, character=10)
...     print("AST at position:", ast)
...
...     # Get AST at theorem declaration
...     ast = client.ast_at_pos("./examples/foo.v", line=0, character=0)
...     print("Theorem declaration AST:", ast)
...
...     # Get AST at proof step
...     ast = client.ast_at_pos("./examples/foo.v", line=3, character=5)
...     print("Proof step AST:", ast)

close()[source]¶

Close the connection to the Petanque server.

Examples

>>> client = Pytanque("127.0.0.1", 8765)
>>> client.connect()
>>> client.close()

connect()[source]¶

Establish connection to the Petanque server.

Raises:

ConnectionError: If connection to the server fails.
OSError: If socket creation fails.

Examples

>>> client = Pytanque("127.0.0.1", 8765)
>>> client.connect()
>>> client.close()

get_root_state(file, opts=None)[source]¶

Get the initial (root) state of a document.

This method returns the very first state of the document, before any commands or proofs have been executed. It represents the initial environment with all imports and definitions loaded.

Parameters:

filestr: Path to the Rocq/Coq file.
optsOpts, optional: Options for proof state management, by default None.

Returns:

State: The root state of the document, including: - st : int - State identifier for the initial state - proof_finished : bool - Always False for root state - feedback : List[Tuple[int, str]] - Initial messages (imports, etc.) - hash : int, optional - State hash

Raises:

PetanqueError: If the file cannot be loaded or processed.
ValueError: If the file path is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     # Get the root state of a file
...     root_state = client.get_root_state("./examples/foo.v")
...     print(f"Root state: {root_state.st}")
...     print(f"Proof finished: {root_state.proof_finished}")  # Always False
...
...     # Check what's available in the initial environment
...     premises = client.premises(root_state)
...     print(f"Available in root context: {len(premises)} premises")
...
...     # Compare with state at specific position
...     pos_state = client.get_state_at_pos("./examples/foo.v", line=3, character=0)
...     print(f"Root state: {root_state.st}, Position state: {pos_state.st}")
...
...     # Check initial feedback
...     for level, msg in root_state.feedback:
...         print(f"Initial feedback level {level}: {msg}")

get_state_at_pos(file, line, character, opts=None)[source]¶

Get the proof state at a specific position in a file.

This method returns the proof state that would be active at the specified position, allowing you to inspect the context, goals, and available tactics at any point in a proof script.

Parameters:

filestr: Path to the Rocq/Coq file.
lineint: Line number (0-based indexing).
characterint: Character position within the line (0-based indexing).
optsOpts, optional: Options for proof state management, by default None.

Returns:

State: The proof state at the specified position, including: - st : int - State identifier - proof_finished : bool - Whether proof is complete at this point - feedback : List[Tuple[int, str]] - Messages from Rocq up to this point - hash : int, optional - State hash

Raises:

PetanqueError: If the position is invalid or the file cannot be processed.
ValueError: If the file path is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     # Get state at beginning of proof
...     state = client.get_state_at_pos("./examples/foo.v", line=2, character=0)
...     print(f"State at start: {state.st}, finished: {state.proof_finished}")
...
...     # Get state in middle of proof
...     state = client.get_state_at_pos("./examples/foo.v", line=5, character=10)
...     goals = client.goals(state)
...     print(f"Goals at position: {len(goals)}")
...
...     # Get state at end of proof
...     state = client.get_state_at_pos("./examples/foo.v", line=8, character=5)
...     print(f"Proof finished: {state.proof_finished}")
...
...     # Check feedback at specific position
...     for level, msg in state.feedback:
...         print(f"Feedback level {level}: {msg}")

goals(state, pretty=True)[source]¶

Retrieve the current goals for a proof state.

Parameters:

stateState: The proof state to query.
prettybool, optional: Whether to add pretty-printed representation to goals, by default True.

Returns:

list[Goal]: List of current goals. Each Goal contains: - info : Any - Goal metadata - hyps : list[GoalHyp] - List of hypotheses - ty : str - Goal type - pp : str, optional - Pretty-printed representation (if pretty=True)

Raises:

PetanqueError: If state is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...     goals = client.goals(state)
...     print(f"Number of goals: {len(goals)}")
...     for i, goal in enumerate(goals):
...         print(f"Goal {i}: {goal.pp}")

premises(state)[source]¶

Get the list of accessible premises (lemmas, definitions) for the current state.

Parameters:

stateState: The proof state to query.

Returns:

Any: List of accessible premises/lemmas for the current proof state.

Raises:

PetanqueError: If state is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...     premises = client.premises(state)
...     print(f"Available premises: {len(premises)}")

query(params, size=4096)[source]¶

Send a low-level JSON-RPC query to the server.

This is an internal method used by other high-level methods. Users should typically use the specific methods like start(), run_tac(), etc.

Parameters:

paramsParams: JSON-RPC parameters (one of StartParams, RunParams, GoalsParams, etc.).
sizeint, optional: Buffer size for receiving response, by default 4096.

Returns:

Response: JSON-RPC response object containing the result.

Raises:

PetanqueError: If the query fails or the server returns an error.
ValueError: If the response format is invalid.

Examples

>>> from pytanque.protocol import StartParams
>>> client = Pytanque("127.0.0.1", 8765)
>>> client.connect()
>>> params = StartParams("file:///path/to/file.v", "theorem_name")
>>> response = client.query(params)
>>> client.close()

run(state, cmd, opts=None, verbose=False, timeout=None)[source]¶

Execute a command on the current proof state.

This method replaces run_tac and supports both tactics and other Rocq commands like Search, Print, Check, etc. The returned state includes feedback containing all messages from Rocq (errors, warnings, search results, etc.).

Parameters:

stateState: The current proof state.
cmdstr: The command to execute. Can be: - Tactics: “induction n.”, “auto.”, “lia.” - Search commands: “Search nat.”, “SearchPattern (_ + _).” - Print commands: “Print list.”, “Print Assumptions.” - Check commands: “Check (fun x => x).”
optsOpts, optional: Options for proof state management, by default None.
verbosebool, optional: Whether to print goals after command execution, by default False.
timeoutint, optional: Timeout in seconds for command execution, by default None.

Returns:

State: The new proof state after command execution. The state.feedback field contains a list of (level, message) tuples with all messages from Rocq including errors, warnings, and command outputs.

Raises:

PetanqueError: If command execution fails.
TimeoutError: If command execution exceeds timeout.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...
...     # Execute tactic
...     state = client.run(state, "induction n.", verbose=True)
...
...     # Execute search command and check feedback
...     state = client.run(state, "Search nat.")
...     for level, msg in state.feedback:
...         print(f"Level {level}: {msg}")
...
...     # Execute print command
...     state = client.run(state, "Print list.")
...     print("Print output in feedback:", state.feedback)
...
...     # Execute check command
...     state = client.run(state, "Check (1 + 1).")
...
...     # Execute with timeout
...     state = client.run(state, "auto.", timeout=5)

set_workspace(debug, dir)[source]¶

Set the root directory for the Coq/Rocq workspace.

Parameters:

debugbool: Enable debug mode for the workspace.
dirstr: Path to the workspace root directory.

Raises:

PetanqueError: If directory is invalid or inaccessible.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     client.set_workspace(debug=False, dir="./examples/")

start(file, thm, pre_commands=None, opts=None)[source]¶

Start a proof session for a specific theorem in a Coq/Rocq file.

Parameters:

filestr: Path to the Coq/Rocq file containing the theorem.
thmstr: Name of the theorem to prove.
pre_commandsstr, optional: Commands to execute before starting the proof, by default None.
optsOpts, optional: Options for proof state management (memo and hash settings), by default None.

Returns:

State: The initial proof state containing: - st : int - State identifier - proof_finished : bool - Whether the proof is complete - hash : int, optional - Hash of the state

Raises:

PetanqueError: If theorem is not found or file cannot be loaded.
ValueError: If file path is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...     print(f"Initial state: {state.st}, finished: {state.proof_finished}")

state_equal(st1, st2, kind)[source]¶

Compare two proof states for equality.

Parameters:

st1State: First state to compare.
st2State: Second state to compare.
kindInspect: Type of comparison (InspectPhysical or InspectGoals).

Returns:

bool: True if states are equal according to the specified comparison type.

Raises:

PetanqueError: If states are invalid.

Examples

>>> from pytanque import Pytanque, InspectPhysical, InspectGoals
>>> with Pytanque("127.0.0.1", 8765) as client:
...     state1 = client.start("./examples/foo.v", "addnC")
...     state2 = client.run(state1, "induction n.")
...     # Compare physical state
...     physical_equal = client.state_equal(state1, state2, InspectPhysical)
...     # Compare goal structure
...     goals_equal = client.state_equal(state1, state2, InspectGoals)

state_hash(state)[source]¶

Get a hash value for a proof state.

Parameters:

stateState: The state to hash.

Returns:

int: Hash value of the state.

Raises:

PetanqueError: If state is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     state = client.start("./examples/foo.v", "addnC")
...     hash_value = client.state_hash(state)
...     print(f"State hash: {hash_value}")

toc(file)[source]¶

Get the table of contents (available definitions and theorems) for a Coq/Rocq file.

Parameters:

filestr: Path to the Coq/Rocq file.

Returns:

list[tuple[str, Any]]: list of (name, definition) pairs representing available definitions and theorems.

Raises:

PetanqueError: If file cannot be loaded.
ValueError: If file path is invalid.

Examples

>>> with Pytanque("127.0.0.1", 8765) as client:
...     toc = client.toc("./examples/foo.v")
...     print("Available definitions:")
...     for name, definition in toc:
...         print(f"  {name}")