diff options
Diffstat (limited to 'dev/ci')
24 files changed, 65 insertions, 79 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558cc..bb13587e94 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index e2fbf1f6d1..dec6f0d182 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -25,7 +25,7 @@ if %USEOPAM% == false ( -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit - 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) if %USEOPAM% == true ( @@ -37,5 +37,5 @@ if %USEOPAM% == true ( GOTO :EOF :ErrorExit - ECHO ERROR MakeCoq_MinGW.bat failed + ECHO ERROR %0 failed EXIT /b 1 diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index d68674381a..c90e516ae9 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -13,4 +13,4 @@ bignums_CI_DIR=${CI_BUILD_DIR}/Bignums git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR} -( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install) +( cd ${bignums_CI_DIR} && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index c3ae7552a9..558e8cbb8c 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-common.sh b/dev/ci/ci-common.sh index 1bfdf7dfbe..58c90ff11d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,8 +5,17 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin - export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" + export CI_BRANCH="$CI_COMMIT_REF_NAME" else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + elif [ -n "${CIRCLECI}" ]; + then + export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" + export CI_BRANCH="$CIRCLE_BRANCH" + fi export COQBIN=`pwd`/bin fi export PATH="$COQBIN:$PATH" @@ -53,6 +62,18 @@ checkout_mathcomp() git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} } +make() +{ + # +x: add x only if defined + if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; + then + # Not submake and parallel make requested + command make -j "$NJOBS" "$@" + else + command make "$@" + fi +} + # this installs just the ssreflect library of math-comp install_ssreflect() { diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index b610f70004..5d6bd6a368 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite ) +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh new file mode 100755 index 0000000000..54cad5df4c --- /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-equations.sh b/dev/ci/ci-equations.sh index f7470463d9..62854afac6 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -7,4 +7,4 @@ 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) +( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 2556f84a55..53eb55fc45 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-hott.sh b/dev/ci/ci-hott.sh index 1bf6e9a872..693135a4c9 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index ed40036012..820ff89eec 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -7,4 +7,4 @@ ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} -( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install ) +( cd ${ltac2_CI_DIR} && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 2837dee963..db4a31e549 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 96acc5a11c..12a70176c2 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -13,11 +13,14 @@ 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}/../.." +export TIMED=1 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index af4a96f4ae..7716bcb59a 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,4 +1,4 @@ -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh deleted file mode 100644 index 5c4dd1324f..0000000000 --- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then - formal_topology_CI_BRANCH=ci - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git - - HoTT_CI_BRANCH=coq-pr-1033 - HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git - - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh deleted file mode 100644 index cdca8e525a..0000000000 --- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then - ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer - ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git -fi diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh deleted file mode 100644 index 6741cf26fb..0000000000 --- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then - ltac2_CI_BRANCH=master - ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2 -fi diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh deleted file mode 100644 index c9f1272bed..0000000000 --- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then - ltac2_CI_BRANCH=localityfixyou - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git -fi diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh deleted file mode 100644 index 7e9b5febdd..0000000000 --- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then - Equations_CI_BRANCH=fix-coq-6324 - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh deleted file mode 100644 index c0dcf79e1d..0000000000 --- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then - Equations_CI_BRANCH=econstr+fix_class - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh new file mode 100644 index 0000000000..c2e3670380 --- /dev/null +++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then + Equations_CI_BRANCH=rm-local-polymorphic-flag + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 0000000000..78789a6fc5 --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh new file mode 100644 index 0000000000..9677b35253 --- /dev/null +++ b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then + Equations_CI_BRANCH=API-removal + Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git + coq_dpdgraph_CI_BRANCH=API-removal + coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git + ltac2_CI_BRANCH=API-removal + ltac2_CI_GITURL=https://github.com/gares/ltac2.git +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9146d3d521..9f0377ceea 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi ``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) |