ejgallego / pycoq

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

Can't install this #30

Open enjoysmath opened 1 year ago

enjoysmath commented 1 year ago
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 in dune:15
File "coq-serapi/serapi/dune", line 5, characters 25-46:
5 |  (libraries coq-core.stm coq-core.plugins.ltac sexplib))
                             ^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ltac" not found.
-> required by library "coq-serapi.serapi_v8_14" in
   _build/default/coq-serapi/serapi
-> required by executables sertop_bin, sercomp, sertok and sername in
   coq-serapi/sertop/dune:10
-> required by _build/default/coq-serapi/sertop/sercomp.exe
-> required by _build/install/default/bin/sercomp.exe
-> required by alias coq-serapi/.coq-serapi-files
-> required by alias pip-install in dune:15
File "coq-serapi/serlib/dune", line 6, characters 12-24:
6 |  (libraries coq-core.stm sexplib))
                ^^^^^^^^^^^^
Error: Library "coq-core.stm" 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 6, characters 12-39:
6 |  (libraries coq-core.plugins.extraction serlib))
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.extraction" 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 12-39:
6 |  (libraries coq-core.plugins.firstorder serlib sexplib))
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.firstorder" 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 12-35:
6 |  (libraries coq-core.plugins.funind serlib serlib_ltac sexplib))
                ^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.funind" 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 12-33:
6 |  (libraries coq-core.plugins.ltac serlib sexplib))
                ^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ltac" 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 12-33:
6 |  (libraries coq-core.plugins.ring serlib serlib_ltac sexplib))
                ^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ring" 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 12-38:
6 |  (libraries coq-core.plugins.ssreflect serlib serlib_ltac serlib_ssrmatching sexplib))
                ^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ssreflect" 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 12-40:
6 |  (libraries coq-core.plugins.ssrmatching serlib serlib_ltac sexplib))
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Library "coq-core.plugins.ssrmatching" 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/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: *** [Makefile:14: install] Error 1

fruit@DESKTOP-C6T8103 ~/pycoq

Windows 10, 64-bit, v21H2

Please help me install the dependencies properly - i thought i did everything.

enjoysmath commented 1 year ago

So I ran the vcvarsall.bat for my VS 2022 instance from within Cygwin successfully. But I can't seem to run make command even though the dune directory is there: image

enjoysmath commented 1 year ago

So I did everything again, this time install OCaml from Cygwin checkbox, this is the result:

image

How can we succesfully build this? Thx