Python Library for interfacing with Coq and Tactician
Project description
PyTactician
PyTactician is a Python Library for interfacing with the Coq Proof Assistant and its Tactician plugin and
reading associated datasets. The major version number x
of this library indicates the version of the
communication protocol. Any PyTactician version x.y
is compatible with the communication protocol x
.
Installation
Binary wheels are provided for Linux and MacOS. On those platforms you can install by executing
pip install pytactician
. If you need to install from source, you need to have Capt'n Proto >= 0.8 installed
on your system. See the main repo README
for more details on prerequisites.
Usage
The Python software provides both a software library to work with the graph based datasets extracted from Coq and
a number of executables. 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] 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 datasetpytact-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 reinforcement-learning-style communication. To learn how to interface Coq and Tactician with this client, see the sections below.
Documentation
TODO: Point to documentation
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distributions
Hashes for pytactician-15.0-cp311-cp311-musllinux_1_1_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 4cce00d54a06c04b22c3c5ed0501241bdfd8971d35088898bbb5c4cd0c1af26c |
|
MD5 | 71e31c25dd4c58ffa0bb5ac73f1e9706 |
|
BLAKE2b-256 | 9f949c380b24a4f5989e1c249e9c4600dc9e782b14d0576e86a9c807a2c7d961 |
Hashes for pytactician-15.0-cp311-cp311-musllinux_1_1_i686.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 452d6c7cca498a3d26c7c33f1f4048cd1c6bc732a399a0417279d403daa897bc |
|
MD5 | ae1ceb1bdac5b64dcf17892a2bbd2348 |
|
BLAKE2b-256 | 0155b815864fe6bca7cc8315bf4648cab3250e148e775dff268667e9e943ffc6 |
Hashes for pytactician-15.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 62c5b2ea6a357461bf48ae9fa710a75d6f1c6adfee6dcdc03f29018d76f704d5 |
|
MD5 | 2f252f793671bc1f1a86fae79f9f6059 |
|
BLAKE2b-256 | c2ff7dd4548f9610778f067621cbc28057717f655ce0e5756bf0eb59d4ce9ad7 |
Hashes for pytactician-15.0-cp311-cp311-manylinux_2_17_i686.manylinux2014_i686.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 3cca0a15c9e70f7ceb4de7ca5161536e89551186e5cd2b34ee745c52bab29ea2 |
|
MD5 | 15f30f12fcb83e06efdb16c24342a18d |
|
BLAKE2b-256 | 1c5ce7906e34ffbcaed269e21ad391803541879d1f040b5848daff712778df4a |
Hashes for pytactician-15.0-cp311-cp311-macosx_10_9_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 3a7afd3983d1a7847c8e505d3d631380253df880e18339dce1a791b71a1e121f |
|
MD5 | e175e391716bc655bcfa24f6708067b4 |
|
BLAKE2b-256 | 3f2873e3317fb5d453e94a38003b6f0e66eca401475c3ec4c74889ec847f048d |
Hashes for pytactician-15.0-cp310-cp310-musllinux_1_1_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | f1b2ce8f1c5533204bdeba85702db8b6e98fc7675633ffbe30c90d5e9c1275a9 |
|
MD5 | b6cef352849cb409eda90ab7fab636b7 |
|
BLAKE2b-256 | b22f3538ed1513f17a503583186dc4c3c6a155110240831746a9073d3d684329 |
Hashes for pytactician-15.0-cp310-cp310-musllinux_1_1_i686.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 447846dcd733e5d579ecd9c71d968521c96dae38766fd2ab029ea3cd43a04cf6 |
|
MD5 | 744000c1a321acca86361819e362212f |
|
BLAKE2b-256 | d5a5b2783a03e2a123925e50b0ba80c6fe843d644f83dca4f17ca571a0f02095 |
Hashes for pytactician-15.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 3c99dc88b67c9187b95da08a44060e0faf12fadc9870eb661b2e6252415178f6 |
|
MD5 | a426bb661097f6e528c9356f3dc5ff6b |
|
BLAKE2b-256 | cadbd1c95dc92de0239c5bfab255e6e6e66ec4fc5b3a64f95f14d0b6ea9006b8 |
Hashes for pytactician-15.0-cp310-cp310-manylinux_2_17_i686.manylinux2014_i686.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | fd1c3ed5f18bf2635f17778fb617083a21e3974f236f2ee44822ffa39a28ccdc |
|
MD5 | 04f09b37916972d3ec5daefeee8ffc0a |
|
BLAKE2b-256 | 1ba4b537cba026776205db9813cb628be0cd55c896954af5107574095fe7d6b0 |
Hashes for pytactician-15.0-cp310-cp310-macosx_10_9_x86_64.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 6762011068d0de77e9a1eb6efb99f4aed27aabad4c2c7b03f61a7944f8116024 |
|
MD5 | 53e00711d5f5e94573a0fb2c4f4eed9a |
|
BLAKE2b-256 | 80f729ef3f0a8eecf405befc8d92660f8ea50c98d0fa254f50f5fab025f88988 |