Merge PR rocq-prover#19829: [ci] Remove SerAPI from CI.

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

Author: coqbot-app[bot]

.gitlab-ci.yml

@@ -1026,13 +1026,6 @@ library:ci-rupicola:
 plugin:ci-coq_lsp:
   extends: .ci-template-flambda
 
-plugin:ci-serapi:
-  extends: .ci-template-flambda
-  needs:
-  - build:edge+flambda
-  - plugin:ci-coq_lsp
-  stage: build-2
-
 plugin:ci-vscoq:
   extends: .ci-template-flambda
 

Makefile.ci

@@ -86,8 +86,6 @@ CI_TARGETS= \
     ci-rewriter \
     ci-riscv_coq \
     ci-rupicola \
-    ci-serapi \
-    ci-serapi_test \
     ci-sf \
     ci-simple_io \
     ci-smtcoq \
@@ -179,8 +177,6 @@ ci-compcert: ci-menhir ci-flocq
 
 ci-relation_algebra: ci-aac_tactics ci-mathcomp
 
-ci-serapi: ci-coq_lsp
-
 ci-smtcoq_trakt: ci-trakt
 
 # Virtual targets used by the CI to group compilation of rules in a single job

dev/ci/ci-basic-overlay.sh

@@ -504,12 +504,6 @@ project jasmin "https://github.com/jasmin-lang/jasmin" "main"
 project lean_importer "https://github.com/SkySkimmer/coq-lean-import" "master"
 # Contact @SkySkimmer on github
 
-########################################################################
-# SerAPI
-########################################################################
-project serapi "https://github.com/ejgallego/coq-serapi" "main"
-# Contact @ejgallego on github
-
 ########################################################################
 # SMTCoq
 ########################################################################

dev/ci/ci-coq_lsp.sh

@@ -15,6 +15,6 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
   _build/install/default/bin/coq-lsp --version
   dune runtest --root . test/serlib
   dune runtest --root . test/compiler
-  # Needed by coq-serapi in CI
+  # It was needed by coq-serapi in CI, we keep it for now
   dune install -p coq-lsp --prefix="$CI_INSTALL_DIR"
 )