search

ejgallego / pycoq

Python bindings for the Coq interactive proof assistant
50 stars 4 forks source link

ppx_base not found during installation #25

Open brando90 opened 1 year ago

brando90 commented 1 year ago 
(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 coq-serapi.sertop_v8_12))
                ^^^^^^^^^
Error: Library "pythonlib" not found.
-> required by _build/default/pycoq/pycoq.so
-> required by alias pip-install in dune:15
File "coq-serapi/sertop/dune", line 12, characters 36-49:
12 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                                         ^^^^^^^^^^^^^
Error: Library "ppx_sexp_conv" not found.
-> required by _build/default/coq-serapi/sertop/sercomp.exe
-> required by _build/install/default/bin/sercomp
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/sertop/dune", line 12, characters 25-35:
12 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                              ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/sertop/.merlin-conf/exe-sertop_bin-cea70dd0b7eed1178ac7bb4aff6fbd91
-> required by _build/default/coq-serapi/sertop/sercomp.exe
-> required by _build/install/default/bin/sercomp
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/vendor/ppx_python/runtime/dune", line 4, characters 17-21:
4 |  (libraries base pyml)
                     ^^^^
Error: Library "pyml" not found.
-> required by library "coq-serapi.ppx_python_runtime_pycoq" in
   _build/default/coq-serapi/vendor/ppx_python/runtime
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serapi/dune", line 5, characters 47-54:
5 |  (libraries coq-core.stm coq-core.plugins.ltac sexplib))
                                                   ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serapi_v8_14" in
   _build/default/coq-serapi/serapi
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/dune", line 6, characters 25-32:
6 |  (libraries coq-core.stm sexplib))
                             ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib" in
   _build/default/coq-serapi/serlib
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/extraction/dune", line 5, characters 36-49:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                                        ^^^^^^^^^^^^^
Error: Library "ppx_sexp_conv" not found.
-> required by library "coq-serapi.serlib.extraction_plugin" in
   _build/default/coq-serapi/serlib/plugins/extraction
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/firstorder/dune", line 6, characters 47-54:
6 |  (libraries coq-core.plugins.firstorder serlib sexplib))
                                                   ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.firstorder_plugin" in
   _build/default/coq-serapi/serlib/plugins/firstorder
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/funind/dune", line 6, characters 55-62:
6 |  (libraries coq-core.plugins.funind serlib serlib_ltac sexplib))
                                                           ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.funind_plugin" in
   _build/default/coq-serapi/serlib/plugins/funind
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ltac/dune", line 6, characters 41-48:
6 |  (libraries coq-core.plugins.ltac serlib sexplib))
                                             ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.ltac" in
   _build/default/coq-serapi/serlib/plugins/ltac
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ring/dune", line 6, characters 53-60:
6 |  (libraries coq-core.plugins.ring serlib serlib_ltac sexplib))
                                                         ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.ring_plugin" in
   _build/default/coq-serapi/serlib/plugins/ring
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ssr/dune", line 6, characters 77-84:
6 |  (libraries coq-core.plugins.ssreflect serlib serlib_ltac serlib_ssrmatching sexplib))
                                                                                 ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.ssreflect_plugin" in
   _build/default/coq-serapi/serlib/plugins/ssr
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ssrmatching/dune", line 6, characters 60-67:
6 |  (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
                                                                ^^^^^^^
Error: Library "sexplib" not found.
-> required by library "coq-serapi.serlib.ssrmatching_plugin" in
   _build/default/coq-serapi/serlib/plugins/ssrmatching
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/sertop/dune", line 6, characters 28-36:
6 |  (libraries findlib.dynload cmdliner serapi serlib serlib_ltac))
                                ^^^^^^^^
Error: Library "cmdliner" not found.
-> required by library "coq-serapi.sertop_v8_12" in
   _build/default/coq-serapi/sertop
