[gitlab] Add bleeding-edge flambda build.

We also introduce a bit more systematic job naming: `base/edge`.

In order to make the flambda switch selectable we update the Docker
image so all the dependencies are installed in that one.

Note the extra quote rule for the flambda parameters, but unless we
can assign arrays to Gitlab variables there is not a good way to do
this I'm afraid.

With this patch we are getting close to being able to remove most
builds from Travis.

4 files changed, 64 insertions, 35 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index c4b7733a65..8921753814 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -8,7 +8,7 @@ defaults:
     # reference syntax)
     working_directory: ~/coq
     docker:
-      - image: coqci/base:V2018-05-07
+      - image: coqci/base:V2018-05-07-V2
 
   environment: &envvars
     NATIVE_COMP: "yes"
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78850fa5ee..1c4346bede 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,4 +1,4 @@
-image: coqci/base:V2018-05-07
+image: coqci/base:V2018-05-07-V2
 
 stages:
   - build
@@ -8,7 +8,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: bionic_coq-V2018-05-03
+  CACHEKEY: bionic_coq-V2018-05-07-V2
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
   # Used to select special compiler switches such as flambda, 32bits, etc...
@@ -19,7 +19,7 @@ before_script:
   - ls -a # figure out if artifacts are around
   - printenv | sort
   - declare -A switch_table
-  - switch_table=( ["base"]="$COMPILER" ["be"]="$COMPILER_BE" )
+  - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_BE" )
   - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
   - eval $(opam config env)
   - opam list
@@ -43,7 +43,7 @@ before_script:
     - set -e
 
     - echo 'start:coq.config'
-    - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF}
+    - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
@@ -67,7 +67,7 @@ before_script:
     - set -e
 
     - echo 'start:coq.config'
-    - ./configure -local ${EXTRA_CONF}
+    - ./configure -local ${COQ_EXTRA_CONF}
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
@@ -76,7 +76,7 @@ before_script:
 
     - set +e
   variables: &warnings-variables
-    EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"
 
 # every non build job must set dependencies otherwise all build
 # artifacts are used together and we may get some random Coq. To that
@@ -121,29 +121,37 @@ before_script:
     - echo 'end:coq.test'
     - set +e
   dependencies:
-    - build
+    - build:base
   variables: &ci-template-vars
     TEST_TARGET: "$CI_JOB_NAME"
 
-build:
+build:base:
   <<: *build-template
   variables:
-    EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
 
 # no coqide for 32bit: libgtk installation problems
-build:32bit:
+build:base+32bit:
   <<: *build-template
   variables:
     OPAM_VARIANT: "+32bit"
-    EXTRA_CONF: "-native-compiler yes"
+    COQ_EXTRA_CONF: "-native-compiler yes"
 
-build:bleeding-edge:
+build:edge:
   <<: *build-template
   variables:
-    OPAM_SWITCH: be
-    EXTRA_CONF: "-native-compiler yes -coqide opt"
+    OPAM_SWITCH: edge
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
 
-warnings:
+build:edge+flambda:
+  <<: *build-template
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+    COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts "
+    COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures"
+
+warnings:base:
   <<: *warnings-template
 
 # warnings:32bit:
@@ -151,42 +159,65 @@ warnings:
 #   variables:
 #     <<: *warnings-variables
 
-warnings:bleeding-edge:
+warnings:edge:
   <<: *warnings-template
   variables:
-    OPAM_SWITCH: be
+    OPAM_SWITCH: edge
 
-test-suite:
+test-suite:base:
   <<: *test-suite-template
   dependencies:
-    - build
+    - build:base
 
-test-suite:32bit:
+test-suite:base+32bit:
   <<: *test-suite-template
   dependencies:
-    - build:32bit
+    - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
 
-test-suite:bleeding-edge:
+test-suite:edge:
+  <<: *test-suite-template
+  dependencies:
+    - build:edge
+  variables:
+    OPAM_SWITCH: edge
+
+test-suite:edge+flambda:
   <<: *test-suite-template
   dependencies:
-    - build:bleeding-edge
+    - build:edge+flambda
   variables:
-    OPAM_SWITCH: be
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
 
-validate:
+validate:base:
   <<: *validate-template
   dependencies:
-    - build
+    - build:base
 
-validate:32bit:
+validate:base+32bit:
   <<: *validate-template
   dependencies:
-    - build:32bit
+    - build:base+32bit
   variables:
     OPAM_VARIANT: "+32bit"
 
+validate:edge:
+  <<: *validate-template
+  dependencies:
+    - build:edge
+  variables:
+    OPAM_SWITCH: edge
+
+validate:edge+flambda:
+  <<: *validate-template
+  dependencies:
+    - build:edge+flambda
+  variables:
+    OPAM_SWITCH: edge
+    OPAM_VARIANT: "+flambda"
+
 ci-bignums:
   <<: *ci-template
 
@@ -211,10 +242,8 @@ ci-equations:
 ci-fcsl-pcm:
   <<: *ci-template
 
-# ci-fiat-crypto:
-#   <<: *ci-template
-#   # out of memory error
-#   allow_failure: true
+ci-fiat-crypto:
+  <<: *ci-template
 
 ci-fiat-parsers:
   <<: *ci-template
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 9201001574..689d203a16 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -43,4 +43,4 @@ RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
 
 # BE+flambda switch
 RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
-    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
index 6daf337a72..307680aa51 100755
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 
-COQCI_VERSION=V2018-05-07
+COQCI_VERSION=V2018-05-07-V2
 docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
 docker push $DOCKER_REPO:$COQCI_VERSION