diff options
| -rw-r--r-- | .circleci/config.yml | 2 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 93 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 2 | ||||
| -rwxr-xr-x | 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 c4b7733a6..892175381 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 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 diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 920100157..689d203a1 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 6daf337a7..307680aa5 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 |