-> required by _build/default/coq-serapi/META.coq-serapi
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/sertop/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python_conv_pycoq))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/sertop/.merlin-conf/lib-coq-serapi.sertop_v8_12
-> required by _build/default/coq-serapi/sertop/sertop.a
-> required by _build/install/default/lib/coq-serapi/sertop_v8_12/sertop.a
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson ppx_python_conv_pycoq))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/.serlib.objs/byte/serlib__Ppx_python_runtime_serapi.cmo
-> required by _build/default/coq-serapi/serlib/serlib.cma
-> required by _build/install/default/lib/coq-serapi/serlib/serlib.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/extraction/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/extraction/.serlib_extraction.objs/byte/serlib_extraction__Ser_g_extraction.cmo
-> required by
   _build/default/coq-serapi/serlib/plugins/extraction/serlib_extraction.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/extraction_plugin/serlib_extraction.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/firstorder/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/firstorder/.serlib_firstorder.objs/byte/serlib_firstorder__Ser_g_ground.cmo
-> required by
   _build/default/coq-serapi/serlib/plugins/firstorder/serlib_firstorder.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/firstorder_plugin/serlib_firstorder.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/funind/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/funind/.serlib_funind.objs/byte/serlib_funind__Ser_g_indfun.cmo
-> required by
   _build/default/coq-serapi/serlib/plugins/funind/serlib_funind.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/funind_plugin/serlib_funind.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ltac/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_python_conv_pycoq))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/ltac/.serlib_ltac.objs/byte/serlib_ltac__Ser_profile_ltac.cmo
-> required by _build/default/coq-serapi/serlib/plugins/ltac/serlib_ltac.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/ltac/serlib_ltac.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ring/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/ring/.serlib_ring.objs/byte/serlib_ring__Ser_g_ring.cmo
-> required by _build/default/coq-serapi/serlib/plugins/ring/serlib_ring.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/ring_plugin/serlib_ring.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ssr/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/ssr/.serlib_ssr.objs/byte/serlib_ssr__Ser_ssrast.cmo
-> required by _build/default/coq-serapi/serlib/plugins/ssr/serlib_ssr.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/ssreflect_plugin/serlib_ssr.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/plugins/ssrmatching/dune", line 5, characters 25-35:
5 |  (preprocess (staged_pps ppx_import ppx_sexp_conv))
                             ^^^^^^^^^^
Error: Library "ppx_import" not found.
-> required by
   _build/default/coq-serapi/serlib/plugins/ssrmatching/.serlib_ssrmatching.objs/byte/serlib_ssrmatching__Ser_ssrmatching.cmo
-> required by
   _build/default/coq-serapi/serlib/plugins/ssrmatching/serlib_ssrmatching.cma
-> required by
   _build/install/default/lib/coq-serapi/serlib/ssrmatching_plugin/serlib_ssrmatching.cma
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/vendor/ppx_python/runtime/dune", line 5, characters 18-26:
5 |  (preprocess (pps ppx_base)))
                      ^^^^^^^^
Error: Library "ppx_base" not found.
-> required by
   _build/default/coq-serapi/vendor/ppx_python/runtime/.merlin-conf/lib-coq-serapi.ppx_python_runtime_pycoq
-> required by
   _build/default/coq-serapi/vendor/ppx_python/runtime/ppx_python_runtime_pycoq.a
-> required by
   _build/install/default/lib/coq-serapi/ppx_python_runtime_pycoq/ppx_python_runtime_pycoq.a
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
make: *** [install] Error 1
brando90 commented 1 year ago

my install commands

# --- To be safe lets create a switch only for pycoq-emilio
# -- 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.
opam switch create pycoq-ejgallego 4.12.0
eval $(opam env --switch=pycoq-ejgallego --set-switch)
opam pin add -y coq 8.16.0
# Install the packages that can be installed directly through opam
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

# --- To build PyCoq, you need Python 3 and an OCaml environment able to build SerAPI; usually, this can be achieved using the OPAM package manager and doing:
#opam install --deps-only coq-serapi
opam install -y coq-serapi
opam install -y pythonlib

# --- Create conda env
conda create -n iit_synthesis python=3.9
conda activate iit_synthesis
#pip install -e ~/ultimate-utils

# - Clone pycoq-emilio repo cuz he says so (this shouldn't be something a python user needs to do)
cd ~
git clone git@github.com:brando90/pycoq-ejgallego.git
cd ~/pycoq-ejgallego
# pip install -e .
git submodule update --init --recursive
make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py

# --- If you want an interactive environment, use:
make install && dune exec -- python
ejgallego commented 1 year ago

@brando90 these instructions seem weird, you want indeed to install what it is in the pycoq.opam file. You can do that with 

opam install --deps-only .