Test the IDE and doc compilation during CI

.gitlab-ci.yml

@@ -38,12 +38,12 @@ bench:
   variables:
     COMPILER: system
   script:
-    - misc/ci-docker.sh misc/ci-local.sh bench
+    - misc/ci-docker.sh misc/ci-local.sh bench ide
 
 .bench_template: &bench_definition
   stage: test
   script:
-    - misc/ci-docker.sh misc/ci-local.sh bench
+    - misc/ci-docker.sh misc/ci-local.sh bench ide
   only:
     - tags
     - schedules
@@ -72,9 +72,10 @@ full:
   stage: test
   variables:
     COMPILER: system
-    PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx
+    DEBIAN_PACKAGES: hevea rubber texlive-latex-extra
+    OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx
   script:
-    - misc/ci-docker.sh misc/ci-local.sh bench
+    - misc/ci-docker.sh misc/ci-local.sh bench ide doc
 
 opam:
   stage: build

misc/Dockerfile.init

 FROM ocaml/ocaml:debian-stable
 
 # install dependencies
+ARG debian_packages
 RUN apt-get update && \
-    apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam
+    apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam xvfb $debian_packages
 
 # create user
 RUN sudo adduser --disabled-password --gecos '' why3
@@ -14,5 +15,5 @@ ARG compiler=system
 RUN opam init -a -y -j1 --compiler=$compiler
 RUN opam repository add coq-released https://coq.inria.fr/opam/released
 
-ARG packages
-RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $packages
+ARG opam_packages
+RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip alt-ergo $opam_packages

misc/ci-docker.sh

@@ -3,12 +3,12 @@
 set -e
 
 autoconf && (automake --add-missing 2> /dev/null || true)
-if test -n "$PACKAGES"; then
-  IMAGE=bench-image-$COMPILER--$(echo $PACKAGES | sed -e 's/ /--/g')
+if test -n "$DEBIAN_PACKAGES" -o -n "$OPAM_PACKAGES"; then
+  IMAGE=bench-image-$COMPILER--$(echo $DEBIAN_PACKAGES | sed -e 's/ /--/g')--$(echo $OPAM_PACKAGES | sed -e 's/ /--/g')
 else
   IMAGE=bench-image-$COMPILER
 fi
-docker build -t $IMAGE -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg packages="$PACKAGES" .
+docker build -t $IMAGE -f misc/Dockerfile.init --build-arg compiler=$COMPILER --build-arg debian_packages="$DEBIAN_PACKAGES" --build-arg opam_packages="$OPAM_PACKAGES" .
 CID=$(docker create --rm -i -w /home/why3/why3 $IMAGE /bin/sh)
 docker start $CID
 docker cp . $CID:/home/why3/why3

misc/ci-local.sh

@@ -21,7 +21,19 @@ eval `opam config env`
 ./configure --enable-local
 make
 
-if test "$1" = bench; then
+while test $# -gt 0
+do
+    case "$1" in
+        bench)
             bin/why3config --detect-provers
             make bench
-fi
+            ;;
+        ide)
+            WHY3CONFIG="" xvfb-run bin/why3 ide --batch "" examples/logic/einstein.why
+            ;;
+        doc)
+            make doc
+            ;;
+    esac
+    shift
+done