Adapt w.r.t. coq/coq#19313.

ejgallego · Jul 5, 2024 · 36d8f84 · 36d8f84
1 parent 3282609
commit 36d8f84
Show file tree

Hide file tree

Showing 7 changed files with 53 additions and 15 deletions.
diff --git a/coq/loader.ml b/coq/loader.ml
@@ -40,8 +40,10 @@ 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        *)

diff --git a/serlib/plugins/cc_core/dune b/serlib/plugins/cc_core/dune
@@ -0,0 +1,12 @@
+(library
+ (name serlib_cc_core)
+ (public_name coq-lsp.serlib.cc_core)
+ (synopsis "Serialization Library for Coq Cc_core Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.cc_core serlib sexplib))
diff --git a/serlib/plugins/firstorder_core/dune b/serlib/plugins/firstorder_core/dune
@@ -0,0 +1,12 @@
+(library
+ (name serlib_firstorder_core)
+ (public_name coq-lsp.serlib.firstorder_core)
+ (synopsis "Serialization Library for Coq Firstorder_core Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.firstorder_core serlib sexplib))
diff --git a/serlib/plugins/nsatz_core/dune b/serlib/plugins/nsatz_core/dune
@@ -0,0 +1,12 @@
+(library
+ (name serlib_nsatz_core)
+ (public_name coq-lsp.serlib.nsatz_core)
+ (synopsis "Serialization Library for Coq Nsatz_core Plugin")
+ (preprocess
+  (staged_pps
+   ppx_import
+   ppx_sexp_conv
+   ppx_deriving_yojson
+   ppx_hash
+   ppx_compare))
+ (libraries coq-core.plugins.nsatz_core serlib sexplib))
diff --git a/test/compiler/basic/run.t b/test/compiler/basic/run.t
@@ -7,7 +7,7 @@ Describe the project
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -18,7 +18,7 @@ Compile a single file, don't generate a `.vo` file:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -34,7 +34,7 @@ Compile a single file, generate a .vo file
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -54,7 +54,7 @@ Compile a dependent file
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -74,7 +74,7 @@ Compile both files
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -95,7 +95,7 @@ Compile a dependent file without the dep being built
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -132,7 +132,7 @@ Compile a file with all messages:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -143,7 +143,7 @@ Compile a file with all messages:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -173,15 +173,15 @@ Use two workspaces
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
   [message] Configuration loaded from Command-line arguments
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -198,7 +198,7 @@ Load the example plugin
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -211,7 +211,7 @@ Load the astdump plugin
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]
@@ -236,7 +236,7 @@ We do the same for the goaldump plugin:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]

diff --git a/test/compiler/exit_code/run.t b/test/compiler/exit_code/run.t
@@ -8,7 +8,7 @@ Describe the environment:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 3 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 3 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]

diff --git a/test/compiler/long_file/run.t b/test/compiler/long_file/run.t
@@ -11,7 +11,7 @@ We now compile the challenging file:
    - coqlib is at: [TEST_PATH]
      + coqcorelib is at: [TEST_PATH]
    - Modules [Coq.Init.Prelude] will be loaded by default
-   - 2 Coq path directory bindings in scope; 24 Coq plugin directory bindings in scope
+   - 2 Coq path directory bindings in scope; 27 Coq plugin directory bindings in scope
    - ocamlpath wasn't overriden
      + findlib config: [TEST_PATH]
      + findlib default location: [TEST_PATH]