[v8.20] [serlib] Embed serlib and remove dependency on coq-lsp.

.gitmodules

@@ -1,4 +0,0 @@
-[submodule "vendor/coq-lsp"]
-	path = vendor/coq-lsp
-	url = https://github.com/ejgallego/coq-lsp.git
-	branch = serlib_merge

Makefile

@@ -17,7 +17,7 @@ GITDEPS=$(ls .git/HEAD .git/index)
 sertop/ser_version.ml: $(GITDEPS)
 	echo "let ser_git_version = \"$(shell git describe --tags || cat VERSION)\";;" > $@
 
-build: vendor/coq-lsp
+build:
 	dune build --root . --only-packages=$(SP_PKGS) @install
 
 check:

coq/dune

@@ -0,0 +1,5 @@
+(library
+ (name coq)
+ (public_name coq-serapi.coq)
+ (libraries coq-core.vernac))
+

coq/loader.ml

@@ -0,0 +1,100 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* coq-lsp / SerAPI                                                     *)
+(************************************************************************)
+(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+             *)
+(* Copyright 2019-2024 Inria           -- License LGPL 2.1+             *)
+(* Written by: Emilio J. Gallego Arias and others                       *)
+(************************************************************************)
+
+[@@@ocamlformat "disable"]
+
+let list_last l = List.(nth l (length l - 1))
+
+let not_available_warn fl_pkg info =
+    Feedback.msg_warning
+      Pp.(str "Serlib plugin: " ++ str fl_pkg
+          ++ str " is not available" ++ str info ++ str "." ++ fnl ()
+          ++ str "Incremental checking for commands in this plugin will be impacted.")
+
+let check_package_exists fl_pkg =
+  try
+    let _ = Findlib.package_directory fl_pkg in
+    Some fl_pkg
+  with
+  | Findlib.No_such_package (_, info) ->
+    not_available_warn fl_pkg info;
+    None
+
+(* Should improve *)
+let map_serlib fl_pkg =
+  let supported = match fl_pkg with
+    (* Supported by serlib *)             (* directory   *)
+    | "coq-core.plugins.btauto"           (* btauto *)
+    | "coq-core.plugins.cc_core"          (* cc_core  *)
+    | "coq-core.plugins.cc"               (* cc  *)
+    | "coq-core.plugins.extraction"       (* extraction  *)
+    | "coq-core.plugins.firstorder_core"  (* firstorder_core  *)
+    | "coq-core.plugins.firstorder"       (* firstorder  *)
+    | "coq-core.plugins.funind"           (* funind      *)
+    | "coq-core.plugins.ltac"             (* ltac        *)
+    | "coq-core.plugins.ltac2"            (* ltac2       *)
+    | "coq-core.plugins.micromega"        (* micromega   *)
+    | "coq-core.plugins.micromega_core"   (* micromega_core *)
+    | "coq-core.plugins.ring"             (* ring        *)
+    | "coq-core.plugins.ssreflect"        (* ssreflect   *)
+    | "coq-core.plugins.ssrmatching"      (* ssrmatching *)
+    | "coq-core.plugins.number_string_notation" (* syntax *)
+    | "coq-core.plugins.tauto"            (* tauto *)
+    | "coq-core.plugins.zify"             (* zify *)
+      -> true
+    | _ ->
+      not_available_warn fl_pkg ": serlib support is missing";
+      false
+  in
+  if supported
+  then
+    let plugin_name = String.split_on_char '.' fl_pkg |> list_last in
+    let serlib_name = "coq-lsp.serlib." ^ plugin_name in
+    check_package_exists serlib_name
+  else None
+
+(* We used to be liberal here in the case a SerAPI plugin was not available.
+   This proved to be a bad choice as Coq got confused when plugin loading
+   failed. Par-contre, we now need to make the list in `map_serlib` open, so
+   plugins can register whether they support serialization. I'm afraid that'll
+   have to happen via the finlib database as we cannot load anticipatedly a
+   plugin that may not exist. *)
+let safe_loader loader fl_pkg =
+  try loader [fl_pkg]
+  with
+    exn ->
+    let iexn = Exninfo.capture exn in
+    let exn_msg = CErrors.iprint iexn in
+     Feedback.msg_warning
+      Pp.(str "Loading findlib plugin: " ++ str fl_pkg
+          ++ str "failed" ++ fnl () ++ exn_msg);
+    Exninfo.iraise iexn
+
+let default_loader pkgs : unit =
+  Fl_dynload.load_packages ~debug:false pkgs
+
+let plugin_handler user_loader =
+  let loader = Option.default default_loader user_loader in
+  let safe_loader = safe_loader loader in
+  fun fl_pkg ->
+    let _, fl_pkg = Mltop.PluginSpec.repr fl_pkg in
+    match map_serlib fl_pkg with
+    | Some serlib_pkg ->
+      safe_loader serlib_pkg
+    | None ->
+      safe_loader fl_pkg

coq/loader.mli

