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.))
You need to setup the OCaml compilation environment properly, for that particular case OCAMLPATH
should point to where Coq's META file is
once ocamlfind list
does list the coq libs, you should be good to go
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
?
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
?
Is 4.06.1+fp too old for serapi?
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
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
Check the coq-serapi.opam file for the exact deps
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)
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
I recommend dune install
as opposed to opam-installer
, but YMMV
So the usual build / install sequence is dune build -p coq-serapi && dune install -p coq-serapi
If you are compiling from sources you need to do dune subst
usually
This is not needed when working with release tarballs
Note that these steps are generic for almost all the packages using dune
so you can just write a small dune_build
script that can handle ocaml packages uniformly
Awesome, thanks!
By the way you don't really need to install serapi if you are adjusting ocamlpath etc...
you can just run it from _build/install
Coq will soon phase local out by this scheme
Last updated: Oct 13 2024 at 01:02 UTC