Merge PR rocq-prover#17678: Add back VsCoq in CI

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

Author: coqbot-app[bot]

.gitlab-ci.yml

@@ -35,7 +35,7 @@ variables:
   # $DATE is so we can tell what's what in the image list
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
-  CACHEKEY: "bionic_coq-V2022-02-16-401854eb90"
+  CACHEKEY: "bionic_coq-V2023-06-07-de28eea879"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
 
   # By default, jobs run in the base switch; override to select another switch
@@ -932,6 +932,9 @@ plugin:ci-coq_lsp:
   - build:edge+flambda
   - plugin:ci-serapi
 
+plugin:ci-vscoq:
+  extends: .ci-template-flambda
+
 plugin:ci-smtcoq:
   extends: .ci-template
 

Makefile.ci

@@ -81,6 +81,7 @@ CI_TARGETS= \
     ci-unimath \
     ci-unicoq \
     ci-verdi_raft \
+    ci-vscoq \
     ci-vst
 
 .PHONY: ci-all $(CI_TARGETS)

dev/ci/ci-basic-overlay.sh

@@ -325,6 +325,11 @@ project coqtail "https://github.com/whonore/Coqtail" "master"
 ########################################################################
 project deriving "https://github.com/arthuraa/deriving" "master"
 
+########################################################################
+# VsCoq
+########################################################################
+project vscoq "https://github.com/coq-community/vscoq" "main"
+
 ########################################################################
 # category-theory
 ########################################################################

dev/ci/ci-vscoq.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+set -e
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download vscoq
+
+if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
+
+( cd "$CI_BUILD_DIR/vscoq/language-server"
+  dune build --root . --only-packages=vscoq-language-server @install
+  dune runtest --root .
+)

dev/ci/docker/bionic_coq/Dockerfile

@@ -66,7 +66,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.14.1" \
     BASE_OPAM_EDGE="dune.3.6.1 dune-build-info.3.6.1 dune-release.1.6.2 ocamlfind.1.9.5 odoc.2.1.1" \
-    CI_OPAM_EDGE="elpi.1.16.5 ppx_import.1.10.0 cmdliner.1.1.1 sexplib.v0.15.1 ppx_sexp_conv.v0.15.1 ppx_hash.v0.15.0 ppx_compare.v0.15.0 ppx_deriving_yojson.3.7.0 yojson.1.7.0 uri.4.2.0" \
+    CI_OPAM_EDGE="elpi.1.16.5 ppx_import.1.10.0 cmdliner.1.1.1 sexplib.v0.15.1 ppx_sexp_conv.v0.15.1 ppx_hash.v0.15.0 ppx_compare.v0.15.0 ppx_deriving_yojson.3.7.0 yojson.1.7.0 uri.4.2.0 ppx_yojson_conv.v0.15.1 ppx_inline_test.v0.15.1 ppx_assert.v0.15.0" \
     COQIDE_OPAM_EDGE="lablgtk3-sourceview3.3.1.3"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use