Remove the init stage and make other stages a bit more generic.

.gitlab-ci.yml

 stages:
-- init
-- build
-- test
-- deploy
+  - build
+  - test
+  - deploy
 
-variables:
-  DEPLOY_TAG: registry.gitlab.inria.fr/why3/why3:latest
-
-init:
-  stage: init
-  script:
-    - docker build -t bench-image -f misc/Dockerfile.init .
-
-.init_template: &init_definition
-  stage: init
+.build_template: &build_definition
+  stage: build
   script:
     - docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER .
-
-init-4.03.0:
-  variables:
-    COMPILER: 4.03.0
-  <<: *init_definition
-
-init-4.04.0:
-  variables:
-    COMPILER: 4.04.0
-  <<: *init_definition
-
-init-4.05.0:
-  variables:
-    COMPILER: 4.05.0
-  <<: *init_definition
-
-init-4.06.0:
-  variables:
-    COMPILER: 4.06.0
-  <<: *init_definition
+    - docker run -t --rm bench-image-$COMPILER misc/ci-local.sh
 
 build:
-  stage: build
-  script:
-    - docker run -t --rm bench-image misc/build.sh
-
-.build_template: &build_definition
-  stage: build
-  script:
-    - docker run -t --rm bench-image-$COMPILER misc/build.sh
+  variables:
+    COMPILER: system
+  <<: *build_definition
 
 build-4.03.0:
   variables:
@@ -69,13 +36,17 @@ build-4.06.0:
 
 bench:
   stage: test
+  variables:
+    COMPILER: system
   script:
-    - docker run -t --rm bench-image misc/ci-bench.sh
+    - docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER .
+    - docker run -t --rm bench-image-$COMPILER misc/ci-local.sh bench
 
 .bench_template: &bench_definition
   stage: test
   script:
-    - docker run -t --rm bench-image-$COMPILER misc/ci-bench.sh
+    - docker build -t bench-image-$COMPILER -f misc/Dockerfile.init --build-arg compiler=$COMPILER .
+    - docker run -t --rm bench-image-$COMPILER misc/ci-local.sh bench
   only:
     - tags
     - schedules
@@ -103,9 +74,9 @@ bench-4.06.0:
 deploy:
   stage: deploy
   script:
-    - docker login -u gitlab-ci-token -p $CI_JOB_TOKEN registry.gitlab.inria.fr
+    - docker login -u gitlab-ci-token -p $CI_JOB_TOKEN $CI_REGISTRY
     - docker build -t deploy-image -f misc/Dockerfile.deploy .
-    - docker tag deploy-image $DEPLOY_TAG
-    - docker push $DEPLOY_TAG
+    - docker tag deploy-image $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
+    - docker push $CI_REGISTRY_IMAGE:$CI_COMMIT_REF_SLUG
   only:
-    - master
\ No newline at end of file
+    - master

misc/build.sh

-#!/bin/bash
-
-set -e
-eval `opam config env`
-
-# configuration
-autoconf
-automake --add-missing 2> /dev/null || true
-./configure --enable-local
-
-# compilation
-make -j2

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

@@ -25,8 +25,12 @@ automake --add-missing 2> /dev/null || true
 # compilation
 make -j2
 
+if test "$1" = bench; then
+
 # detection of provers
 bin/why3config --detect-provers
 
 # run the bench
 make bench
+
+fi