[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.

1 files changed, 61 insertions, 32 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 78850fa5e..1c4346bed 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