Merge PR #13472: [ci] Add job for gappa

Reviewed-by: SkySkimmer
Ack-by: ejgallego

4 files changed, 27 insertions, 1 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index bd015a40b6..af54edfa21 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE-$hash
   # The $hash is the first 10 characters of the md5 of the dockerfile
-  CACHEKEY: "bionic_coq-V2020-11-26-db194d584e"
+  CACHEKEY: "bionic_coq-V2020-11-26-50e9456f22"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -847,6 +847,16 @@ library:ci-corn:
   - build:edge+flambda
   - library:ci-math_classes
 
+plugin:ci-gappa:
+  extends: .ci-template-flambda
+  stage: stage-3
+  needs:
+  - build:edge+flambda
+  - library:ci-flocq
+  dependencies:
+  - build:edge+flambda
+  - library:ci-flocq
+
 library:ci-geocoq:
   extends: .ci-template-flambda
 
diff --git a/Makefile.ci b/Makefile.ci
index 9f08de662f..d549ed1b39 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -35,6 +35,7 @@ CI_TARGETS= \
     ci-fiat_parsers \
     ci-flocq \
     ci-fourcolor \
+    ci-gappa \
     ci-geocoq \
     ci-coqhammer \
     ci-hott \
@@ -94,6 +95,7 @@ ci-metacoq: ci-equations
 ci-vst: ci-flocq
 
 ci-compcert: ci-menhir ci-flocq
+ci-gappa: ci-flocq
 
 # Generic rule, we use make to ease CI integration
 $(CI_TARGETS): ci-%:
diff --git a/dev/ci/ci-gappa.sh b/dev/ci/ci-gappa.sh
new file mode 100755
index 0000000000..c346354b70
--- /dev/null
+++ b/dev/ci/ci-gappa.sh
@@ -0,0 +1,12 @@
+ #!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download gappa_tool
+
+( cd "${CI_BUILD_DIR}/gappa_tool" && ( if [ ! -x ./configure ]; then autoreconf && touch stamp-config_h.in && ./configure --prefix=${CI_INSTALL_DIR}; fi ) && ./remake "-j${NJOBS}" && ./remake install )
+
+git_download gappa_plugin
+
+( cd "${CI_BUILD_DIR}/gappa_plugin" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 96d96328f8..1aefebb007 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -15,6 +15,8 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         perl libgmp-dev libgmp-dev:i386 \
         # Dependencies of lablgtk (for CoqIDE)
         libgtksourceview-3.0-dev \
+        # Dependencies of Gappa
+        libboost1.65-all-dev libmpfr-dev autoconf-archive bison flex \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \