Merge PR coq#19134: [ci] Switch dependencies serapi <-> coq_lsp

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

.gitlab-ci.yml

@@ -1028,23 +1028,14 @@ library:ci-rupicola:
   - library:ci-bedrock2
   stage: build-3+
 
-plugin:ci-serapi:
+plugin:ci-coq_lsp:
   extends: .ci-template-flambda
 
-plugin:ci-serapi_test:
-  extends: .ci-template-flambda
-  needs:
-  - build:edge+flambda
-  - plugin:ci-elpi_hb
-  - library:ci-mathcomp_1
-  - plugin:ci-serapi
-  stage: build-2
-
-plugin:ci-coq_lsp:
+plugin:ci-serapi:
   extends: .ci-template-flambda
   needs:
   - build:edge+flambda
-  - plugin:ci-serapi
+  - plugin:ci-coq_lsp
   stage: build-2
 
 plugin:ci-vscoq:

Makefile.ci

@@ -180,9 +180,7 @@ ci-compcert: ci-menhir ci-flocq
 
 ci-relation_algebra: ci-aac_tactics ci-mathcomp
 
-ci-serapi_test: ci-mathcomp_1 ci-serapi
-
-ci-coq_lsp: ci-serapi
+ci-serapi: ci-coq_lsp
 
 # Virtual targets used by the CI to group compilation of rules in a single job
 

dev/ci/ci-coq_lsp.sh

@@ -11,5 +11,10 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/coq_lsp"
   dune build --root . --only-packages=coq-lsp @install
+  # Tests
   _build/install/default/bin/coq-lsp --version
+  dune runtest --root . test/serlib
+  dune runtest --root . test/compiler
+  # Needed by coq-serapi in CI
+  dune install -p coq-lsp --prefix="$CI_INSTALL_DIR"
 )

dev/ci/ci-serapi.sh

@@ -11,5 +11,8 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/serapi"
   make
+  make test
+  # Not needed by any other CI job for now, but we still install just
+  # in case
   dune install -p coq-serapi --prefix="$CI_INSTALL_DIR"
 )