Jason Gross (Apr 09 2021 at 13:45): Jason Gross (Apr 09 2021 at 13:45):Does serapi not work if I install Coq via make install? I'm getting
+ make -j7 TIMED=1 COQBIN=/home/jgross/.local64/coq/coq-master/bin/
dune build @install
File "serapi/dune", line 5, characters 20-36:
5 | (libraries coq.stm coq.plugins.ltac sexplib))
^^^^^^^^^^^^^^^^
Error: Library "coq.plugins.ltac" not found.
Hint: try:
dune external-lib-deps --missing @install
What should I do?
(I'm not using opam to manage my Coq installations because I have 58 versions of Coq installed and I don't want to pay the extra overhead of having a different opam switch for each of them (at best I think that'll cost me an extra 10 GB of HD space. And also it'll take forever to install OCaml 58 times.))
Emilio Jesús Gallego Arias (Apr 09 2021 at 14:46):You need to setup the OCaml compilation environment properly, for that particular case OCAMLPATH should point to where Coq's META file is
Emilio Jesús Gallego Arias (Apr 09 2021 at 14:46):once ocamlfind list does list the coq libs, you should be good to go
Jason Gross (Apr 09 2021 at 17:05):Ah, great, thanks! What about the ppx stuff?
dune build @install
File "serlib/dune", line 5, characters 25-35:
5 | (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson))
^^^^^^^^^^
Error: Library "ppx_import" not found.
Hint: try:
dune external-lib-deps --missing @install
File "serlib/dune", line 5, characters 36-49:
5 | (preprocess (staged_pps ppx_import ppx_sexp_conv ppx_deriving_yojson))
^^^^^^^^^^^^^
Error: Library "ppx_sexp_conv" not found.
Hint: try:
dune external-lib-deps --missing @install
File "serlib/plugins/extraction/dune", line 5, characters 25-35:
5 | (preprocess (staged_pps ppx_import ppx_sexp_conv))
^^^^^^^^^^
Error: Library "ppx_import" not found.
Hint: try:
dune external-lib-deps --missing @install
File "serlib/plugins/firstorder/dune", line 5, characters 25-35:
5 | (preprocess (staged_pps ppx_import ppx_sexp_conv))
^^^^^^^^^^
Error: Library "ppx_import" not found.
Hint: try:
dune external-lib-deps --missing @install
File "serlib/plugins/funind/dune", line 5, characters 25-35:
5 | (preprocess (staged_pps ppx_import ppx_sexp_conv))
^^^^^^^^^^
I guess I just need opam install ppx_import?
Jason Gross (Apr 09 2021 at 17:09):What about
dune build @install
File "serlib/ser_environ.ml", line 50, characters 12-23:
Error: Unbound value Pervasives.ref_of_sexp
File "serlib/ser_genintern.ml", line 37, characters 12-44:
Error: Unbound value Pervasives.ref_of_sexp
File "serlib/ser_univ.ml", line 168, characters 12-35:
Error: Unbound value Lazy.t_of_sexp
File "sertop/sertop_sexp.ml", line 80, characters 16-33:
Error: Unbound module Stdlib
?
Jason Gross (Apr 09 2021 at 17:10):Is 4.06.1+fp too old for serapi?
Emilio Jesús Gallego Arias (Apr 09 2021 at 20:59):Yup, it has quite a bit of deps. Indeed the minimum version is 4.07.1 , as it is very cumbersome to support old versions due to Stdlib
Emilio Jesús Gallego Arias (Apr 09 2021 at 21:00):Note that the usual way to build SerAPI + Coq "locally", is just to vendor Coq, but I don't advertise this setup until Coq 8.14 is out
Emilio Jesús Gallego Arias (Apr 09 2021 at 21:01):Check the coq-serapi.opam file for the exact deps
Jason Gross (Apr 13 2021 at 13:37):Is there a branch of serapi that builds with master? I was only able to build with v8.13.
Also, how do I install coq-serapi? (And how do I uninstall it if I need to?) make install doesn't exist and make build-install doesn't seem to install things... (I'm trying to set it up so that pointing OCAMLPATH, etc at the right version of Coq will let me build Alectryon)
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:42):Is there a branch of serapi that builds with master? I was only able to build with v8.13.
No, usually we usually update SerAPI when betas are out, I hope we can improve this.
How do I install / uninstall
SerAPI follows opam standard layout [as generated by Dune], so you can use any of opam-install / dune install to install / uninstall
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:43):I recommend dune install as opposed to opam-installer, but YMMV
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:44):So the usual build / install sequence is dune build -p coq-serapi && dune install -p coq-serapi
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:44):If you are compiling from sources you need to do dune subst usually
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:44):This is not needed when working with release tarballs
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:45):Note that these steps are generic for almost all the packages using dune
Emilio Jesús Gallego Arias (Apr 13 2021 at 14:45):so you can just write a small dune_build script that can handle ocaml packages uniformly
Jason Gross (Apr 13 2021 at 18:48):Awesome, thanks!
Emilio Jesús Gallego Arias (Apr 13 2021 at 21:06):By the way you don't really need to install serapi if you are adjusting ocamlpath etc...
Emilio Jesús Gallego Arias (Apr 13 2021 at 21:06):you can just run it from _build/install
Emilio Jesús Gallego Arias (Apr 13 2021 at 21:07):Coq will soon phase local out by this scheme
Last updated: Apr 20 2024 at 07:01 UTC