Pytanque

Pytanque is a Python API for lightweight communication with the Rocq proof assistant via coq-lsp.

Overview

• Pytanque is a lightweight Python client for Petanque
• Petanque is part of coq-lsp and provides a machine-to-machine protocol based on JSON-RPC to communicate with the Rocq prover.
• pet-server is the command that starts a Petanque server which can interpret requests for the Rocq prover

Key Features

• Interactive theorem proving: Execute tactics and commands step by step
• Comprehensive feedback: Access all Rocq messages (errors, warnings, search results)
• AST parsing: Get abstract syntax trees for commands and file positions
• State management: Navigate proof states and compare them
• Position-based queries: Get states at specific file positions

Installation

Prerequisites

First, install coq-lsp with the required dependencies:

# Install dependencies
opam install lwt logs coq.8.20.0

# Pin the correct version of coq-lsp
opam pin add coq-lsp https://github.com/ejgallego/coq-lsp.git#v8.20

Install Pytanque

We recommend using a virtual environment. With uv:

uv venv
uv pip install -e .
source .venv/bin/activate

Or with standard Python:

python -m venv .venv
source .venv/bin/activate
pip install -e .

Quick Start

1. Start the Petanque Server

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

2. Basic Usage

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 a similar example with:

python examples/foo.py

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

API Overview

Core Methods

• start(file, theorem): Begin a proof session
• run(state, command): Execute tactics or commands
• goals(state): Get current proof goals
• premises(state): Get available premises/lemmas

Advanced Features

• ast(state, text): Parse command to AST
• ast_at_pos(file, line, char): Get AST at file position
• get_state_at_pos(file, line, char): Get proof state at position
• get_root_state(file): Get initial document state
• state_equal(st1, st2, kind): Compare proof states
• state_hash(state): Get state hash
• toc(file): Get table of contents

Working with Feedback

All commands return states with feedback containing Rocq messages:

state = client.run(state, "Search nat.")
for level, message in state.feedback:
    print(f"Level {level}: {message}")

Testing

You can launch all the tests with pytest.

pytest -v .

Documentation

The complete API documentation is available at: https://llm4rocq.github.io/pytanque

Building Documentation Locally

To build the documentation locally:

# Install documentation dependencies
poetry install --with docs

# Build the documentation
cd docs
poetry run sphinx-build -b html . _build/html

# Open the documentation
open _build/html/index.html  # macOS
# or
xdg-open _build/html/index.html  # Linux

Development

Protocol

We use atdpy to automatically generate serializers/deserializers from protocol type definitions. These types definition should match the ocaml code of petanque in coq-lsp.

To add a new method:

1. Add type definitions in protocol.atd
2. Run atdpy protocol.atd to generate protocol.py
3. Update client.py with the new method

Project Structure

pytanque/
├── client.py          # Main Pytanque client class
├── protocol.py        # Auto-generated protocol definitions
├── __init__.py        # Package exports
tests/
├── conftest.py        # Shared test fixtures
├── test_unit.py       # Unit tests for individual methods
├── test_integration.py # Integration and workflow tests
examples/
├── foo.py            # Basic usage example
├── getting_started.ipynb # Jupyter notebook tutorial
└── foo.v             # Example Coq/Rocq file

Troubleshooting

Common Issues

Server Connection Errors

• Ensure pet-server is running: pet-server -p 8765
• Verify port availability

File Path Issues

• Use absolute paths or ensure working directory is correct
• Check file exists and has proper Coq/Rocq syntax

Installation Issues

• Ensure coq-lsp is properly installed
• Install lwt and logs before coq-lsp (required for pet-server)