Metadata-Version: 2.1
Name: pytactician
Version: 15.1
Summary: Python Library for interfacing with Coq and Tactician
Author-email: Lasse Blaauwbroek <lasse@blaauwbroek.eu>, Vasily Pestun <vasily.pestun@gmail.com>, Miroslav Olšák <mirek@olsak.net>
License: MIT
Project-URL: Homepage, https://coq-tactician.github.io
Project-URL: Documentation, https://coq-tactician.github.io/api/pytactician-pdoc
Project-URL: Repository, https://github.com/coq-tactician/coq-tactician-api
Project-URL: Changelog, https://github.com/coq-tactician/coq-tactician-api/blob/coq8.11/CHANGELOG.md
Classifier: Development Status :: 5 - Production/Stable
Classifier: Intended Audience :: Science/Research
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: C
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Operating System :: POSIX :: Linux
Classifier: Operating System :: MacOS
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Requires-Python: >=3.8
Description-Content-Type: text/markdown
License-File: LICENSE.md
Requires-Dist: pycapnp<2,>=1.2.2
Requires-Dist: immutables
Requires-Dist: graphviz
Requires-Dist: sanic==23.6.0
Requires-Dist: sanic-ext==23.6.0
Requires-Dist: Jinja2
Requires-Dist: inflection

# PyTactician

PyTactician is a Python Library for interfacing with the [Coq Proof
Assistant](https://coq.inria.fr) through the
[API](https://coq-tactician.github.io/api) of its
[Tactician](https://coq-tactician.github.io) 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](https://pypi.org/project/pytactician)). 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](https://github.com/coq-tactician/coq-tactician-api#prerequisites) 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](https://coq-tactician.github.io/api/pytactician-pdoc).

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.
