From ca5aaa579d9fe87e999f543db0dcb66d2b78032c Mon Sep 17 00:00:00 2001
From: whonore
Date: Mon, 20 Jul 2020 14:35:49 -0400
Subject: Add Coqtail to CI

---
 .gitlab-ci.yml                      | 5 ++++-
 Makefile.ci                         | 1 +
 dev/ci/ci-basic-overlay.sh          | 7 +++++++
 dev/ci/ci-coqtail.sh                | 8 ++++++++
 dev/ci/docker/bionic_coq/Dockerfile | 7 ++++---
 5 files changed, 24 insertions(+), 4 deletions(-)
 create mode 100755 dev/ci/ci-coqtail.sh

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ec8fe23171..32b05ec746 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-05-24-V1"
+  CACHEKEY: "bionic_coq-V2020-07-21-V38"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -726,6 +726,9 @@ library:ci-coqprime:
   - build:edge+flambda
   - plugin:ci-bignums
 
+library:ci-coqtail:
+  extends: .ci-template
+
 library:ci-coquelicot:
   extends: .ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index 77d8bda671..85e4b965f9 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS= \
     ci-color \
     ci-compcert \
     ci-coq_dpdgraph \
+    ci-coqtail \
     ci-coquelicot \
     ci-corn \
     ci-cross_crypto \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4973cbb478..2725e6b56c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -380,3 +380,10 @@
 : "${sf_CI_REF:=master}"
 : "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
 : "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
+
+########################################################################
+# Coqtail
+########################################################################
+: "${coqtail_CI_REF:=master}"
+: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}"
+: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh
new file mode 100755
index 0000000000..b8b5c6c724
--- /dev/null
+++ b/dev/ci/ci-coqtail.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coqtail
+
+( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8c5696f4f9..7570b17095 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-24-V1"
+# CACHEKEY: "bionic_coq-V2020-07-21-V38"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -17,9 +17,10 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of source-doc and coq-makefile
         texlive-science tipa
 
-# More dependencies of the sphinx doc
+# More dependencies of the sphinx doc, pytest for coqtail
 RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
-                 antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2
+        antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \
+        pytest==5.4.3
 
 # We need to install OPAM 2.0 manually for now.
 RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
-- 
cgit v1.2.3