From f3f24b40995b4f98f6f3830d5b9be1714be56b6b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 3 Jun 2024 19:01:28 +0200
Subject: [PATCH] [ci] Switch dependencies serapi <-> coq_lsp

Now serapi depends on coq_lsp, also serapi tests have been moved
there.

To coordinate with the merge of
https://github.com/ejgallego/coq-serapi/pull/409
---
 .gitlab-ci.yml           | 15 +++------------
 Makefile.ci              |  4 +---
 dev/ci/ci-coq_lsp.sh     |  5 +++++
 dev/ci/ci-serapi.sh      |  3 +++
 dev/ci/ci-serapi_test.sh | 12 ------------
 5 files changed, 12 insertions(+), 27 deletions(-)
 delete mode 100644 dev/ci/ci-serapi_test.sh

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 014401eb06f7..9ab4a0fde079 100644
--- a/.gitlab-ci.yml
+++ b/.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:
diff --git a/Makefile.ci b/Makefile.ci
index 5589168eb3cc..72f0844ce52c 100644
--- a/Makefile.ci
+++ b/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
 
diff --git a/dev/ci/ci-coq_lsp.sh b/dev/ci/ci-coq_lsp.sh
index dae358265e21..03aee5df90f5 100644
--- a/dev/ci/ci-coq_lsp.sh
+++ b/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"
 )
diff --git a/dev/ci/ci-serapi.sh b/dev/ci/ci-serapi.sh
index 2e1361abafd4..da3146d29b02 100644
--- a/dev/ci/ci-serapi.sh
+++ b/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"
 )
diff --git a/dev/ci/ci-serapi_test.sh b/dev/ci/ci-serapi_test.sh
deleted file mode 100644
index a770f4e34baf..000000000000
--- a/dev/ci/ci-serapi_test.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
-
-( cd "${CI_BUILD_DIR}/serapi"
-  make test
-)