[serlib] Remove serlib and use coq-lsp serlib version instead.

Also:

- Update README.
- Adapt CI

.github/workflows/ci.yml

@@ -41,7 +41,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x]
+        ocaml-compiler: [4.12.x, 4.13.x, 4.14.x]
         test-target: [test]
         extra-opam: [coq.dev]
         include:
@@ -60,6 +60,8 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
+        with:
+          submodules: true
       - name: Install apt dependencies
         run: |
           sudo apt-get install aptitude
@@ -100,7 +102,9 @@ jobs:
         if: ${{ matrix.extra-opam != '' }}
         run: opam install ${{ matrix.extra-opam }}
       - name: Install SerAPI deps
-        run: opam install --ignore-constraints-on=coq --deps-only .
+        run: |
+          opam install --ignore-constraints-on=coq --deps-only vendor/coq-lsp/coq-lsp.opam
+          opam install --ignore-constraints-on=coq,coq-lsp --deps-only .
       - name: Build SerAPI
         run: |
           opam exec -- make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME"

.gitmodules

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

CHANGES.md

@@ -2,6 +2,8 @@
 
  - [serlib] Support `micromega_core` plugin (@ejgallego)
  - [serlib] Compat with ppx_deriving 6 (@ejgallego)
+ - [serlib] Move `serlib` sources to `coq-lsp` (@ejgallego, #409)
+ - [general] Drop support for OCaml 4.09-4.11 (@ejgallego, #409)
 
 ## Version 0.19.3
 

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:
+build: vendor/coq-lsp
 	dune build --root . --only-packages=$(SP_PKGS) @install
 
 check:
@@ -40,6 +40,23 @@ browser:
 sertop: build
 	dune exec -- rlwrap sertop
 
+vendor/coq-lsp:
+	$(error Submodules not initialized, please do "make submodules-init")
+
+.PHONY: submodules-init
+submodules-init:
+	git submodule update --init
+
+# Deinitialize submodules
+.PHONY: submodules-deinit
+submodules-deinit:
+	git submodule deinit -f --all
+
+# Update submodules from upstream
+.PHONY: submodules-update
+submodules-update:
+	(cd vendor/coq-lsp && git checkout main && git pull upstream main)
+
 #####################################################
 # Misc
 

README.md

@@ -1,10 +1,15 @@
-**Note**: Coq SerAPI is now in maintenance mode, and has been
-succeeded by [coq-lsp](https://github.com/ejgallego/coq-lsp/), which
-solves many longstanding issues and feature requests.
+**Note**: Coq SerAPI has now stopped development, the 0.20 release for
+Coq 8.20 will be the last managed by us. Coq SerAPI has been succeeded
+by [coq-lsp](https://github.com/ejgallego/coq-lsp/), which solves many
+longstanding issues and feature requests.
 
 See https://github.com/ejgallego/coq-serapi/issues/252 for more
-information. The `serlib` component of this repository is still
-active, pending its integration in Coq at some point.
+information. The `serlib` component of this repository now lives in
+the `coq-lsp` repository..
+
+We'd like to thanks all the people that have contributed in one way or
+another to SerAPI after all these years, without you neither SerAPI or
+`coq-lsp` would have been possible.
 
 ## SerAPI: Machine-Friendly, Data-Centric Serialization for Coq
 

coq-serapi.opam

@@ -23,19 +23,21 @@ authors: [
 ]
 
 depends: [
-  "ocaml"               {           >= "4.09.0"                    }
+  "dune"                {           >= "2.0.1"                     }
+  "ocaml"               {           >= "4.12.0"                    }
   "coq"                 {           >= "8.20" & < "8.21" | = "dev" }
+  # We vendor this for now
+  # "coq-lsp"             {           >= "0.2.0"                     }
   "cmdliner"            {           >= "1.1.0"                     }
   "ocamlfind"           {           >= "1.8.0"                     }
   "sexplib"             {           >= "v0.13.0"                   }
   "dune"                {           >= "2.0.1"                     }
+  "cmdliner"            {           >= "1.1.0"               }
+  "ocamlfind"           {           >= "1.8.0"               }
   "ppx_import"          { build   & >= "1.5-3" & < "2.0"     }
   "ppx_deriving"        {           >= "4.2.1"               }
+  "sexplib"             {           >= "v0.13.0"             }
   "ppx_sexp_conv"       {           >= "v0.13.0"             }
-  "ppx_compare"         {           >= "v0.13.0"             }
-  "ppx_hash"            {           >= "v0.13.0"             }
-  "yojson"              {           >= "1.7.0"               }
-  "ppx_deriving_yojson" {           >= "3.4"                 }
 ]
 
 conflicts: [

dune

@@ -0,0 +1,2 @@
+(vendored_dirs vendor)
+

dune-project

@@ -1,4 +1,3 @@
 (lang dune 2.0)
 (formatting (enabled_for ocaml))
 (name coq-serapi)
-

serapi/serapi_protocol.ml

@@ -584,7 +584,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
   | TypeOf id      -> snd (QueryUtil.info_of_id env id)
   | Search         -> [CoqString "Not Implemented"]
   (* XXX: should set printing options in all queries *)
-  | Vernac q       -> let pa = Pcoq.Parsable.make (Ser_stream.of_string q) in
+  | Vernac q       -> let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string q) in
                       Stm.query ~doc ~at:opt.sid ~route:opt.route pa; []
   (* XXX: Should set the proper sid state *)
   | Env            -> [CoqEnv env]
@@ -700,12 +700,12 @@ module ControlUtil = struct
     parsing_state_of_st (Stm.state_of_id ~doc ontop)
     |> Option.map (fun pstate ->
         let entry = Pcoq.Constr.lconstr in
-        let pa = Pcoq.Parsable.make (Ser_stream.of_string str) in
+        let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string str) in
         Vernacstate.Parser.parse pstate entry pa)
 
   let parse_sentence ~doc ~ontop sent =
     let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in
-    let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in
+    let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in
     let entry = Pvernac.main_entry in
     Stm.parse_sentence ~doc ontop ~entry pa
 
@@ -718,7 +718,7 @@ module ControlUtil = struct
   exception End_of_input
 
   let add_sentences ~doc opts sent =
-    let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in
+    let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in
     let i   = ref 1                    in
     let acc = ref []                   in
     let stt = ref (Extra.value opts.ontop ~default:(Stm.get_current_state ~doc)) in
@@ -943,7 +943,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
   | Tokenize input ->
     let st = CLexer.Lexer.State.get () in
     begin try
-        let istr = Ser_stream.of_string input in
+        let istr = Gramlib.Stream.of_string input in
         let lex = CLexer.Lexer.tok_func istr in
         CLexer.Lexer.State.set st;
         let objs = Extra.stream_tok 0 [] lex in