The pip distribution package pycoq provides two python packages:

• serlib

• pycoq

pycoq is a python library that provides interface to Coq using the serialization coq-serapi https://github.com/ejgallego/coq-serapi

serlib is a python library providing s-expression parser implemented in C++

Currently we support only the Linux platform.

We assume a standard set of building tools. For Ubuntu 20.04 you can get them with

apt-get update && apt-get install -y --no-install-recommends ssh git m4 libgmp-dev opam wget ca-certificates rsync strace

The pycoq calls opam package manager to install and run the coq-serapi and coq binaries. The pycoq assumes that opam binary of version 2.* is in the $PATH.

On Ubuntu 20.04 install opam with sudo apt-get install opam. See https://opam.ocaml.org/doc/Install.html for other systems.

The pycoq calls strace to inspect the building of coq-projects to prepare the context. The pycoq assumes
that strace is in the $PATH.

On Ubuntu 20.04 install strace with sudo apt-get install strace. See https://github.com/strace/strace for other systems.

Assuming python>=3.8 and pip are in your environment, to install from https://pypi.org/project/pycoq/ run

pip install pycoq

to install from the github source repository run

pip install git+https://github.com/IBM/pycoq

From your python environment with pycoq installed run

pytest --pyargs pycoq

The location of the project directory, debug level and other parameters can be specified in the config file $HOME/.pycoq

From your python environment with pycoq installed run

pip uninstall pycoq

By default, pycoq uses directory $HOME/.local/share/pycoq to store temporary files such as the opam repository, project files and the logs. To remove the project directory:

rm -fr $HOME/.local/share/pycoq

To remove the config file:

rm $HOME/.pycoq

For basics see the example tutorial/tutorial_pycoq.py and the test scripts in pycoq/test.

Install docker, git clone the source repository and from the directory containing Dockerfile run

docker build -t pycoq:test .

to verify the setup and test of pycoq in docker container on linux