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
🔗 Links