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

.github/workflows/ci.yml

@@ -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 .
+          opam install --ignore-constraints-on=coq --deps-only vendor/coq-lsp/coq-lsp.opam
       - 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

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
 

coq-serapi.opam

@@ -25,6 +25,7 @@ authors: [
 depends: [
   "ocaml"               {           >= "4.09.0"              }
   "coq"                 {           >= "8.20" & < "8.21"     }
+  # "coq-lsp"      { >= "0.2.0" }
   "cmdliner"            {           >= "1.1.0"               }
   "ocamlfind"           {           >= "1.8.0"               }
   "sexplib"             {           >= "v0.13.0"             }

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