aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README.md2
-rw-r--r--dev/ci/appveyor.bat4
-rw-r--r--dev/ci/ci-basic-overlay.sh3
-rwxr-xr-xdev/ci/ci-bignums.sh2
-rwxr-xr-xdev/ci/ci-color.sh33
-rw-r--r--dev/ci/ci-common.sh23
-rwxr-xr-xdev/ci/ci-coq-dpdgraph.sh2
-rwxr-xr-xdev/ci/ci-corn.sh10
-rwxr-xr-xdev/ci/ci-equations.sh2
-rwxr-xr-xdev/ci/ci-formal-topology.sh22
-rwxr-xr-xdev/ci/ci-hott.sh2
-rwxr-xr-xdev/ci/ci-ltac2.sh4
-rwxr-xr-xdev/ci/ci-math-classes.sh14
-rwxr-xr-xdev/ci/ci-sf.sh11
-rwxr-xr-xdev/ci/ci-wrapper.sh5
-rw-r--r--dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh2
-rw-r--r--dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh9
-rw-r--r--dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh4
-rw-r--r--dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh4
-rw-r--r--dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh4
-rw-r--r--dev/ci/user-overlays/06493-gares-API-remove-big-file.sh8
-rw-r--r--dev/ci/user-overlays/README.md4
22 files changed, 76 insertions, 98 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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 168a34e6e4..232b8a56e4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -115,7 +115,8 @@
########################################################################
# CoLoR
########################################################################
-: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
+: ${CoLoR_CI_BRANCH:=master}
+: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}
########################################################################
# SF
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 309050057c..558e8cbb8c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,33 +3,8 @@
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-Color_CI_DIR=${CI_BUILD_DIR}/color
+CoLoR_CI_DIR=${CI_BUILD_DIR}/color
-# Setup Bignums
-
-source ${ci_dir}/ci-bignums.sh
-
-# Compiles CoLoR
-
-svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
-
-sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v
-sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v
-sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
-sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
-
-# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
-sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
-sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
-sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
-sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
-sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
-sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
-sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
-sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
-sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
-sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
-sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
-sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
-
-( cd ${Color_CI_DIR} && make )
+# 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 4865be31ec..820ff89eec 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -3,8 +3,8 @@
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+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-sf.sh b/dev/ci/ci-sf.sh
index 217540cc19..4e8c7e145e 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,13 +3,10 @@
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-# XXX: Needs fixing to properly set the build directory.
-wget ${sf_lf_CI_TARURL}
-wget ${sf_plf_CI_TARURL}
-wget ${sf_vfa_CI_TARURL}
-tar xvfz lf.tgz
-tar xvfz plf.tgz
-tar xvfz vfa.tgz
+mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR}
+wget -qO- ${sf_lf_CI_TARURL} | tar xvz
+wget -qO- ${sf_plf_CI_TARURL} | tar xvz
+wget -qO- ${sf_vfa_CI_TARURL} | tar xvz
sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
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/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/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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:26:26 +0000