Pytanque

Documentation Build Status Tests Python 3.10+ License

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/pet are the commands that start a Petanque server which can interpret requests for the Rocq prover

Key Features

  • Two communication modes: Socket mode (via pet-server) for multi-client usage or stdio mode (via pet) for single-client simplicity

  • Interactive theorem proving: Execute tactics and commands step by step

  • Comprehensive feedback: Access all Rocq messages (errors, warnings, search results)

  • State management: Navigate proof states and compare them

  • AST parsing: Get abstract syntax trees for commands and file positions (only with the dev version of coq-lsp)

  • Position-based queries: Get states at specific file positions (only with the dev version of coq-lsp)

🔗 Links

Index