pycoq
pycoq copied to clipboard
Python bindings for the Coq interactive proof assistant
``` fruit@DESKTOP-C6T8103 ~/pycoq $ make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py dune build @pip-install Error: No rule found for pycoq/pycoq.so -> required by alias pip-install...
the command: ``` make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py ``` is running some test files. Why do we need to run a test file...
I noticed that: ``` make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py ``` runs code and builds/compiles code through `make install`. If any code is needed...
installation
sorry, still trying to install pycoq. did install coq 8.14.1 can you please help me with those problems? 1. ``` asam@ubunt2:~/Desktop/LMF/pycoq$ make install dune build @pip-install File "coq-serapi/vendor/ppx_python/src/ppx_python_conv.ml", line 207,...
We should provide a method for users to install the PyCoq package seamlessly. It is not clear to me how the install flow should go, as I'm 100% unfamiliar with...
i.e. this step is confusing: > If that's your first checkout, you'll also have to update the git submodules, usually using git submodule update --init --recursive. it shouldn't be needed...
``` (iit_synthesis) brandomiranda~/pycoq-ejgallego ❯ make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py dune build @pip-install File "pycoq/dune", line 5, characters 12-21: 5 | (libraries pythonlib coq-serapi.serapi_v8_14...
This is not pythonic and should be resolved: ``` make install && dune exec -- python3 ``` not is this: ``` import os os.chdir('_build/default') import pycoq, coq ```
As of now, `make` does a full `python3 setup.py build && pip3 install .` ; would be nice if we had a faster workflow, but I have no idea how...