Brando Miranda (Feb 24 2023 at 17:29): Brando Miranda (Feb 24 2023 at 17:29):hi! I was trying to install @Emilio Jesús Gallego Arias new promosing Python bindings for Coq. But I can't have the installation work. Has anyone been successful in instlaling and using the python serapi bindings emilio made? I've documented my current attempts here https://github.com/ejgallego/pycoq/issues/24 but thought asking someone who has actually made it work would be better.
Andrew Samokish (Feb 27 2023 at 10:17):yes, i did manage to run the example provided. the key problem was to install correct version of Coq. if I remember well : 8.15. I can check something if would help you
Brando Miranda (Feb 27 2023 at 17:35):hi @Andrew Samokish would love some help!
Installing Coq isn't a problem for me. Last command I did was
$ opam install --deps-only coq-serapi
$ opam install pythonlib
after that it's not clear what I'm supposed to do based on this: https://github.com/ejgallego/pyCoq what is the next command you ran? (if you have the series of commands you did that would be fantastic!)
Emilio Jesús Gallego Arias (Feb 27 2023 at 17:39):@Brando Miranda I have trouble understanding your problems, indeed the instructions are a bit out of date, the key point is that
opam install --deps-only .
suceeds
Emilio Jesús Gallego Arias (Feb 27 2023 at 17:40):The right set of packages is kept a pycoq.opam
Emilio Jesús Gallego Arias (Feb 27 2023 at 17:40):Once you have that, then the regular make instructions would work
Emilio Jesús Gallego Arias (Feb 27 2023 at 17:43):The current version is a bit sensitive on package issues due to OCaml at the time undergoing an API migration
Brando Miranda (Feb 28 2023 at 17:28):Emilio Jesús Gallego Arias said:
Brando Miranda I have trouble understanding your problems, indeed the instructions are a bit out of date, the key point is that
opam install --deps-only .suceeds
two problems.
1st: It's clear what needs to be run up until
$ opam install --deps-only coq-serapi
$ opam install pythonlib
after that there is this paragraph:
for the 0.13 version that targets Coq v8.13; note that OCaml >= 4.11.0 is recommended, and >= 4.08.0 required by the dependencies.
If that's your first checkout, you'll also have to update the git submodules, usually using
git submodule update --init --recursive.For the moment, PyCoq requires a special version of
ppx_python, while the situation stabilizes in the OPAM repository we have vendored it in the SerAPI branch we use.
which mentions git submodule update --init --recursive and ppx_python. Does this mean that not only I need to do the opam command opam install --deps-only coq-serapi && opam install pythonlib but also clone the repo or some commands that were not documented? In addition the mention of ppx_python is confusing -- especially given there is no pip install ppx_python command accompanying it.
2nd: Then this is confusion is exacerbated by the fact make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py doesn't work. It makes it seem there is a bunch of commands I missed in between.
The error msg is:
(pycoq-ejgallego) brandomiranda~/pycoq-ejgallego ❯ make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py
dune build @pip-install
File "coq-serapi/serapi/serapi_assumptions.mli", line 22, characters 18-48:
22 | { predicative : Declarations.set_predicativity
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound type constructor Declarations.set_predicativity
File "coq-serapi/serapi/serapi_goals.ml", line 57, characters 9-18:
57 | (g : Goal.goal) =
^^^^^^^^^
Error (alert deprecated): Goal.goal
File "coq-serapi/serapi/serapi_goals.ml", line 58, characters 66-80:
58 | ppx @@ EConstr.to_constr ~abort_on_undefined_evars:false sigma (Goal.V82.concl sigma g)
^^^^^^^^^^^^^^
Error: Unbound module Goal.V82
File "coq-serapi/serapi/serapi_doc.ml", line 43, characters 2-25:
43 | Library.save_library_to todo_proofs ~output_native_objects:false ldir out_vo (Global.opaque_tables ())
^^^^^^^^^^^^^^^^^^^^^^^
Error: This function has type
'a Library.todo_proofs ->
output_native_objects:bool -> Names.DirPath.t -> string -> unit
It is applied to too many arguments; maybe you forgot a `;'.
File "coq-serapi/vendor/ppx_python/src/ppx_python_conv.ml", line 207, characters 35-79:
207 | ~lhs:(ppat_constant ~loc (Pconst_string (variant.pcd_name.txt, None)))
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The constructor Pconst_string expects 3 argument(s),
but is applied here to 2 argument(s)
make: *** [install] Error 1
seems like your coq version is more recent than your serapi version
Brando Miranda (Mar 02 2023 at 15:41):that's confusing. Why would opam allow to install me deps that don't match?
Brando Miranda (Mar 02 2023 at 15:41):@Emilio Jesús Gallego Arias is there a way to "pip freeze" the deps of pycoq so the install works? Or have lower bounds on all versions of the dependencies (deps) so we can try to help?
Emilio Jesús Gallego Arias (Mar 03 2023 at 18:57):Brando thanks for all the feedback, note that pycoq doesn't use pip, but opam. I'll try to cleanup the install procedure a bit next week, this week I don't really have the cycles :(
Last updated: Oct 13 2024 at 01:02 UTC