Quick Start

Pytanque supports two communication modes with the Petanque backend:

Socket Mode (via pet-server)

1. Start the Petanque Server

$ pet-server  # Default port: 8765
# Or specify a custom port:
$ pet-server -p 9000

2. Connect via Socket

from pytanque import Pytanque

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

    # Execute tactics step by step
    state = client.run(state, "induction n.", verbose=True)
    state = client.run(state, "auto.", verbose=True)

    # Check current goals
    goals = client.goals(state)
    print(f"Current goals: {len(goals)}")

You can quickly try this example with:

# Socket mode example
python examples/foo.py

See also the notebook examples/getting_started.ipynb for more examples.

Stdio Mode (via pet)

For direct communication without a server, use subprocess mode:

from pytanque import Pytanque

with Pytanque(stdio=True) as client:
    # Same API as socket mode
    state = client.start("./examples/foo.v", "addnC")
    print(f"Initial state: {state.st}, finished: {state.proof_finished}")

    # Execute tactics step by step
    state = client.run(state, "induction n.", verbose=True)
    state = client.run(state, "auto.", verbose=True)

    # Check current goals
    goals = client.goals(state)
    print(f"Current goals: {len(goals)}")