From cde263581c49a75f8abdbcb398511942906e6204 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 5 May 2018 19:23:49 +0200 Subject: [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. --- .circleci/config.yml | 2 +- .gitlab-ci.yml | 93 +++++++++++++++++++++----------- dev/ci/docker/bionic_coq/Dockerfile | 2 +- dev/ci/docker/bionic_coq/hooks/post_push | 2 +- 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 -- cgit v1.2.3