ejgallego
commented
1 year ago What does opam list show?
Open ASamSam opened 1 year ago
ejgallego
commented
1 year ago What does opam list show?
ejgallego
commented
1 year ago This is a problem with the versions of the packages you have, you won't be able to fix the code manually unfortunately, code is very different among Coq versions.
ASamSam
commented
1 year ago here is opam list result. what is the correct coq version for me? i can reinstall everything, but did understood that coq 8.14 is ok
opam list
Packages matching: installed
Name Installed Synopsis
base v0.15.1 Full standard library replacement for OCaml
base-bigarray base
base-threads base
base-unix base
cairo2 0.6.4 Binding to Cairo, a 2D Vector Graphics Library
camlp-streams 5.0.1 The Stream and Genlex libraries for use with Camlp4 and Camlp5
cmdliner 1.1.1 Declarative definition of command line interfaces for OCaml
conf-adwaita-icon-theme 2 Virtual package relying on adwaita-icon-theme
conf-cairo 1 Virtual package relying on a Cairo system installation
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
conf-gtk3 18 Virtual package relying on GTK+ 3
conf-gtksourceview3 0+2 Virtual package relying on a GtkSourceView-3 system installation
conf-pkg-config 2 Check if pkg-config is installed and create an opam switch local pkgconfig folder
coq 8.14.1 pinned to version 8.14.1
coqide 8.14.1 IDE of the Coq formal proof management system
cppo 1.6.9 Code preprocessor like cpp for OCaml
csexp 1.5.1 Parsing and printing of S-expressions in Canonical form
dune 3.6.2 Fast, portable, and opinionated build system
dune-configurator 3.6.2 Helper library for gathering system configuration
jane-street-headers v0.15.0 Jane Street C header files
jst-config v0.15.1 Compile-time configuration for Jane Street libraries
lablgtk3 3.1.3 OCaml interface to GTK+3
lablgtk3-sourceview3 3.1.3 OCaml interface to GTK+ gtksourceview library
num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml 4.13.1 The OCaml compiler (virtual package)
ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged
ocaml-config 2 OCaml Switch Configuration
ocaml-system 4.13.1 The OCaml compiler (system version, from outside of opam)
ocamlfind 1.9.5 A library manager for OCaml
parsexp v0.15.0 S-expression parsing library
ppx_assert v0.15.0 Assert-like extension nodes that raise useful errors on failure
ppx_base v0.15.0 Base set of ppx rewriters
ppx_cold v0.15.0 Expands [@cold] into [@inline never][@specialise never][@local never]
ppx_compare v0.15.0 Generation of comparison functions from types
ppx_derivers 1.2.1 Shared [@@deriving] plugin registry
ppx_deriving 5.2.1 Type-driven code generation for OCaml
ppx_deriving_yojson 3.7.0 JSON codec generator for OCaml
ppx_enumerate v0.15.0 Generate a list containing all values of a finite type
ppx_expect v0.15.1 Cram like framework for OCaml
ppx_hash v0.15.0 A ppx rewriter that generates hash functions from type expressions and definitions
ppx_here v0.15.0 Expands [%here] into its location
ppx_import 1.10.0 A syntax extension for importing declarations from interface files
ppx_inline_test v0.15.0 Syntax extension for writing in-line tests in ocaml code
ppx_let v0.15.0 Monadic let-bindings
ppx_optcomp v0.15.0 Optional compilation for OCaml
ppx_python v0.15.0 [@@deriving] plugin to generate Python conversion functions
ppx_sexp_conv v0.15.1 [@@deriving] plugin to generate S-expression conversion functions
ppxlib 0.28.0 Standard library for ppx rewriters
pyml 20220905 OCaml bindings for Python
pythonlib v0.15.1 A library to help writing wrappers around ocaml code for python
re 1.10.4 RE is a regular expression library for OCaml
result 1.5 Compatibility Result module
seq base Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib v0.15.1 Library for serializing OCaml values to and from S-expressions
sexplib0 v0.15.1 Library containing the definition of S-expressions and some base converters
stdcompat 19 Compatibility module for OCaml standard library
stdio v0.15.0 Standard IO library for OCaml
stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler
time_now v0.15.0 Reports the current time
typerep v0.15.0 Typerep is a library for runtime types
yojson 2.0.2 Yojson is an optimized parsing and printing library for the JSON format
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integersIndeed some deps are wrong, see pycoq.opam file, in particular the ppxlib version is critical I think, 0.28.0 doesn't work with this repos.
You can try to get the right stuff installed using:
opam install --deps-only .From the pycoq directory.
As you can see the project is not very active these days as I've been working on https://github.com/ejgallego/coq-lsp , which includes a new checking engine; coq-lsp could be very useful for you, depending on your use case.
Once coq-lsp is a bit more stable we hope to port and update this project to use it.
ejgallego
commented
1 year ago When I wrote pycoq some OCaml libraries where under migration, the situation is much better now; so if you need to use pyCoq with a newer Coq version we should be able to update this.
ASamSam
commented
1 year ago practically, i'm trying to study some Coq files executing them in pqrqllel in COQ, and python is very comfortable for me for this task. I'm not doing something special, so even the old version of COQ should be OK for me. ok, thanks, I'll try opam install --deps-only .
brando90
commented
1 year ago @ejgallego installations https://github.com/ejgallego/pycoq dont make sense from a python perspective user. After I run the opam stuff and have the right switch and coq, as a python using I'd expect something like this:
pip install pycoq-emilioor
cd ~/pycoq-emilio/
pip install -e .can a standard python tool like pip be used to install pycoq-emilio? Right now it doesn't make sense how to install it. Specifically, git submodules after this:
If that's your first checkout, you'll also have to update the git submodules, usually using git submodule update --init --recursive.
is very odd. Plus no reference to git cloning your repo, or anything else is mentioned there so it's very confusing. What are we suppose to do once we get to the git submodule command? Are you expect me to have cloned your repo or something?
brando90
commented
1 year ago also no reference to a python environment manager like conde is mentioned. Usually people have set up something like this:
conda create -n iit_synthesis python=3.9
conda activate iit_synthesisand start pip/conda installing packages.
brando90
commented
1 year ago ok then the next sentence comes out of the blue:
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.
Why is this mentioned without context? Why should a user of pycoq-emilio care?
brando90
commented
1 year ago Once the right dependencies have been installed, you can do:
which depedencies?
ejgallego
commented
1 year ago @brando90 indeed the current setup procedure is not pythonic at all, patches welcome. In short, what it needs to be done here is:
duneOCAMLPATH to be set properly, in particular to either _build/install/default/lib or to whatever place the OCaml libs that pyCoq has are installed.I'm don't know how to make that work in a standard python env.
brando90
commented
1 year ago @ejgallego I can help with that in a bit. But until the gap from
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.
to
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.
Once the right dependencies have been installed, you can do:
$ make install && dune build examples/test.py && dune exec -- python3 _build/default/examples/test.py
is made clear to me it will be hard for me to help. What secret commands were run btw there? I'm puzzled. Let me share you what I have so far.
brando90
commented
1 year ago # --- 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_synthesisOk I have all that done. What do I do after? @ejgallego
brando90
commented
1 year ago @ejgallego this is what I think is next:
# - 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.pybut fails:
(iit_synthesis) brandomiranda~/pycoq-ejgallego ❯ 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
zsh: command not found: #
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_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/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/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 moving discussion here: https://coq.zulipchat.com/#narrow/stream/252087-Machine-learning-and-automation/topic/pycoq-egallego
hope to close issue once I get a conclusion/solution.
brando90
commented
1 year ago @ejgallego I still need help.
Last command I did was
$ opam install --deps-only coq-serapi
$ opam install pythonlibafter 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!)
sorry, still trying to install pycoq. did install coq 8.14.1 can you please help me with those problems?
1.
did fix it providing Location.none as second argument then
make install dune build @pip-install File "coq-serapi/serlib/ser_constr.ml", line 104, characters 12-19: 104 | [%import: 'constr Constr.pcase_return] ^^^^^^^ Error: ppx_sexp_conv: unbound type variable 'constr File "coq-serapi/serlib/ser_locus.ml", line 62, characters 12-15: 62 | [%import: 'id Locus.clause_expr] ^^^ Error: ppx_sexp_conv: unbound type variable 'id File "coq-serapi/serlib/ser_univ.ml", lines 43-47, characters 2-35: 43 | ..type _t = 44 | { hash : int 45 | ; data : RawLevel.t 46 | } 47 | [@@deriving sexp, yojson, python] Error: Unbound value Stdlib.ref File "interp/genintern.mli", lines 17-23, characters 0-1: Error: Unbound value Stdlib.ref File "kernel/environ.mli", lines 51-56, characters 2-5: Error: Unbound value Stdlib.ref File "coq-serapi/sertop/sercomp.ml", line 233, characters 4-13: 233 | Term.info "sercomp" ~version:sercomp_version ~doc:sercomp_doc ~man:sercomp_man ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.info Use Cmd.info instead. File "coq-serapi/sertop/sercomp.ml", line 236, characters 12-21: 236 | try match Term.eval ~catch:false sercomp_cmd with ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.eval Use Cmd.v and one of Cmd.eval instead. File "coq-serapi/sertop/sername.ml", line 221, characters 4-13: 221 | Term.info "sername" ~version:sername_version ~doc:sername_doc ~man:sername_man ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.info Use Cmd.info instead. File "coq-serapi/sertop/sername.ml", line 224, characters 12-21: 224 | try match Term.eval ~catch:false sername_cmd with ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.eval Use Cmd.v and one of Cmd.eval instead. File "coq-serapi/sertop/sertok.ml", line 214, characters 4-13: 214 | Term.info "sertok" ~version:sertok_version ~doc:sertok_doc ~man:sertok_man ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.info Use Cmd.info instead. File "coq-serapi/sertop/sertok.ml", line 217, characters 12-21: 217 | try match Term.eval ~catch:false sertok_cmd with ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.eval Use Cmd.v and one of Cmd.eval instead. File "coq-serapi/sertop/sertop_bin.ml", line 84, characters 2-11: 84 | Term.info "sertop" ~version:sertop_version ~doc ~man ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.info Use Cmd.info instead. File "coq-serapi/sertop/sertop_bin.ml", line 87, characters 8-17: 87 | match Term.eval sertop_cmd with ^^^^^^^^^ Error (alert deprecated): Cmdliner.Term.eval Use Cmd.v and one of Cmd.eval instead. File "pycoq/pycoq.ml", line 98, characters 27-34: 98 | Pymodule.set mod "add" coq_add; ^^^^^^^ Error: This expression has type pyobject D.t but an expression was expected of type (unit -> pyobject) D.t Hint: Did you forget to wrap the expression using `fun () ->'? make: *** [Makefile:14: install] Error 1