Stream: SerAPI

Topic: Building


view this post on Zulip 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.))

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))
                             ^^^^^^^^^^

view this post on Zulip Jason Gross (Apr 09 2021 at 17:06):

I guess I just need opam install ppx_import?

view this post on Zulip 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

?

view this post on Zulip Jason Gross (Apr 09 2021 at 17:10):

Is 4.06.1+fp too old for serapi?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 09 2021 at 21:01):

Check the coq-serapi.opam file for the exact deps

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 14:43):

I recommend dune install as opposed to opam-installer, but YMMV

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 14:44):

If you are compiling from sources you need to do dune subst usually

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 14:44):

This is not needed when working with release tarballs

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 14:45):

Note that these steps are generic for almost all the packages using dune

view this post on Zulip 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

view this post on Zulip Jason Gross (Apr 13 2021 at 18:48):

Awesome, thanks!

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 21:06):

you can just run it from _build/install

view this post on Zulip Emilio Jesús Gallego Arias (Apr 13 2021 at 21:07):

Coq will soon phase local out by this scheme


Last updated: Sep 26 2023 at 11:01 UTC