diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f674a0191ef5..192c359703c5 100644 --- a/.gitlab-ci.yml +++ b/.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 diff --git a/Makefile.ci b/Makefile.ci index 368c9f8bdaf5..15b0a19dc2ce 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -81,6 +81,7 @@ CI_TARGETS= \ ci-unimath \ ci-unicoq \ ci-verdi_raft \ + ci-vscoq \ ci-vst .PHONY: ci-all $(CI_TARGETS) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 50f1948245b8..5680d392748b 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/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 ######################################################################## diff --git a/dev/ci/ci-vscoq.sh b/dev/ci/ci-vscoq.sh new file mode 100644 index 000000000000..9df1755a82d5 --- /dev/null +++ b/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 . +) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8b7ca1741062..a86f511746ee 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/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