@@ -0,0 +1,22 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(************************************************************************)
+(* coq-lsp / SerAPI                                                     *)
+(************************************************************************)
+(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+             *)
+(* Copyright 2019-2024 Inria           -- License LGPL 2.1+             *)
+(* Written by: Emilio J. Gallego Arias and others                       *)
+(************************************************************************)
+
+(** [plugin_handler user_loader] Plugin loader that will also load the
+    instrumentation plugins for serlib if those available. [user_loader] can be
+    used to override the default of [Fl_dynload.load_packages] as loader. *)
+val plugin_handler : (string list -> unit) option -> Mltop.PluginSpec.t -> unit

serlib_8_20/.ocamlformat

@@ -0,0 +1 @@
+disable

serlib_8_20/README.md

@@ -0,0 +1,142 @@
+## Serlib README
+
+Welcome to `coq-serlib` README.
+
+`coq-serlib` is a library that declares missing serialization
+functions (from/to JSON, sexp), comparison, and hash functions for
+most Coq datatypes, allowing users to serialize full ASTs faithfully
+for example, and many other interesting use cases.
+
+`coq-serlib` also includes support for [Coq's extensible syntax]() and
+plugins.
+
+### Builtins and Configuration
+
+`serlib` provides some builtins and configuration values in the
+`Serlib_base` and `Serlib_init` modules.
+
+### Serializing regular Coq types
+
+The standard recipe is to use a combination of `ppx_import` and
+several ppx-based "derivers" to make `serlib` generate the
+corresponding serializers.
+
+The pattern for a Coq module `Foo` exporting the datatype `bar` and
+their constructors is:
+
+1. create a new OCaml module named `ser_foo.ml`
+2. get the corresponding serializers for existing types in scope, this is unusually done in two steps:
+  - serializers for OCaml Stdlib:
+```ocaml
+open Ppx_hash_lib.Std.Hash.Builtin
+open Ppx_compare_lib.Builtin
+open Sexplib.Std
+```
+  - serializers for types that `Foo.bar` depends on, for example:
+```ocaml
+module Names = Ser_names
+module EConstr = Ser_eConstr
+...
+```
+3. implement the serializers for your type. Add to `ser_foo.ml`:
+```ocaml
+type bar =
+  [%import: Foo.bar]
+  [@@deriving sexp,yojson,hash,compare]
+```
+
+Additionally, you can add an `.mli` file, with the same contents as
+above, but in this case, `[@@deriving ...]` will generate the right
+interface declarations.
+
+If `Foo.bar` has no public constructors, `Obj.magic` will be
+needed. `serlib` provides helpers for this, see below.
+
+### Serializing opaque and private types
+
+`serlib` uses `ppx_import` to retrieve the original type definitions
+from Coq; when these are not available, we provide some helpers in the
+`SerType` module. Current helpers are:
+
+- `Biject`: use when it is convenient to provide an isomorphic type to
+  the one that is "opaque".
+- `Pierce`: use when it is not possible to access the type, you really
+  want to use a copy + `Obj.magic`
+- `Opaque`: when you want to declare the type as non-serializable
+
+**note**: use of `Obj.magic` is now prohibited, all the type piercings
+need to use the `Pierce` functor.
+
+### Serializing GADTS
+
+Unfortunately, it is not possible to easily serialize GADTS. For now,
+we use a very ugly workaround: we basically copy the original Coq
+datatype, in non-GADT version, then we pierce the type as their
+representation is isomorphic.
+
+We will use an example from https://github.com/coq/coq/pull/17667#issuecomment-1714473449 :
+
+```ocaml
+type _ gen_pattern = GPat : Genarg.glob_generic_argument -> [ `uninstantiated ] gen_pattern
+```
+
+In this case, we could indeed derive a serialization function (try
+`[@@deriving of_sexp]` for example), however full serialization is
+harder, so we may need to provide an alternative data-type:
+
+```ocaml
+module GenPatternRep : SerType.Pierceable1 = struct
+
+    type 'a t = 'a Pattern.gen_pattern
+
+    type _ _t = GPat of Genarg.glob_generic_argument
+       [@@deriving sexp,yojson,hash,compare]
+end
+
+module GenPatternSer = SerType.Pierce1(GenPatternRep)
+type 'a gen_pattern = GenPatternSer.t [@@deriving sexp,yojson,hash,compare]
+```
+
+and here you go! The main problem with this approach is that it
+requires a manual check for each use of `Pierce` and each Coq
+version. Fortunately the numbers of `Pierce`'s so far have been very
+low.
+
+### Pre-release checks
+
+Due to the above, when updating SerAPI for a new release to OPAM, we
+must check that the definitions we are piercing are up to date.
+
+I perform this check with Emacs + Merlin for OCaml:
+
+- I do `vc-git-grep` for `Pierce(` and `Pierce1(`
+- For each use, I use merlin to jump to the original type
+- I compare update these types
+
+That's painful, but takes like 10 minutes, so for now it is doable a
+couple of times a year. To illustrate, these are the current
+occurrences to check:
+
+```
+serlib/plugins/ltac2/ser_tac2expr.ml:module T2E = Serlib.SerType.Pierce(T2ESpec)
+serlib/plugins/ltac2/ser_tac2expr.ml:module GT2E = Serlib.SerType.Pierce(GT2ESpec)
+serlib/ser_cooking.ml:module B_ = SerType.Pierce(CIP)
+serlib/ser_environ.ml:  include SerType.Pierce(PierceSpec)
+serlib/ser_float64.ml:include SerType.Pierce(PierceSpec)
+serlib/ser_impargs.ml:module B_ = SerType.Pierce(ISCPierceSpec)
+serlib/ser_names.ml:include SerType.Pierce(MBIdBij)
+serlib/ser_names.ml:    include SerType.Pierce(PierceSpec)
+serlib/ser_names.ml:  include SerType.Pierce(PierceSpec)
+serlib/ser_numTok.ml:  include SerType.Pierce(PierceSpec)
+serlib/ser_opaqueproof.ml:module B_ = SerType.Pierce(OP)
+serlib/ser_opaqueproof.ml:module C_ = SerType.Pierce(OTSpec)
+serlib/ser_rtree.ml:include SerType.Pierce1(RTreePierce)
+serlib/ser_sList.ml:include SerType.Pierce1(SL)
+serlib/ser_safe_typing.ml:module B_ = SerType.Pierce(PC)
+serlib/ser_sorts.ml:include SerType.Pierce(PierceSpec)
+serlib/ser_stateid.ml:include SerType.Pierce(SId)
+serlib/ser_univ.ml:  module PierceImp = SerType.Pierce(PierceSpec)
+serlib/ser_univ.ml:  include SerType.Pierce(PierceSpec)
+serlib/ser_univ.ml:  include SerType.Pierce(ACPierceDef)
+serlib/ser_vmemitcodes.ml:module B = SerType.Pierce(PierceToPatch)
+```

serlib_8_20/dune

@@ -0,0 +1,12 @@
+(library
+ (name serlib)
+ (public_name coq-serapi.serlib)
+ (synopsis "AST utility Library for Coq")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_hash
+   ppx_compare
+   ppx_deriving_yojson))
+ (libraries coq-core.vernac sexplib))

serlib_8_20/plugins/btauto/dune

@@ -0,0 +1,12 @@
+(library
+ (name serlib_btauto)
+ (public_name coq-serapi.serlib.btauto)
+ (synopsis "Serialization Library for Coq BTauto Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.btauto serlib sexplib))

serlib_8_20/plugins/cc/dune

@@ -0,0 +1,12 @@
+(library
+ (name serlib_cc)
+ (public_name coq-serapi.serlib.cc)
+ (synopsis "Serialization Library for Coq Congruence Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.cc serlib sexplib))

serlib_8_20/plugins/extraction/dune

@@ -0,0 +1,12 @@
+(library
+ (name serlib_extraction)
+ (public_name coq-serapi.serlib.extraction)
+ (synopsis "Serialization Library for Coq Fundind Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.extraction serlib))

serlib_8_20/plugins/extraction/ser_g_extraction.ml

@@ -0,0 +1,56 @@
+(************************************************************************)
+(* SerAPI: Coq interaction protocol with bidirectional serialization    *)
+(************************************************************************)
+(* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+             *)
+(* Copyright 2019-2023 Inria           -- License LGPL 2.1+             *)
+(* Written by: Emilio J. Gallego Arias and others                       *)
+(************************************************************************)
+
+open Serlib
+
+open Sexplib.Conv
+open Ppx_compare_lib.Builtin
+open Ppx_hash_lib.Std.Hash.Builtin
+
+module Names = Ser_names
+
+module Extraction_plugin = struct
+  module G_extraction = Extraction_plugin.G_extraction
+  module Table = struct
+    type int_or_id =
+      [%import: Extraction_plugin.Table.int_or_id]
+      [@@deriving sexp,yojson,hash,compare]
+    type lang =
+      [%import: Extraction_plugin.Table.lang]
+      [@@deriving sexp,yojson,hash,compare]
+  end
+end
+
+module WitII = struct
+  type t = Extraction_plugin.Table.int_or_id
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_int_or_id = let module M = Ser_genarg.GSV(WitII) in M.genser
+
+module WitL = struct
+  type t = Extraction_plugin.Table.lang
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_language = let module M = Ser_genarg.GSV(WitL) in M.genser
+
+module WitMN = struct
+  type t = string
+    [@@deriving sexp,yojson,hash,compare]
+end
+
+let ser_wit_mlname = let module M = Ser_genarg.GSV(WitMN) in M.genser
+
+let register () =
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_int_or_id ser_wit_int_or_id;
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_language ser_wit_language;
+  Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_mlname ser_wit_mlname;
+  ()
+
+let _ = register ()