PyTactician

PyTactician is a Python Library for interfacing with the Coq Proof Assistant through the API of its Tactician plugin and reading associated datasets.

The major version number x of this library indicates the version of the dataset and communication protocol. Any PyTactician version x.y is compatible with the communication protocol x.

Installation

Binary wheels are provided for Linux and MacOS (on PyPI). On those platforms you can install by executing pip install pytactician. If you need to install from source, you need to have Cap'n Proto >= 0.8 installed on your system. See the main repo README for more details on prerequisites. Once you have the prerequisites, you can install by running pip install . from the root of the repository.

Usage

PyTactician provides a library to work with the datasets extracted from Coq and to directly interface with Coq through Tacticians API. The documentation for the library can be found here.

In addition, PyTactician contains a number of executables that can be used to analyze datasets and interact with Coq. Available executables are as follows (use the --help flag for each executable to learn about all the options).

• pytact-check [-h] [--jobs JOBS] [--quick] [--verbose VERBOSE] dir Run sanity checks on a dataset and print some statistics.
• pytact-visualize [-h] [--port PORT] [--hostname HOSTNAME] [--dev] [--fast | --workers WORKERS] dataset: Start an interactive server that visualizes a dataset.
• pytact-server [-h] [--tcp TCP] [--record RECORD_FILE] {graph,text} Example python server capable of communicating with Coq through Tactician's 'synth' tactic To learn how to interface Coq and Tactician with this server, see the sections below.
• pytact-oracle [-h] [--tcp PORT] [--record RECORD_FILE] {graph,text} dataset A tactic prediction server acting as an oracle, retrieving it's information from a dataset
• pytact-fake-coq [-h] (--tcp TCP_LOCATION | --stdin EXECUTABLE) data A fake Coq client that connects to a prediction server and feeds it a stream of previously recorded messages.
• pytact-prover: A dummy example client that interfaces with Coq and Tactician for proof exploration driven by the client.