Skip to content

Commit

Permalink
README
Browse files Browse the repository at this point in the history
  • Loading branch information
@LasseBlaauwbroek
LasseBlaauwbroek committed Oct 23, 2023
1 parent 41409bc commit fa07030
Show file tree
Hide file tree
Showing 4 changed files with 137 additions and 90 deletions.
184 changes: 110 additions & 74 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,88 +1,78 @@
# A Graph -and Text-based machine learning interface for Tactician
# Tactician's API: A graph- and text-based machine learning interface for Coq

![Tactician's web of large-scale formal knowledge](assets/web.jpg)
Tactician's API provides external machine learning agents with the data
collected by [Tactician](https://coq-tactician.github.io) from the [Coq Proof
Assistant](https://coq.inria.fr). It is able to extract large-scale datasets
from a wide variety of Coq packages for the purpose of offline machine learning.
Additionally, it allows agents to interact with Coq. Proving servers can be
connected to Tactician's `synth` tactic and prove theorems for Coq users (see
[below](#interaction-with-synth)). Additionally, servers can do proof
exploration through the `Tactician Explore` command (see
[below](#client-based-proof-exploration)).

The data provided to agents includes definitions, theorems, proof terms and a
machine-readable representation of tactical proofs. The data is provided both in
Coq's standard text-based human-readable format and as a semantic graph. The
semantic graph is a single interconnected object that includes the entire
mathematical universe known to Coq (at a given moment in time). The graph is
designed to represent the semantic meaning of a mathematical object as
faithfully as possible, minimizing the amount of implicit knowledge needed to
interpret the object. For example, when a definition `X` refers to another
definition `Y`, such a dependency is encoded explicitly using an edge in the
graph. No definition lookup table is need. We also shy away from using names or
de Bruijn indices as variables. Instead, variables point directly to their
binders, so that name lookup becomes a trivial operation. Such an encoding
reduces alpha-equivalence between terms to the graph-theoretic notion of
bisimilarity, and allows us to globally deduplicate any alpha-equivalent terms
in the graph.

Communication with agents happens through the [Cap'n
Proto](https://capnproto.org) serialization format and remote procedure calling
(RPC) protocol. It supports a wide variety of programming languages, including
Python, OCaml, C++, Haskell, Rust and more. This serialization was chosen
because it allows us to memory-map (`mmap`) large graph datasets, allowing fast
random-access to graphs that may not fit into main memory. Furthermore, Cap'n
Proto's RPC protocol, based on the [distributed
object-capability](https://en.wikipedia.org/wiki/Distributed_object) model,
allows us to export Coq's proof states to external agents. Agents can inspect
the proof states, and execute tactics on them, allowing exploration of the proof
search space in arbitrary order.

## PyTactician library

This repository includes a Python library that provides a layer of abstraction
over Cap'n Proto to make it easier to implement agents in Python. Check its
[README](pytact/README.md) for more information.

## Prerequisites

This repository has an OCaml component that should be installed through the Opam package manager and a Python
component that should be installed through the Pip package manager. Additionally, some extra dependencies are needed:
- Opam 2.1.x
- Capt'n Proto >= 0.8
- XXHash >= 0.8
- Graphviz
- A reasonable set of development packages like git, bash, gmp, c/c++ compiler toolchains that should be installed
on most systems.

The simplest and most reliable way to install these packages is through Conda. This repository provides a
`environment.yml` file with the required Conda dependencies. To set it up, follow these commands:
```
git clone --recurse-submodules git@github.com:coq-tactician/coq-tactician-api.git # Clone this repo
cd coq-tactician-api
conda env create -f environment.yml
conda activate tactician
export CPATH="$CONDA_PREFIX:$CPATH" # Needed by cmake to find conda headers
```

If you don't want to use Conda, you'll have to install the dependencies listed above through your distributions
package manager. On Ubuntu 22.04 or newer, you can get the required packages as follows (older versions of Ubuntu
have to fall back to the Conda solutions because the bundled software is out of date)
```
sudo apt-get --yes install graphviz capnproto libcapnp-dev pkg-config libev-dev libxxhash-dev
```
## Installation

After installing the prerequisites, you'll need a Python virtualenv and an Opam switch to install the software.
To create the virtualenv, run
```
python3.10 -m venv <desired-location-of-virtualenv>
```
To activate the virtualenv run `source <location-of-virtualenv>/bin/activate`.
**Before attempting installation, ensure that you have all
[prerequisites](#prerequisites) installed!**

For the OCaml side, if you've never run Opam before, initialize it by running `opam init`. Then, create a switch
with the appropriate software repositories:
```
opam switch create tactician --empty --repos=custom-archive=git+https://github.com/LasseBlaauwbroek/custom-archive.git,coq-extra-dev=https://coq.inria.fr/opam/extra-dev,coq-core-dev=https://coq.inria.fr/opam/core-dev,coq-released=https://coq.inria.fr/opam/released,default
```
Make sure to follow any printed instructions regarding `eval $(opam env)` to activate the switch.
To install the OCaml component of this repository, make sure that you have the
appropriate switch activated and run the command `opam install .` from the root
of this repository.

## Installation
To install the Python component of this repository, make sure that you have a virtualenv enabled then run the
command `pip install .` from the root of this repository.

To install the OCaml component of this repository, make sure that you have the appropriate switch activated and
run the command `opam install . --no-depexts --yes` from the root of this repository.

If you want maximum performance, it is recommended that you use an OCaml version with `flambda` enabled. On newer versions of Opam you can achieve this by installing `ocaml-option-flambda`.

## Usage of the Python software
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 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. To learn how to interface Coq and Tactician with this client, see the sections below.
If you want maximum performance, it is recommended that you use an OCaml version
with `flambda` enabled. On newer versions of Opam you can achieve this by
installing `ocaml-option-flambda`.

## Usage of the Coq plugin

### Available Commands

These commands will create a graph of some object, and write it to `graph.pdf` (if `graphviz` is available).
These commands will create a graph of some object, and write it to `graph.pdf`
(if `graphviz` is available).

The following commands are always available:
```
[Shared] Graph [Depth <n>] Ident identifier.
[Shared] Graph [Depth <n>] Term term.
```
The normal commands print a fully transitive graph. Adding `Depth i` limits the traversal to visiting at most `i`
nested definitions.

The normal commands print a fully transitive graph. Adding `Depth i` limits the
traversal to visiting at most `i` nested definitions.

Additionally, in proof mode, these commands are available:
```
Expand All @@ -97,10 +87,13 @@ Options that modify the graphs generated by the commands above are
```

### Interaction with `synth`
In order to connect Tactician's `synth` tactic to a external tactic prediction server like the dummy
`pytact-server` described above, the plugin makes a number of commands and settings available in Coq.
In order to load the plugin, Coq needs to be started appropriately. This can be done by prefixing every invocation
of a command that uses Coq, like `coqc`, `coqide`, a `make` command or an editor like `emacs` with `tactician exec`:
In order to connect Tactician's `synth` tactic to a external tactic prediction
server like the dummy `pytact-server` described above, the plugin makes a number
of commands and settings available in Coq. In order to load the plugin, Coq
needs to be started appropriately. This can be done by prefixing every
invocation of a command that uses Coq, like `coqc`, `coqide`, a `make` command
or an editor like `emacs` with `tactician exec`:

```
tactician exec -- coqc ...
tactician exec -- coqide ...
Expand Down Expand Up @@ -182,6 +175,49 @@ opam install coq-package --keep-build-dir
and you find the `*.bin` in the directory `<switch>/.opam-switch/build`. The recorded
dependency paths are relative to `<switch>/.opam-switch/build`.

## Prerequisites

This repository has an OCaml component that should be installed through the Opam
package manager and a Python component that should be installed through the Pip
package manager. Additionally, some extra dependencies are needed:
- Opam 2.1.x
- Capt'n Proto >= 0.8
- XXHash >= 0.8
- Graphviz
- A reasonable set of development packages like git, bash, gmp, c/c++ compiler
toolchains that should be installed on most systems.

If your operating systems package manager does not provide these packages with the
correct version, the simplest and most reliable way to install these packages is
through Conda. This repository provides a `environment.yml` file with the required
Conda dependencies. To set it up, follow these commands:
```
git clone --recurse-submodules git@github.com:coq-tactician/coq-tactician-api.git # Clone this repo
cd coq-tactician-api
conda env create -f environment.yml
conda activate tactician
export CPATH="$CONDA_PREFIX:$CPATH" # Needed by cmake to find conda headers
```

On Ubuntu 22.04 or newer, you can get the required packages as follows (older versions of Ubuntu
have to fall back to the Conda solutions because the bundled software is out of date)
```
sudo apt-get --yes install graphviz capnproto libcapnp-dev pkg-config libev-dev libxxhash-dev
```

After installing the prerequisites, you'll need a Python virtualenv and an Opam
switch to install the software. To create the virtualenv, run ``` python -m
venv <desired-location-of-virtualenv> ``` To activate the virtualenv run `source
<location-of-virtualenv>/bin/activate`.

For the OCaml side, if you've never run Opam before, initialize it by running `opam init`. Then, create a switch
with the appropriate software repositories:
```
opam switch create tactician --empty --repos=custom-archive=git+https://github.com/LasseBlaauwbroek/custom-archive.git,coq-extra-dev=https://coq.inria.fr/opam/extra-dev,coq-core-dev=https://coq.inria.fr/opam/core-dev,coq-released=https://coq.inria.fr/opam/released,default
```
Make sure to follow any printed instructions regarding `eval $(opam env)` to activate the switch.


## CI
To verify the build and test locally by specification in `Dockerfile` you run

Expand Down
Binary file added assets/web.jpg
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ dependencies = [

[project.urls]
Homepage = "https://coq-tactician@github.io"
# Documentation = "https://readthedocs.org"
Documentation = "https://coq-tactician.github.io/api/pytactician-pdoc"
Repository = "https://github.com/coq-tactician/coq-tactician-api"
Changelog = "https://github.com/coq-tactician/coq-tactician-api/CHANGELOG.md"

Expand Down
41 changes: 26 additions & 15 deletions pytact/README.md
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,40 @@
# 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`.
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 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](https://github.com/coq-tactician/coq-tactician-api#prerequisites)
for more details on prerequisites.
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

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).
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] dataset`:
- `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
Expand All @@ -30,7 +45,3 @@ about all the options).
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.

## Documentation

TODO: Point to documentation

0 comments on commit fa07030

Please sign in to comment.