Merge pull request #192 from ejgallego/v8.11+wrap

[serapi] [general] Bump version numbers for 8.11 and wrap libraries

CHANGES.md

@@ -3,6 +3,9 @@
  * [general] (!) support Coq 8.11, a few datatypes have changed, in
              particular `CoqAst` handles locations as an AST node, and
              the kernel type includes primitive floats.
+ * [general] (!) Now the `sertop` and `serapi` OCaml libraries are
+             built packed, we've also bumped their compat version number
+             (#192 @ejgallego)
 
 ## Version 0.7.0:
 

FAQ.md

@@ -13,8 +13,8 @@ changelog with `(!)`.
 
 ## Which Coq versions does SerAPI support?
 
-At the moment, Coq 8.10 is the current supported version for the
-current protocol. Older versions (8.6---8.9) work, however the
+At the moment, Coq 8.11 is the current supported version for the
+current protocol. Older versions (8.6---8.10) work, however the
 protocol and feature sets do differ.
 
 ## How can I install SerAPI?

README.md

@@ -1,6 +1,6 @@
 ## SerAPI: Machine-Friendly, Data-Centric Serialization for Coq
 
-[![Build Status](https://travis-ci.org/ejgallego/coq-serapi.svg?branch=v8.10)](https://travis-ci.org/ejgallego/coq-serapi) [![Gitter](https://badges.gitter.im/coq-serapi/Lobby.svg)](https://gitter.im/coq-serapi/Lobby)
+[![Build Status](https://travis-ci.org/ejgallego/coq-serapi.svg?branch=v8.11)](https://travis-ci.org/ejgallego/coq-serapi) [![Gitter](https://badges.gitter.im/coq-serapi/Lobby.svg)](https://gitter.im/coq-serapi/Lobby)
 
 ```
 $ opam install coq-serapi
@@ -103,7 +103,7 @@ There are three categories of [commands](serapi/serapi_protocol.mli#L147):
 
 ### Roadmap:
 
-SerAPI 0.7.x is based on Coq 8.10. These days, most work related to
+SerAPI 0.11.x is based on Coq 8.11. These days, most work related to
 SerAPI is directly happening over [Coq's upstream](https://github.com/coq/coq)
 itself. The main objective is to improve the proof-document model; building
 a rich query language will be next.

notes/build.md

@@ -2,22 +2,22 @@
 
 SerAPI is available for different Coq versions, with each of its
 branches targeting the corresponding Coq branch. The current
-development branch is `v8.10` targeting Coq's `v8.10` branch.
+development branch is `v8.11` targeting Coq's `v8.11` branch.
 
 Basic build instructions are below; the `.travis.yml` files should
 contain up-to-date information in any case. We recommend using OPAM to
 setup the build environment, however Théo Zimmermann has reported
 success in [NixOS](https://nixos.org).
 
 0. The currently supported OCaml version is 4.07.1:
-   ``$ opam switch 4.07.1 && eval $(opam env)``. We also assume `COQVER=v8.10`.
+   ``$ opam switch 4.07.1 && eval $(opam env)``. We also assume `COQVER=v8.11`.
 1. Install the needed packages:
    `$ opam install cmdliner sexplib dune ppx_import ppx_deriving ppx_sexp_conv yojson ppx_deriving_yojson`.
 2. Download and compile Coq. We recommend:
    `$ git clone -b ${COQVER} https://github.com/coq/coq.git ~/external/coq-${COQVER} && cd ~/external/coq-${COQVER} && ./configure -local -native-compiler no && make -j $NJOBS`.
 3. Type `make SERAPI_COQ_HOME=~/external/coq-${COQVER}` to build `sertop`.
 
-Alternatively, you can install Coq `>= 8.10` using OPAM and build against it using just `make`.
+Alternatively, you can install Coq `>= 8.11` using OPAM and build against it using just `make`.
 
 The above instructions assume that you use `~/external/coq-${COQVER}`
 directory to place the Coq build that SerAPI needs; you can modify
@@ -39,6 +39,7 @@ If that is not properly done, the usual symptom is the error message:
 (CoqExn "Cannot link ml-object ground_plugin.cmxs to Coq code (Fl_package_base.No_such_package(\"coq-serapi.serlib.ground_plugin\", \"\"))."))
 ```
 When executing binaries via `dune exec`, be sure to pass any arguments after `--`, e.g., `dune exec sercomp -- --help`.
+
 ## Advanced Developer Setup
 
 SerAPI builds using Dune which supports modular builds. Starting with

serapi/dune

@@ -1,6 +1,5 @@
 (library
  (name serapi)
- (public_name coq-serapi.serapi_v8_10)
- (wrapped false)
+ (public_name coq-serapi.serapi_v8_11)
  (synopsis "Serialization Protocol for Coq")
  (libraries coq.stm coq.plugins.ltac sexplib))

serlib/plugins/extraction/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_extraction)
  (public_name coq-serapi.serlib.extraction_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq Fundind Plugin")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.extraction serlib))

serlib/plugins/firstorder/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_firstorder)
  (public_name coq-serapi.serlib.ground_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq Firstorder Plugin")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.firstorder serlib sexplib))

serlib/plugins/funind/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_funind)
  (public_name coq-serapi.serlib.recdef_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq Fundind Plugin")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.funind serlib serlib_ltac sexplib))

serlib/plugins/funind/ser_g_indfun.ml

@@ -6,7 +6,7 @@ module Constrexpr = Ser_constrexpr
 module Tactypes   = Ser_tactypes
 module Genintern  = Ser_genintern
 module EConstr    = Ser_eConstr
-module Tacexpr    = Ser_tacexpr
+module Tacexpr    = Serlib_ltac.Ser_tacexpr
 
 module A1 = struct
 

serlib/plugins/ltac/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_ltac)
  (public_name coq-serapi.serlib.ltac)
- (wrapped false)
  (synopsis "Serialization Library for Coq [LTAC plugin]")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.ltac serlib sexplib))

serlib/plugins/setoid_ring/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_setoid_ring)
  (public_name coq-serapi.serlib.newring_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq Setoid Newring Plugin")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.setoid_ring serlib serlib_ltac sexplib))

serlib/plugins/setoid_ring/ser_g_newring.ml

@@ -7,10 +7,10 @@ module Constrexpr = Ser_constrexpr
 module Tactypes   = Ser_tactypes
 module Genintern  = Ser_genintern
 module EConstr    = Ser_eConstr
-module Tacexpr    = Ser_tacexpr
+module Tacexpr    = Serlib_ltac.Ser_tacexpr
 
 module Ltac_plugin = struct
-  module Tacexpr = Ser_tacexpr
+  module Tacexpr = Serlib_ltac.Ser_tacexpr
 end
 
 type 'constr coeff_spec =

serlib/plugins/ssr/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_ssr)
  (public_name coq-serapi.serlib.ssreflect_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq [SSR plugin]")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.ssreflect serlib serlib_ltac serlib_ssrmatching sexplib))

serlib/plugins/ssr/ser_ssrast.ml

@@ -26,11 +26,11 @@ module Genintern  = Ser_genintern
 module Geninterp  = Ser_geninterp
 
 module Ssrmatching_plugin = struct
-  module Ssrmatching = Ser_ssrmatching
+  module Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching
 end
 
 module Ltac_plugin = struct
-  module Tacexpr = Ser_tacexpr
+  module Tacexpr = Serlib_ltac.Ser_tacexpr
 end
 
 (* What a hack is ssreflect using... *)

serlib/plugins/ssr/ser_ssrequality.ml

@@ -16,7 +16,7 @@
 open Sexplib.Conv
 
 module Ssrmatching_plugin = struct
-  module Ssrmatching = Ser_ssrmatching
+  module Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching
 end
 
 module Ssreflect_plugin = struct

serlib/plugins/ssr/ser_ssrparser.ml

@@ -18,11 +18,11 @@
 open Sexplib.Conv
 open Serlib
 
-module Ssrmatching = Ser_ssrmatching
+module Ssrmatching = Serlib_ssrmatching.Ser_ssrmatching
 open Ssrmatching
 
 module Ltac_plugin = struct
-  module Tacexpr = Ser_tacexpr
+  module Tacexpr = Serlib_ltac.Ser_tacexpr
 end
 
 module Ssrast = Ser_ssrast
@@ -108,9 +108,9 @@ let ser_wit_ssrhintarg =
   }
 
 module A1 = struct
-  type h1 = Ser_tacexpr.raw_tactic_expr ssrseqarg
+  type h1 = Serlib_ltac.Ser_tacexpr.raw_tactic_expr ssrseqarg
   [@@deriving sexp]
-  type h2 = Ser_tacexpr.glob_tactic_expr ssrseqarg
+  type h2 = Serlib_ltac.Ser_tacexpr.glob_tactic_expr ssrseqarg
   [@@deriving sexp]
   type h3 = Geninterp.Val.t ssrseqarg
   [@@deriving sexp]
@@ -128,9 +128,9 @@ let ser_wit_ssrseqarg = let open A1 in Ser_genarg.
   }
 
 module A2 = struct
-  type h1 = Ser_tacexpr.raw_tactic_expr * ssripats
+  type h1 = Serlib_ltac.Ser_tacexpr.raw_tactic_expr * ssripats
   [@@deriving sexp]
-  type h2 = Ser_tacexpr.glob_tactic_expr * ssripats
+  type h2 = Serlib_ltac.Ser_tacexpr.glob_tactic_expr * ssripats
   [@@deriving sexp]
   type h3 = Geninterp.Val.t * ssripats
   [@@deriving sexp]
@@ -148,9 +148,9 @@ let ser_wit_ssrintrosarg = let open A2 in Ser_genarg.
   }
 
 module A3 = struct
-  type h1 = Ser_tacexpr.raw_tactic_expr ffwbinders
+  type h1 = Serlib_ltac.Ser_tacexpr.raw_tactic_expr ffwbinders
   [@@deriving sexp]
-  type h2 = Ser_tacexpr.glob_tactic_expr ffwbinders
+  type h2 = Serlib_ltac.Ser_tacexpr.glob_tactic_expr ffwbinders
   [@@deriving sexp]
   type h3 = Geninterp.Val.t ffwbinders
   [@@deriving sexp]
@@ -169,9 +169,9 @@ end
 let ser_wit_ssrcongrarg = let open A4 in Ser_genarg.mk_uniform sexp_of_h1 h1_of_sexp
 
 module A5 = struct
-  type h1 = Ser_tacexpr.raw_tactic_expr ssrdoarg
+  type h1 = Serlib_ltac.Ser_tacexpr.raw_tactic_expr ssrdoarg
   [@@deriving sexp]
-  type h2 = Ser_tacexpr.glob_tactic_expr ssrdoarg
+  type h2 = Serlib_ltac.Ser_tacexpr.glob_tactic_expr ssrdoarg
   [@@deriving sexp]
   type h3 = Geninterp.Val.t ssrdoarg
   [@@deriving sexp]
@@ -191,9 +191,9 @@ end
 let ser_wit_ssrsetfwd = let open A6 in Ser_genarg.mk_uniform sexp_of_h1 h1_of_sexp
 
 module A7 = struct
-  type h1 = Ser_tacexpr.raw_tactic_expr ssrhint
+  type h1 = Serlib_ltac.Ser_tacexpr.raw_tactic_expr ssrhint
   [@@deriving sexp]
-  type h2 = Ser_tacexpr.glob_tactic_expr ssrhint
+  type h2 = Serlib_ltac.Ser_tacexpr.glob_tactic_expr ssrhint
   [@@deriving sexp]
   type h3 = Geninterp.Val.t ssrhint
   [@@deriving sexp]
@@ -345,8 +345,8 @@ let register () =
   Ssreflect_plugin.Ssrparser.wit_ssrstruct
 *)
   register_genser wit_ssrsufffwd ser_wit_ssrsufffwd;
-  register_genser wit_ssrtacarg Ser_tacarg.ser_wit_tactic;
-  register_genser wit_ssrtclarg Ser_tacarg.ser_wit_tactic;
+  register_genser wit_ssrtacarg Serlib_ltac.Ser_tacarg.ser_wit_tactic;
+  register_genser wit_ssrtclarg Serlib_ltac.Ser_tacarg.ser_wit_tactic;
 
   register_genser wit_ssrterm       (mk_uniform sexp_of_ssrterm ssrterm_of_sexp);
   register_genser wit_ssrunlockarg  ser_wit_ssrunlockarg;

serlib/plugins/ssrmatching/dune

@@ -1,7 +1,6 @@
 (library
  (name serlib_ssrmatching)
  (public_name coq-serapi.serlib.ssrmatching_plugin)
- (wrapped false)
  (synopsis "Serialization Library for Coq [SSR Matching plugin]")
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries coq.plugins.ssrmatching serlib serlib_ltac sexplib))

sertop/dune

@@ -1,17 +1,17 @@
 (library
- (name sertoplib)
- (public_name coq-serapi.sertop_v8_10)
- (modules :standard \ sertop sercomp sertok sertop_js sertop_async)
- (wrapped false)
+ (name sertop)
+ (public_name coq-serapi.sertop_v8_11)
+ (modules :standard \ sertop_bin sercomp sertok sertop_js sertop_async)
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (libraries findlib.dynload cmdliner serapi serlib serlib_ltac))
 
 (executables
  (public_names sertop sercomp sertok)
- (modules sertop sercomp sertok)
+ (names sertop_bin sercomp sertok)
+ (modules sertop_bin sercomp sertok)
  (preprocess (staged_pps ppx_import ppx_sexp_conv))
  (link_flags -linkall)
- (libraries sertoplib num))
+ (libraries sertop num))
 
 (executable
  (name sertop_js)
@@ -27,7 +27,7 @@
   (flags :standard --dynlink +nat.js +dynlink.js +toplevel.js))
 ; (flags :standard --dynlink +nat.js +dynlink.js +toplevel.js --pretty --noinline --disable shortvar --debug-info)
  (link_flags -linkall -noautolink -no-check-prims)
- (libraries sertoplib ppx_deriving_yojson.runtime jscoq_lib))
+ (libraries sertop ppx_deriving_yojson.runtime jscoq_lib))
 
 (rule
  (targets ser_version.ml)

sertop/sercomp.ml

@@ -25,7 +25,7 @@ let fatal_exn exn info =
 
 let create_document ~in_file ~async ~async_workers ~quick ~iload_path ~debug =
 
-  let open Sertop_init in
+  let open Sertop.Sertop_init in
 
   (* coq initialization *)
   coq_init
@@ -75,7 +75,7 @@ let create_document ~in_file ~async ~async_workers ~quick ~iload_path ~debug =
 exception End_of_input
 let input_doc ~input ~in_file ~in_chan ~process ~doc ~sid =
   let stt = ref (doc, sid) in
-  let open Sertop_arg in
+  let open Sertop.Sertop_arg in
   match input with
   | I_vernac ->
      begin
@@ -111,14 +111,14 @@ let process_vernac ~mode ~pp ~doc ~sid ast =
   let doc, n_st, tip = Stm.add ~doc ~ontop:sid false ast in
   if tip <> `NewTip then
     CErrors.user_err ?loc:ast.loc Pp.(str "fatal, got no `NewTip`");
-  let open Sertop_arg in
+  let open Sertop.Sertop_arg in
   let () = match mode with
     | C_env   -> ()
     | C_vo    -> ()
     | C_check -> ()
     | C_parse -> ()
     | C_stats ->
-      Sercomp_stats.do_stats ast
+      Sertop.Sercomp_stats.do_stats ast
     | C_print ->
       printf "@[%a@]@\n%!" Pp.pp_with Ppvernac.(pr_vernac ast)
     | C_sexp ->
@@ -139,13 +139,13 @@ let check_pending_proofs ~pstate =
     ) pstate
 
 let close_document ~pp ~mode ~doc ~in_file ~pstate =
-  let open Sertop_arg in
+  let open Sertop.Sertop_arg in
   match mode with
   | C_parse -> ()
   | C_sexp  -> ()
   | C_print -> ()
   | C_stats ->
-    Sercomp_stats.print_stats ()
+    Sertop.Sercomp_stats.print_stats ()
   | C_check ->
     let _doc = Stm.join ~doc in
     check_pending_proofs ~pstate
@@ -162,7 +162,7 @@ let close_document ~pp ~mode ~doc ~in_file ~pstate =
     Library.save_library_to todo_proofs ~output_native_objects:false ldir out_vo (Global.opaque_tables ())
 
 (* Command line processing *)
-let sercomp_version = Ser_version.ser_git_version
+let sercomp_version = Sertop.Ser_version.ser_git_version
 
 let sercomp_man =
   [
@@ -185,14 +185,14 @@ open Cmdliner
 let driver input mode debug printer async async_workers quick coq_path ml_path load_path rload_path in_file omit_loc omit_att exn_on_opaque =
 
   (* closures *)
-  let pp = Sertop_ser.select_printer printer in
+  let pp = Sertop.Sertop_ser.select_printer printer in
   let process = process_vernac ~mode ~pp in
 
   (* initialization *)
   let options = Serlib.Serlib_init.{ omit_loc; omit_att; exn_on_opaque } in
   Serlib.Serlib_init.init ~options;
 
-  let iload_path = Serapi_paths.coq_loadpath_default ~implicit:true ~coq_path @ ml_path @ load_path @ rload_path in
+  let iload_path = Serapi.Serapi_paths.coq_loadpath_default ~implicit:true ~coq_path @ ml_path @ load_path @ rload_path in
   let doc, sid = create_document ~in_file ~async ~async_workers ~quick ~iload_path ~debug in
 
   (* main loop *)
@@ -212,7 +212,7 @@ let main () =
   in
 
   let sercomp_cmd =
-    let open Sertop_arg in
+    let open Sertop.Sertop_arg in
     Term.(const driver
           $ comp_input $ comp_mode $ debug $ printer $ async $ async_workers $ quick $ prelude
           $ ml_include_path $ load_path $ rload_path $ input_file $ omit_loc $ omit_att $ exn_on_opaque