From e5922809138d45fb29677577c7f8822875b5b67b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 8 Dec 2017 20:00:22 +0100 Subject: CI: poc Circleci configuration Revert "CI: poc Circleci configuration" Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34. CI: poc Circleci configuration Fixup Try minimising build for faster testing Various fixes Fixup: yaml identation Do not -j2: native compiler seems to take too much memory Revert "Do not -j2: native compiler seems to take too much memory" This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372. Deactivate native compiler Fixup (how did this happen?) Do not call time (not install on docker images, will fix later) Fixup Fixup --- .circleci/config.yml | 143 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 143 insertions(+) create mode 100644 .circleci/config.yml (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml new file mode 100644 index 000000000..cb195f212 --- /dev/null +++ b/.circleci/config.yml @@ -0,0 +1,143 @@ +defaults: + params: + # Following parameters are used in Coq CircleCI Job (using yaml + # reference syntax) + working_directory: &workdir ~/coq + base_image: &base ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda + + # Job configuration + config: &coq + working_directory: *workdir + docker: + - image: *base + environment: + # required by some of the targets, e.g. compcert, passed for + # instance to opam to configure the number of parallel jobs + # allowed + - NJOBS: 2 + +version: 2 + +# Defines individual jobs, see the workflows section below for job orchestration +jobs: + # TODO: linter + + # Build and prepare test environment + build: + <<: *coq + steps: + - checkout + # Restore last version of the dependencies in cache When a new + # major version of caches has to be generated, please use + # vYYMMDD format to avoid collision. + - restore_cache: + key: coq-opam-cache-{{ arch }}-v171208- + - run: + name: Build opam dependencies + command: | + # workaround, ought to be fixed in recent opams. See + # https://github.com/ocaml/opam/issues/2978 + export TERM=xterm + opam install -y camlp5 ocamlfind + - save_cache: + key: coq-opam-cache-{{ arch }}-v171208-static-deps + paths: + - ~/.opam + - run: + name: Configure + command: | + # XXX: all this .profile stuff is a shortcoming of the + # docker image. To be improved. + . ~/.profile + ./configure -local -native-compiler no + - run: + name: Build + command: | + . ~/.profile + make -j2 + - run: + name: Validate + command: | + . ~/.profile + make -j2 validate + - persist_to_workspace: + root: &workspace ~/ + paths: + - .opam + - coq/ + + bignums: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: System dependencies + command: | + sudo apt-get update + sudo apt-get install -y python + - run: + name: Build + command: | + . ~/.profile + make -j2 ci-bignums + # bignums is a dependency + - persist_to_workspace: + root: &workspace ~/ + paths: + - coq/ + + color: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: System dependencies + command: | + sudo apt-get update + sudo apt-get install -y python + - run: + name: Build + command: | + . ~/.profile + make -j2 ci-color + + compcert: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: System dependencies + command: | + sudo apt-get update + sudo apt-get install -y python + - run: + name: Build + command: | + . ~/.profile + make -j2 ci-compcert + +workflows: + version: 2 + # Run on each push + ci: + jobs: + - build + - bignums: + requires: + - build + - color: + requires: + - build + - bignums + - compcert: + requires: + - build -- cgit v1.2.3 From 8323ac57d63d3734c5f43b787c97644bf2fce32d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 11 Dec 2017 15:43:34 +0100 Subject: Near-full implementation of Circle CI. VS gitlab: + fiat-crypto (Circle has 4GB RAM, gitlab 2GB) - caching opam (TODO) - publishing artefacts (TODO) * tests with -local, not installed VS travis: + reusing build products - flambda validate job (TODO?) - OSX jobs (TODO at least check if free OSX is possible) - linter (TODO?) --- .circleci/config.yml | 475 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 354 insertions(+), 121 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index cb195f212..42df67e71 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -1,143 +1,376 @@ defaults: - params: + params: ¶ms # Following parameters are used in Coq CircleCI Job (using yaml # reference syntax) - working_directory: &workdir ~/coq - base_image: &base ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda - - # Job configuration - config: &coq - working_directory: *workdir + working_directory: ~/coq docker: - - image: *base - environment: - # required by some of the targets, e.g. compcert, passed for - # instance to opam to configure the number of parallel jobs - # allowed - - NJOBS: 2 + - image: ocaml/opam:ubuntu + + environment: &envvars + # required by some of the targets, e.g. compcert, passed for + # instance to opam to configure the number of parallel jobs + # allowed + NJOBS: 2 + COMPILER: "system" + CAMLP5_VER: "6.14" + + # some useful values + COMPILER_32BIT: &compiler-32bit "4.02.3+32bit" + + COMPILER_BLEEDING_EDGE: &compiler-be "4.06.0" + CAMLP5_VER_BLEEDING_EDGE: &camlp5-ver-be "7.03" + + TIMING_PACKAGES: &timing-packages "time python" + + COQIDE_PACKAGES: &coqide-packages "libgtk2.0-dev libgtksourceview2.0-dev" + #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" + COQIDE_OPAM: &coqide-opam "lablgtk-extras" + COQIDE_OPAM_BE: &coqide-opam-be "num lablgtk.2.18.6 lablgtk-extras.1.6" + COQDOC_PACKAGES: &coqdoc-packages "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa" + COQDOC_OPAM: &coqdoc-opam "hevea" version: 2 +before_script: &before_script + name: before_script + command: | + source ~/.profile + export TERM=xterm + ls # figure out if artifacts are around + printenv + #if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi + if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi + + # the default repo in this docker image is a local directory + # at the time of 4aaeb8abf it lagged behind the official + # repository such that camlp5 7.01 was not available + opam repository set-url default https://opam.ocaml.org + opam update + opam switch ${COMPILER} + eval $(opam config env) + opam config list + opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} + rm -rf ~/.opam/log/ + opam list + +.build-template: &build-template + <<: *params + steps: + - checkout + # - restore_cache: + # key: coq-opam-cache-{{ arch }}-v171208- + - run: *before_script + # - save_cache: + # key: coq-opam-cache-{{ arch }}-v171208-static-deps + # paths: + # - ~/.opam + - run: &build-configure + name: Configure + command: | + source ~/.profile + + echo 'start:coq.config' + ./configure -local -native-compiler no ${EXTRA_CONF} + echo 'end:coq.config' + - run: &build-build + name: Build + command: | + source ~/.profile + echo 'start:coq.build' + make -j ${NJOBS} byte + make -j ${NJOBS} + make test-suite/misc/universes/all_stdlib.v + echo 'end:coq:build' + - persist_to_workspace: + root: &workspace ~/ + paths: + - .opam + - coq/ + + environment: &build-variables + <<: *envvars + EXTRA_CONF: "-coqide opt" + EXTRA_PACKAGES: *coqide-packages + EXTRA_OPAM: *coqide-opam + +.validate-template: &validate-template + <<: *params + steps: + - checkout + - attach_workspace: + at: *workspace + - run: *before_script + - run: + name: Validate + command: | + source ~/.profile + make validate + environment: *envvars + +.documentation-template: &documentation-template + <<: *params + steps: + - checkout + - attach_workspace: + at: *workspace + - run: *before_script + - run: + name: Documentation + command: | + source ~/.profile + make -j ${NJOBS} doc + environment: &documentation-variables + <<: *envvars + EXTRA_PACKAGES: *coqdoc-packages + EXTRA_OPAM: *coqdoc-opam + +.test-suite-template: &test-suite-template + <<: *params + steps: + - checkout + - attach_workspace: + at: *workspace + - run: *before_script + - run: + name: Test + command: | + source ~/.profile + cd test-suite + make clean + make -j ${NJOBS} all + environment: &test-suite-variables + <<: *envvars + EXTRA_PACKAGES: *timing-packages + +.warnings-template: &warnings-template + <<: *params + steps: + - checkout + - run: *before_script + - run: + name: Configure + command: | + source ~/.profile + ./configure -local ${EXTRA_CONF} + + - run: + name: Build + command: | + source ~/.profile + make -j ${NJOBS} coqocaml + environment: &warnings-variables + <<: *envvars + EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + EXTRA_PACKAGES: *coqide-packages + EXTRA_OPAM: *coqide-opam + +.ci-template: &ci-template + <<: *params + steps: + - checkout + - attach_workspace: + at: *workspace + - run: *before_script + - run: + name: Test + command: | + source ~/.profile + echo 'start:coq.test' + make -f Makefile.ci -j ${NJOBS} ${CIRCLE_JOB} + echo 'end:coq.test' + environment: &ci-template-vars + <<: *envvars + EXTRA_PACKAGES: *timing-packages + # Defines individual jobs, see the workflows section below for job orchestration jobs: # TODO: linter # Build and prepare test environment - build: - <<: *coq - steps: - - checkout - # Restore last version of the dependencies in cache When a new - # major version of caches has to be generated, please use - # vYYMMDD format to avoid collision. - - restore_cache: - key: coq-opam-cache-{{ arch }}-v171208- - - run: - name: Build opam dependencies - command: | - # workaround, ought to be fixed in recent opams. See - # https://github.com/ocaml/opam/issues/2978 - export TERM=xterm - opam install -y camlp5 ocamlfind - - save_cache: - key: coq-opam-cache-{{ arch }}-v171208-static-deps - paths: - - ~/.opam - - run: - name: Configure - command: | - # XXX: all this .profile stuff is a shortcoming of the - # docker image. To be improved. - . ~/.profile - ./configure -local -native-compiler no - - run: - name: Build - command: | - . ~/.profile - make -j2 - - run: - name: Validate - command: | - . ~/.profile - make -j2 validate - - persist_to_workspace: - root: &workspace ~/ - paths: - - .opam - - coq/ - - bignums: - <<: *coq - steps: - # Restore workspace - - checkout - - attach_workspace: - at: *workspace - - run: - name: System dependencies - command: | - sudo apt-get update - sudo apt-get install -y python - - run: - name: Build - command: | - . ~/.profile - make -j2 ci-bignums - # bignums is a dependency - - persist_to_workspace: - root: &workspace ~/ - paths: - - coq/ - - color: - <<: *coq - steps: - # Restore workspace - - checkout - - attach_workspace: - at: *workspace - - run: - name: System dependencies - command: | - sudo apt-get update - sudo apt-get install -y python - - run: - name: Build - command: | - . ~/.profile - make -j2 ci-color - - compcert: - <<: *coq - steps: - # Restore workspace - - checkout - - attach_workspace: - at: *workspace - - run: - name: System dependencies - command: | - sudo apt-get update - sudo apt-get install -y python - - run: - name: Build - command: | - . ~/.profile - make -j2 ci-compcert + build: *build-template + + build-32bit: + <<: *build-template + environment: + <<: *envvars # no coqide for 32bit + EXTRA_PACKAGES: "gcc-multilib" + COMPILER: *compiler-32bit + + build-be: + <<: *build-template + environment: + <<: *build-variables + COMPILER: *compiler-be + CAMLP5_VER: *camlp5-ver-be + EXTRA_OPAM: *coqide-opam-be + + validate: *validate-template + + validate-32bit: + <<: *validate-template + environment: + <<: *envvars + COMPILER: *compiler-32bit + EXTRA_PACKAGES: "gcc-multilib" + + warnings: *warnings-template + + warnings-be: + <<: *warnings-template + environment: + <<: *warnings-variables + COMPILER: *compiler-be + CAMLP5_VER: *camlp5-ver-be + EXTRA_OPAM: *coqide-opam-be + + documentation: *documentation-template + + documentation-be: + <<: *documentation-template + environment: + <<: *documentation-variables + COMPILER: *compiler-be + CAMLP5_VER: *camlp5-ver-be + + test-suite: + <<: *test-suite-template + + test-suite-32bit: + <<: *test-suite-template + environment: + <<: *test-suite-variables + COMPILER: *compiler-32bit + EXTRA_PACKAGES: "gcc-multilib time python" + + test-suite-be: + <<: *test-suite-template + environment: + <<: *test-suite-variables + COMPILER: *compiler-be + CAMLP5_VER: *camlp5-ver-be + EXTRA_PACKAGES: *timing-packages + + ci-bignums: + <<: *ci-template + + ci-color: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: *timing-packages + + ci-compcert: + <<: *ci-template + + ci-coq-dpdgraph: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_OPAM: "ocamlgraph" + EXTRA_PACKAGES: "time python autoconf automake" + + ci-coquelicot: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: "time python autoconf automake" + + ci-equations: + <<: *ci-template + + ci-geocoq: + <<: *ci-template + + ci-fiat-crypto: + <<: *ci-template + + ci-fiat-parsers: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: *timing-packages + + ci-flocq: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: "time python autoconf automake" + + ci-formal-topology: + <<: *ci-template + + ci-hott: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: "time python autoconf automake" + + ci-iris-lambda-rust: + <<: *ci-template + + ci-ltac2: + <<: *ci-template + + ci-math-comp: + <<: *ci-template + + ci-sf: + <<: *ci-template + environment: + <<: *ci-template-vars + EXTRA_PACKAGES: "time python wget" + + ci-unimath: + <<: *ci-template + + ci-vst: + <<: *ci-template workflows: version: 2 # Run on each push - ci: + main: jobs: - build - - bignums: + - warnings + - validate: &req-main requires: - build - - color: + - test-suite: *req-main + - documentation: *req-main + + - ci-bignums: *req-main + - ci-color: *req-main + - ci-compcert: *req-main + - ci-coq-dpdgraph: *req-main + - ci-coquelicot: *req-main + - ci-equations: *req-main + - ci-geocoq: *req-main + - ci-fiat-crypto: *req-main + - ci-fiat-parsers: *req-main + - ci-flocq: *req-main + - ci-formal-topology: *req-main + - ci-hott: *req-main + - ci-iris-lambda-rust: *req-main + - ci-ltac2: *req-main + - ci-math-comp: *req-main + - ci-sf: *req-main + - ci-unimath: *req-main + - ci-vst: *req-main + + # 32bit: + # jobs: + - build-32bit + - validate-32bit: &req-32bit requires: - - build - - bignums - - compcert: + - build-32bit + - test-suite-32bit: *req-32bit + + # bleeding-edge: + # jobs: + - build-be + - warnings-be + - test-suite-be: &req-be requires: - - build + - build-be + - documentation-be: *req-be -- cgit v1.2.3 From c2b7b15526f0c8b87b9442567ddfa0e133cfebcf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 13:26:59 +0100 Subject: Circle CI: enable native compiler. --- .circleci/config.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index 42df67e71..fecabd7bc 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -13,6 +13,7 @@ defaults: NJOBS: 2 COMPILER: "system" CAMLP5_VER: "6.14" + NATIVE_COMP: "yes" # some useful values COMPILER_32BIT: &compiler-32bit "4.02.3+32bit" @@ -70,7 +71,7 @@ before_script: &before_script source ~/.profile echo 'start:coq.config' - ./configure -local -native-compiler no ${EXTRA_CONF} + ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} echo 'end:coq.config' - run: &build-build name: Build @@ -151,7 +152,7 @@ before_script: &before_script name: Configure command: | source ~/.profile - ./configure -local ${EXTRA_CONF} + ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - run: name: Build @@ -160,7 +161,7 @@ before_script: &before_script make -j ${NJOBS} coqocaml environment: &warnings-variables <<: *envvars - EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + EXTRA_CONF: "-coqide byte -byte-only" EXTRA_PACKAGES: *coqide-packages EXTRA_OPAM: *coqide-opam -- cgit v1.2.3 From 4d11d6dc3bfcef3ecdf3f905dcf2fdbca259677e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 13:42:59 +0100 Subject: Circle CI: use cache for opam --- .circleci/config.yml | 55 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 48 insertions(+), 7 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index fecabd7bc..7b68a0711 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -58,13 +58,15 @@ before_script: &before_script <<: *params steps: - checkout - # - restore_cache: - # key: coq-opam-cache-{{ arch }}-v171208- + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script - # - save_cache: - # key: coq-opam-cache-{{ arch }}-v171208-static-deps - # paths: - # - ~/.opam + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: &build-configure name: Configure command: | @@ -85,7 +87,6 @@ before_script: &before_script - persist_to_workspace: root: &workspace ~/ paths: - - .opam - coq/ environment: &build-variables @@ -100,7 +101,15 @@ before_script: &before_script - checkout - attach_workspace: at: *workspace + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: name: Validate command: | @@ -114,7 +123,15 @@ before_script: &before_script - checkout - attach_workspace: at: *workspace + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: name: Documentation command: | @@ -131,7 +148,15 @@ before_script: &before_script - checkout - attach_workspace: at: *workspace + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: name: Test command: | @@ -147,7 +172,15 @@ before_script: &before_script <<: *params steps: - checkout + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: name: Configure command: | @@ -171,7 +204,15 @@ before_script: &before_script - checkout - attach_workspace: at: *workspace + - restore_cache: + keys: + - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script + - save_cache: + key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + paths: + - ~/.opam - run: name: Test command: | -- cgit v1.2.3 From cef0430e14c370e6cbfe72db75e61cb4b8c8a8b9 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 15:05:10 +0100 Subject: Circle CI: enable TIMED for external developments --- .circleci/config.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index 7b68a0711..718bd6b5e 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -218,7 +218,7 @@ before_script: &before_script command: | source ~/.profile echo 'start:coq.test' - make -f Makefile.ci -j ${NJOBS} ${CIRCLE_JOB} + make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB} echo 'end:coq.test' environment: &ci-template-vars <<: *envvars -- cgit v1.2.3 From eced3ec17e156a6cf5c96822bc675b353a9b0168 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 15:16:04 +0100 Subject: Circle CI: uses dependencies between external developments. --- .circleci/config.yml | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index 718bd6b5e..437f5cd2e 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -220,7 +220,11 @@ before_script: &before_script echo 'start:coq.test' make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB} echo 'end:coq.test' - environment: &ci-template-vars + - persist_to_workspace: + root: &workspace ~/ + paths: + - coq/ +environment: &ci-template-vars <<: *envvars EXTRA_PACKAGES: *timing-packages @@ -338,6 +342,12 @@ jobs: <<: *ci-template-vars EXTRA_PACKAGES: "time python autoconf automake" + ci-math-classes: + <<: *ci-template + + ci-corn: + <<: *ci-template + ci-formal-topology: <<: *ci-template @@ -382,7 +392,10 @@ workflows: - documentation: *req-main - ci-bignums: *req-main - - ci-color: *req-main + - ci-color: + requires: + - build + - ci-bignums - ci-compcert: *req-main - ci-coq-dpdgraph: *req-main - ci-coquelicot: *req-main @@ -391,7 +404,18 @@ workflows: - ci-fiat-crypto: *req-main - ci-fiat-parsers: *req-main - ci-flocq: *req-main - - ci-formal-topology: *req-main + - ci-math-classes: + requires: + - build + - ci-bignums + - ci-corn: + requires: + - build + - ci-math-classes + - ci-formal-topology: + requires: + - build + - ci-corn - ci-hott: *req-main - ci-iris-lambda-rust: *req-main - ci-ltac2: *req-main -- cgit v1.2.3 From 7fc585a30ee5aaeb3463eb0c5dc317ffcee3ce53 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 17:07:17 +0100 Subject: Circle CI: remove warning jobs --- .circleci/config.yml | 46 ---------------------------------------------- 1 file changed, 46 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index 437f5cd2e..96e935876 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -168,36 +168,6 @@ before_script: &before_script <<: *envvars EXTRA_PACKAGES: *timing-packages -.warnings-template: &warnings-template - <<: *params - steps: - - checkout - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - - run: *before_script - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam - - run: - name: Configure - command: | - source ~/.profile - ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - - - run: - name: Build - command: | - source ~/.profile - make -j ${NJOBS} coqocaml - environment: &warnings-variables - <<: *envvars - EXTRA_CONF: "-coqide byte -byte-only" - EXTRA_PACKAGES: *coqide-packages - EXTRA_OPAM: *coqide-opam - .ci-template: &ci-template <<: *params steps: @@ -259,16 +229,6 @@ jobs: COMPILER: *compiler-32bit EXTRA_PACKAGES: "gcc-multilib" - warnings: *warnings-template - - warnings-be: - <<: *warnings-template - environment: - <<: *warnings-variables - COMPILER: *compiler-be - CAMLP5_VER: *camlp5-ver-be - EXTRA_OPAM: *coqide-opam-be - documentation: *documentation-template documentation-be: @@ -384,7 +344,6 @@ workflows: main: jobs: - build - - warnings - validate: &req-main requires: - build @@ -424,18 +383,13 @@ workflows: - ci-unimath: *req-main - ci-vst: *req-main - # 32bit: - # jobs: - build-32bit - validate-32bit: &req-32bit requires: - build-32bit - test-suite-32bit: *req-32bit - # bleeding-edge: - # jobs: - build-be - - warnings-be - test-suite-be: &req-be requires: - build-be -- cgit v1.2.3 From 81e0ef590172c8eeed7b3c5e5b4290010557dc48 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 13 Dec 2017 17:38:56 +0100 Subject: Circle CI: separate job to boot opam with all used packages. --- .circleci/config.yml | 164 +++++++++++++++++++++++++++------------------------ 1 file changed, 86 insertions(+), 78 deletions(-) (limited to '.circleci') diff --git a/.circleci/config.yml b/.circleci/config.yml index 96e935876..7c250c667 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -33,59 +33,80 @@ defaults: version: 2 before_script: &before_script - name: before_script + name: Install system packages command: | + echo export TERM=xterm >> ~/.profile source ~/.profile - export TERM=xterm - ls # figure out if artifacts are around printenv #if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi - # the default repo in this docker image is a local directory - # at the time of 4aaeb8abf it lagged behind the official - # repository such that camlp5 7.01 was not available - opam repository set-url default https://opam.ocaml.org - opam update +opam-switch: &opam-switch + name: Select opam switch + command: | + source ~/.profile opam switch ${COMPILER} - eval $(opam config env) opam config list - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - rm -rf ~/.opam/log/ opam list -.build-template: &build-template +.opam-boot-template: &opam-boot-template <<: *params steps: - checkout + - run: *before_script - restore_cache: keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - - run: *before_script + - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}- + - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}- # this grabs old cache if checksum doesn't match + - run: + name: Update opam lists + command: | + source ~/.profile + opam repository set-url default https://opam.ocaml.org + opam update + - run: + name: Install opam packages + command: | + source ~/.profile + opam switch -j ${NJOBS} ${COMPILER} + opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${COQIDE_OPAM} ${COQDOC_OPAM} ${EXTRA_OPAM} + - run: + name: Clean cache + command: | + source ~/.profile + rm -rf ~/.opam/log/ - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- + key: coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}- paths: - ~/.opam + - persist_to_workspace: + root: &workspace ~/ + paths: + - .opam/ + +.build-template: &build-template + <<: *params + steps: + - checkout + - run: *before_script + - attach_workspace: &attach_workspace + at: *workspace + - run: *opam-switch - run: &build-configure name: Configure command: | source ~/.profile - echo 'start:coq.config' ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - echo 'end:coq.config' - run: &build-build name: Build command: | source ~/.profile - echo 'start:coq.build' make -j ${NJOBS} byte make -j ${NJOBS} make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - persist_to_workspace: - root: &workspace ~/ + root: *workspace paths: - coq/ @@ -93,23 +114,12 @@ before_script: &before_script <<: *envvars EXTRA_CONF: "-coqide opt" EXTRA_PACKAGES: *coqide-packages - EXTRA_OPAM: *coqide-opam .validate-template: &validate-template <<: *params steps: - - checkout - - attach_workspace: - at: *workspace - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam + - attach_workspace: *attach_workspace - run: name: Validate command: | @@ -120,18 +130,8 @@ before_script: &before_script .documentation-template: &documentation-template <<: *params steps: - - checkout - - attach_workspace: - at: *workspace - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam + - attach_workspace: *attach_workspace - run: name: Documentation command: | @@ -140,23 +140,12 @@ before_script: &before_script environment: &documentation-variables <<: *envvars EXTRA_PACKAGES: *coqdoc-packages - EXTRA_OPAM: *coqdoc-opam .test-suite-template: &test-suite-template <<: *params steps: - - checkout - - attach_workspace: - at: *workspace - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam + - attach_workspace: *attach_workspace - run: name: Test command: | @@ -171,30 +160,18 @@ before_script: &before_script .ci-template: &ci-template <<: *params steps: - - checkout - - attach_workspace: - at: *workspace - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match - run: *before_script - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam + - attach_workspace: *attach_workspace - run: name: Test command: | source ~/.profile - echo 'start:coq.test' make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB} - echo 'end:coq.test' - persist_to_workspace: - root: &workspace ~/ + root: *workspace paths: - coq/ -environment: &ci-template-vars + environment: &ci-template-vars <<: *envvars EXTRA_PACKAGES: *timing-packages @@ -202,6 +179,31 @@ environment: &ci-template-vars jobs: # TODO: linter + opam-boot: + <<: *opam-boot-template + environment: + <<: *envvars + EXTRA_PACKAGES: *coqide-packages + EXTRA_OPAM: "ocamlgraph" + + opam-boot-32bit: + <<: *opam-boot-template + environment: + <<: *envvars + EXTRA_PACKAGES: "gcc-multilib" + COMPILER: *compiler-32bit + COQIDE_OPAM: "" + COQDOC_OPAM: "" + + opam-boot-be: + <<: *opam-boot-template + environment: + <<: *envvars + EXTRA_PACKAGES: *coqide-packages + COMPILER: *compiler-be + CAMLP5_VER: *camlp5-ver-be + COQIDE_OPAM: *coqide-opam-be + # Build and prepare test environment build: *build-template @@ -217,8 +219,6 @@ jobs: environment: <<: *build-variables COMPILER: *compiler-be - CAMLP5_VER: *camlp5-ver-be - EXTRA_OPAM: *coqide-opam-be validate: *validate-template @@ -253,7 +253,6 @@ jobs: environment: <<: *test-suite-variables COMPILER: *compiler-be - CAMLP5_VER: *camlp5-ver-be EXTRA_PACKAGES: *timing-packages ci-bignums: @@ -272,7 +271,6 @@ jobs: <<: *ci-template environment: <<: *ci-template-vars - EXTRA_OPAM: "ocamlgraph" EXTRA_PACKAGES: "time python autoconf automake" ci-coquelicot: @@ -343,7 +341,13 @@ workflows: # Run on each push main: jobs: - - build + - opam-boot + - opam-boot-32bit + - opam-boot-be + + - build: + requires: + - opam-boot - validate: &req-main requires: - build @@ -383,13 +387,17 @@ workflows: - ci-unimath: *req-main - ci-vst: *req-main - - build-32bit + - build-32bit: + requires: + - opam-boot-32bit - validate-32bit: &req-32bit requires: - build-32bit - test-suite-32bit: *req-32bit - - build-be + - build-be: + requires: + - opam-boot-be - test-suite-be: &req-be requires: - build-be -- cgit v1.2.3