ibm / pycoq Goto Github PK

View Code? Open in Web Editor NEW

6.0 7.0 8.0 367 KB

python API to coq-serapi

License: MIT License

Makefile 0.16% Python 59.29% C++ 9.15% Coq 31.01% Dockerfile 0.39%

pycoq's Introduction

The pip distribution package pycoq provides two python packages:

serlib
pycoq

pycoq

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

serlib

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

Install on Linux

Currently we support only the Linux platform.

Build tools

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

External dependencies

opam

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.

strace

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.

Install

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

Test your setup

From your python environment with pycoq installed run

pytest --pyargs pycoq

Config pycoq

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

Uninstall 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

Using pycoq

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

Build pycoq in Docker

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

pycoq's People

Contributors

Stargazers

Watchers

Forkers

brando90 cbmm mirefek pestun yeahrmek pestun-ihes

pycoq's Issues

where is strace_parser supposed to be at?

    from strace_parser.parser import get_parser
ModuleNotFoundError: No module named 'strace_parser'

What is the real purpose of strace in PyCoq?

Why doesn't CoqSerapi object call .start()?

I saw:

        elif isinstance(kernel_or_cfg, pycoq.common.LocalKernelConfig):
            self._kernel = None
            self._cfg = kernel_or_cfg

but it's only called in the aenter but not in the init. Why?

If thats done it's hard to build your own context manager. @pestun

What is the path to remove the dependence on linux only (e.g. strace)?

PyCoq is difficult to run on systems that are not linux. What is an outline of what would be needed to be changed for this to happen?

e.g. I notice the need for strace. Why is this needed and how can one remove this dependence completely e.g. by using only standard python libraries?

How does one close manually the CoqSerapi obj?

I see it has a aexit but that method doesn't have default args. Nor does the obj have a .closing or .quit method. So how does one close this? @pestun

why does PyCoq opam pin a package before doing the strace of an opam reinstall?

I noticed that PyCoq does:

    if ((not coq_proj_path is None) and
            not opam_pin_package(coq_proj, coq_proj_path, coq_serapi, coq_serapi_pin, compiler)):

before it tries to strace the opam reinstall ... coq_pkg of the coq pkg in question. Is the opam pin really necessary before? How can we remove that depedency? Would it work if the package was built with make clean -C ...?

why doesn't the _aexit_ function have a check if self._kernel is None?

when the coq serapi instance is one if its fields can be None:

    def __init__(self, kernel_or_cfg: Union[pycoq.kernel.LocalKernel, pycoq.common.LocalKernelConfig], logfname=None):
        """ 
        wraps coq-serapi interface on the running kernel object
        """
        self._logfname = logfname
        if isinstance(kernel_or_cfg, pycoq.kernel.LocalKernel):
            self._kernel = kernel_or_cfg
            self._cfg = None
        elif isinstance(kernel_or_cfg, pycoq.common.LocalKernelConfig):
            self._kernel = None
            self._cfg = kernel_or_cfg
        else:
            raise TypeError("CoqSerapi class must be initialized either with an existing kernel "
                            "object of type pycoq.kernel.LocalKernel or config object of type "
                            " pycoq.common.LocalKernelConfig "
                            f"but the supplied argument has type {type(kernel_or_cfg)}")

but a exist there is not check that we use the one is not None

    async def __aexit__(self, exception_type, exception_value, traceback):
        await self._kernel.__aexit__(exception_type, exception_value, traceback)
        async for line in self._kernel.readlines():
            self._serapi_response_history.append(line)
...

why?

also what resources is it trying to let go? @pestun