Move to Docker-based CI.

.dockerignore

+.git

.gitlab-ci.yml

-before_script:
-  - . $HOME/.opam/opam-init/variables.sh
+stages:
+  - build
+  - test
+  - deploy
 
-ci-bench:
+.build_template: &build_definition
+  stage: build
   script:
-    - misc/ci-bench.sh
+    - misc/ci-docker.sh misc/ci-local.sh
+
+build:
+  variables:
+    COMPILER: system
+  <<: *build_definition
+
+build-4.03.0:
+  variables:
+    COMPILER: 4.03.0
+  <<: *build_definition
+
+build-4.04.0:
+  variables:
+    COMPILER: 4.04.0
+  <<: *build_definition
+
+build-4.05.0:
+  variables:
+    COMPILER: 4.05.0
+  <<: *build_definition
+
+build-4.06.0:
+  variables:
+    COMPILER: 4.06.0
+  <<: *build_definition
+
+bench:
+  stage: test
+  variables:
+    COMPILER: system
+  script:
+    - misc/ci-docker.sh misc/ci-local.sh bench
+
+.bench_template: &bench_definition
+  stage: test
+  script:
+    - misc/ci-docker.sh misc/ci-local.sh bench
+  only:
+    - tags
+    - schedules
+
+bench-4.03.0:
+  variables:
+    COMPILER: 4.03.0
+  <<: *bench_definition
+
+bench-4.04.0:
+  variables:
+    COMPILER: 4.04.0
+  <<: *bench_definition
+
+bench-4.05.0:
+  variables:
+    COMPILER: 4.05.0
+  <<: *bench_definition
+
+bench-4.06.0:
+  variables:
+    COMPILER: 4.06.0
+  <<: *bench_definition
+
+deploy:
+  stage: deploy
+  script:
+    - autoconf && (automake --add-missing 2> /dev/null || true)
+    - docker build -t bench-image -f misc/Dockerfile.init .
+    - docker build -t deploy-image -f misc/Dockerfile.deploy .
+    - docker login -u gitlab-ci-token -p $CI_JOB_TOKEN $CI_REGISTRY
+    - docker tag deploy-image $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
+    - docker push $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
+    - docker image prune -f
+  only:
+    - master
+    - /^bugfix[/]v[0-9.]*$/
+    - tags

misc/Dockerfile.deploy

+FROM bench-image
+
+USER root
+
+RUN adduser --disabled-password --gecos '' guest
+
+USER why3
+
+COPY --chown=why3:why3 . why3
+WORKDIR /home/why3/why3
+
+RUN eval `opam config env` && \
+    ./configure && \
+    make -j2
+
+USER root
+
+RUN make install
+
+USER guest
+ENV HOME /home/guest
+WORKDIR /home/guest
+
+RUN why3 config --detect

misc/Dockerfile.init

+FROM ocaml/ocaml:debian-stable
+
+# install dependencies
+RUN apt-get update && \
+    apt-get install -y wget libgmp-dev gtk+-2.0 libgtksourceview2.0-dev gnome-themes-standard libcanberra-gtk-module opam
+
+# create user
+RUN sudo adduser --disabled-password --gecos '' why3
+USER why3
+ENV HOME /home/why3
+WORKDIR /home/why3
+
+ARG compiler=system
+RUN opam init -a -y -j2 --compiler=$compiler
+RUN opam install -y menhir conf-gtksourceview lablgtk ocamlgraph zarith camlzip
+
+# Alt-Ergo
+RUN opam install alt-ergo.1.30

misc/ci-docker.sh

+#!/bin/bash
+
+set -e -x
+
+autoconf && (automake --add-missing 2> /dev/null || true)
+docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER .
+CID=$(docker create --rm -i -w /home/why3/why3 bench-image-$COMPILER /bin/sh)
+docker start $CID
+docker cp . $CID:/home/why3/why3
+docker exec -u root $CID chown -R why3:why3 /home/why3/why3
+docker attach $CID <<EOF
+exec $@
+EOF

misc/ci-bench.sh → misc/ci-local.sh

 #!/bin/bash
 
-# runner:
-# apt-get install curl opam automake libgmp-dev zlib1g-dev
+# Runner installation
+# -------------------
+# apt-get install curl autoconf automake
 # curl -L https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh | bash
-# apt-get install gitlab-runner
+# curl -fsSL https://download.docker.com/linux/debian/gpg | apt-key add -
+# apt-key fingerprint 0EBFCD88
+# echo "deb https://download.docker.com/linux/debian stretch stable" >> /etc/apt/sources.list
+# apt-get update
+# apt-get install gitlab-runner docker-ce
 # gitlab-runner register
 #   https://gitlab.inria.fr/
 #   shell
-# su gitlab-runner
-# cd
-# opam init
-# opam install menhir alt-ergo
+# usermod -aG docker gitlab-runner
 
 set -e
+eval `opam config env`
 
-# configuration
-autoconf
-automake --add-missing 2> /dev/null || true
 ./configure --enable-local
-
-# compilation
 make -j2
 
-# detection of provers
+if test "$1" = bench; then
 bin/why3config --detect-provers
-
-# run the bench
 make bench
+fi