diff options
| -rw-r--r-- | .circleci/config.yml | 404 | ||||
| -rw-r--r-- | Makefile.ci | 20 | ||||
| -rw-r--r-- | README.md | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-color.sh | 3 | ||||
| -rwxr-xr-x | dev/ci/ci-corn.sh | 10 | ||||
| -rwxr-xr-x | dev/ci/ci-formal-topology.sh | 22 | ||||
| -rwxr-xr-x | dev/ci/ci-math-classes.sh | 14 | ||||
| -rwxr-xr-x | dev/ci/ci-wrapper.sh | 5 | ||||
| -rw-r--r-- | test-suite/Makefile | 2 |
9 files changed, 442 insertions, 44 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml new file mode 100644 index 000000000..7c250c667 --- /dev/null +++ b/.circleci/config.yml @@ -0,0 +1,404 @@ +defaults: + params: ¶ms + # Following parameters are used in Coq CircleCI Job (using yaml + # reference syntax) + working_directory: ~/coq + docker: + - 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" + NATIVE_COMP: "yes" + + # 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: Install system packages + command: | + echo export TERM=xterm >> ~/.profile + source ~/.profile + 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 + +opam-switch: &opam-switch + name: Select opam switch + command: | + source ~/.profile + opam switch ${COMPILER} + opam config list + opam list + +.opam-boot-template: &opam-boot-template + <<: *params + steps: + - checkout + - run: *before_script + - restore_cache: + keys: + - 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 }}-{{ .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 + + ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} + - run: &build-build + name: Build + command: | + source ~/.profile + make -j ${NJOBS} byte + make -j ${NJOBS} + make test-suite/misc/universes/all_stdlib.v + - persist_to_workspace: + root: *workspace + paths: + - coq/ + + environment: &build-variables + <<: *envvars + EXTRA_CONF: "-coqide opt" + EXTRA_PACKAGES: *coqide-packages + +.validate-template: &validate-template + <<: *params + steps: + - run: *before_script + - attach_workspace: *attach_workspace + - run: + name: Validate + command: | + source ~/.profile + make validate + environment: *envvars + +.documentation-template: &documentation-template + <<: *params + steps: + - run: *before_script + - attach_workspace: *attach_workspace + - run: + name: Documentation + command: | + source ~/.profile + make -j ${NJOBS} doc + environment: &documentation-variables + <<: *envvars + EXTRA_PACKAGES: *coqdoc-packages + +.test-suite-template: &test-suite-template + <<: *params + steps: + - run: *before_script + - attach_workspace: *attach_workspace + - run: + name: Test + command: | + source ~/.profile + cd test-suite + make clean + make -j ${NJOBS} all + environment: &test-suite-variables + <<: *envvars + EXTRA_PACKAGES: *timing-packages + +.ci-template: &ci-template + <<: *params + steps: + - run: *before_script + - attach_workspace: *attach_workspace + - run: + name: Test + command: | + source ~/.profile + make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB} + - persist_to_workspace: + root: *workspace + paths: + - coq/ + environment: &ci-template-vars + <<: *envvars + EXTRA_PACKAGES: *timing-packages + +# Defines individual jobs, see the workflows section below for job orchestration +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 + + 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 + + validate: *validate-template + + validate-32bit: + <<: *validate-template + environment: + <<: *envvars + COMPILER: *compiler-32bit + EXTRA_PACKAGES: "gcc-multilib" + + 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 + 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_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-math-classes: + <<: *ci-template + + ci-corn: + <<: *ci-template + + 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 + main: + jobs: + - opam-boot + - opam-boot-32bit + - opam-boot-be + + - build: + requires: + - opam-boot + - validate: &req-main + requires: + - build + - test-suite: *req-main + - documentation: *req-main + + - ci-bignums: *req-main + - ci-color: + requires: + - build + - ci-bignums + - 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-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 + - ci-math-comp: *req-main + - ci-sf: *req-main + - ci-unimath: *req-main + - ci-vst: *req-main + + - build-32bit: + requires: + - opam-boot-32bit + - validate-32bit: &req-32bit + requires: + - build-32bit + - test-suite-32bit: *req-32bit + + - build-be: + requires: + - opam-boot-be + - test-suite-be: &req-be + requires: + - build-be + - documentation-be: *req-be diff --git a/Makefile.ci b/Makefile.ci index a17d4ddf7..2a6222e22 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -4,6 +4,7 @@ CI_TARGETS=ci-all \ ci-compcert \ ci-coq-dpdgraph \ ci-coquelicot \ + ci-corn \ ci-cpdt \ ci-equations \ ci-fiat-crypto \ @@ -24,6 +25,21 @@ CI_TARGETS=ci-all \ .PHONY: $(CI_TARGETS) +_build_ci/.ci-%.done: + +./dev/ci/ci-wrapper.sh $* + +ci-color: ci-bignums + +ci-math-classes: ci-bignums + +ci-corn: ci-math-classes + +ci-formal-topology: ci-corn + # Generic rule, we use make to ease travis integration with mixed rules -$(CI_TARGETS): ci-%: - +./dev/ci/ci-wrapper.sh ci-$*.sh +$(CI_TARGETS): ci-%: _build_ci/.ci-%.done + +# For emacs: +# Local Variables: +# mode: makefile +# End: @@ -1,6 +1,10 @@ # Coq -[](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://gitter.im/coq/coq) +- [](https://travis-ci.org/coq/coq/builds) Travis CI +- [](https://ci.appveyor.com/project/coq/coq/branch/master) Appveyor CI (Windows) +- [](https://circleci.com/gh/SkySkimmer/workflows/coq) Circle CI + +[](https://gitter.im/coq/coq) Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index c3ae7552a..558e8cbb8 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -5,9 +5,6 @@ source ${ci_dir}/ci-common.sh CoLoR_CI_DIR=${CI_BUILD_DIR}/color -# Setup Bignums -source ${ci_dir}/ci-bignums.sh - # Compile CoLoR git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} ( cd ${CoLoR_CI_DIR} && make ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh new file mode 100755 index 000000000..54cad5df4 --- /dev/null +++ b/dev/ci/ci-corn.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Corn_CI_DIR=${CI_BUILD_DIR}/corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make && make install ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 2556f84a5..53eb55fc4 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -3,30 +3,8 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes - -Corn_CI_DIR=${CI_BUILD_DIR}/corn - formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology -# Setup Bignums - -source ${ci_dir}/ci-bignums.sh - -# Setup Math-Classes - -git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} - -( cd ${math_classes_CI_DIR} && make && make install ) - -# Setup Corn - -git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} - -( cd ${Corn_CI_DIR} && make && make install ) - -# Setup formal-topology - git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} ( cd ${formal_topology_CI_DIR} && make ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 2837dee96..db4a31e54 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -5,20 +5,6 @@ source ${ci_dir}/ci-common.sh math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes -Corn_CI_DIR=${CI_BUILD_DIR}/corn - -# Setup Bignums - -source ${ci_dir}/ci-bignums.sh - -# Setup Math-Classes - git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} ( cd ${math_classes_CI_DIR} && make && make install ) - -# Setup Corn - -git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} - -( cd ${Corn_CI_DIR} && make ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 96acc5a11..a21bf9f38 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -13,7 +13,8 @@ function travis_fold { fi } -CI_SCRIPT="$1" +CI_NAME="$1" +CI_SCRIPT="ci-${CI_NAME}.sh" DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" # assume this script is in dev/ci/, cd to the root Coq directory cd "${DIR}/../.." @@ -22,3 +23,5 @@ cd "${DIR}/../.." travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log travis_fold 'end' 'coq.test.timing' + +touch "_build_ci/.ci-${CI_NAME}.done" diff --git a/test-suite/Makefile b/test-suite/Makefile index 6865dcc76..dbd63a57b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -177,7 +177,7 @@ summary.log: report: summary.log $(HIDE)bash save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi + $(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### |