diff options
| author | Maxime Dénès | 2017-11-21 13:07:11 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-21 13:07:11 +0100 |
| commit | 33c5603dfe76cbd96944fd38d5fa6699c32a9355 (patch) | |
| tree | c80d4da99d5c357218cafd7498b50adf648153d5 | |
| parent | d0c42fea9edfef645a822e9f12d475c205f93932 (diff) | |
| parent | 9826bbd4eb1ded394d38a94abff25baa71823221 (diff) | |
Merge PR #6168: Add Equations to CI
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | .travis.yml | 1 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-equations.sh | 10 |
5 files changed, 21 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index fcf6413be3..7c3489de42 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -284,6 +284,9 @@ ci-coquelicot: <<: *ci-template-vars EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" +ci-equations: + <<: *ci-template + ci-geocoq: <<: *ci-template allow_failure: true diff --git a/.travis.yml b/.travis.yml index 3ebfbefd20..1f6bb11e0e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -50,6 +50,7 @@ env: - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - TEST_TARGET="ci-coquelicot TIMED=1" + - TEST_TARGET="ci-equations TIMED=1" - TEST_TARGET="ci-geocoq TIMED=1" - TEST_TARGET="ci-fiat-crypto TIMED=1" - TEST_TARGET="ci-fiat-parsers TIMED=1" diff --git a/Makefile.ci b/Makefile.ci index 0b2cbb6637..a17d4ddf75 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -5,6 +5,7 @@ CI_TARGETS=ci-all \ ci-coq-dpdgraph \ ci-coquelicot \ ci-cpdt \ + ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ ci-flocq \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index cb1493d6aa..168a34e6e4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -135,3 +135,9 @@ ######################################################################## : ${bignums_CI_BRANCH:=master} : ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} + +######################################################################## +# Equations +######################################################################## +: ${Equations_CI_BRANCH:=8.8+alpha} +: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh new file mode 100755 index 0000000000..f7470463d9 --- /dev/null +++ b/dev/ci/ci-equations.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Equations_CI_DIR=${CI_BUILD_DIR}/Equations + +git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} + +( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install) |