aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/ci-basic-overlay.sh103
-rwxr-xr-xdev/ci/ci-color.sh10
-rw-r--r--dev/ci/ci-common.sh66
-rwxr-xr-xdev/ci/ci-compcert.sh12
-rwxr-xr-xdev/ci/ci-coquelicot.sh12
-rwxr-xr-xdev/ci/ci-cpdt.sh10
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh10
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh10
-rwxr-xr-xdev/ci/ci-flocq.sh10
-rwxr-xr-xdev/ci/ci-geocoq.sh16
-rwxr-xr-xdev/ci/ci-hott.sh10
-rwxr-xr-xdev/ci/ci-iris-coq.sh26
-rwxr-xr-xdev/ci/ci-math-classes.sh20
-rwxr-xr-xdev/ci/ci-math-comp.sh15
-rwxr-xr-xdev/ci/ci-metacoq.sh19
-rwxr-xr-xdev/ci/ci-sf.sh12
-rwxr-xr-xdev/ci/ci-template.sh12
-rwxr-xr-xdev/ci/ci-tlc.sh10
-rwxr-xr-xdev/ci/ci-unimath.sh14
-rw-r--r--dev/ci/ci-user-overlay.sh22
20 files changed, 419 insertions, 0 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
new file mode 100644
index 0000000000..241ec35861
--- /dev/null
+++ b/dev/ci/ci-basic-overlay.sh
@@ -0,0 +1,103 @@
+#!/usr/bin/env bash
+
+# This is the basic overlay set for repositories in the CI.
+
+# Maybe we should just use Ruby to have real objects...
+
+########################################################################
+# MathComp
+########################################################################
+: ${mathcomp_CI_BRANCH:=master}
+: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}
+
+########################################################################
+# UniMath
+########################################################################
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
+
+########################################################################
+# Unicoq + Metacoq
+########################################################################
+: ${unicoq_CI_BRANCH:=master}
+: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}
+
+: ${metacoq_CI_BRANCH:=master}
+: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}
+
+########################################################################
+# Mathclasses + Corn
+########################################################################
+: ${math_classes_CI_BRANCH:=v8.6}
+: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+
+: ${Corn_CI_BRANCH:=v8.6}
+: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+
+########################################################################
+# Iris
+########################################################################
+: ${stdpp_CI_BRANCH:=master}
+: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}
+
+: ${Iris_CI_BRANCH:=master}
+: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}
+
+########################################################################
+# HoTT
+########################################################################
+: ${HoTT_CI_BRANCH:=mz-8.7}
+: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git}
+
+########################################################################
+# GeoCoq
+########################################################################
+: ${GeoCoq_CI_BRANCH:=master}
+: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}
+
+########################################################################
+# Flocq
+########################################################################
+: ${Flocq_CI_BRANCH:=master}
+: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}
+
+########################################################################
+# Coquelicot
+########################################################################
+: ${Coquelicot_CI_BRANCH:=master}
+: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}
+
+########################################################################
+# CompCert
+########################################################################
+: ${CompCert_CI_BRANCH:=master}
+: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+
+########################################################################
+# fiat_parsers
+########################################################################
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
+
+########################################################################
+# fiat_crypto
+########################################################################
+: ${fiat_crypto_CI_BRANCH:=master}
+: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+
+########################################################################
+# CoLoR
+########################################################################
+: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color}
+
+########################################################################
+# SF
+########################################################################
+: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz}
+
+########################################################################
+# TLC
+########################################################################
+: ${tlc_CI_BRANCH:=master}
+: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
new file mode 100755
index 0000000000..3f0716511d
--- /dev/null
+++ b/dev/ci/ci-color.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Color_CI_DIR=${CI_BUILD_DIR}/color
+
+svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
+
+( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
new file mode 100644
index 0000000000..2711b7ecaa
--- /dev/null
+++ b/dev/ci/ci-common.sh
@@ -0,0 +1,66 @@
+#!/usr/bin/env bash
+
+set -xe
+
+# Coq's tools need an ending slash :S, we should fix them.
+export COQBIN=`pwd`/bin/
+export PATH=`pwd`/bin:$PATH
+
+ls `pwd`/bin
+
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
+source ${ci_dir}/ci-user-overlay.sh
+source ${ci_dir}/ci-basic-overlay.sh
+
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+# git_checkout branch url dest will create a git repository
+# in <dest> (if it does not exist already) and checkout the
+# remote branch <branch> from <url>
+git_checkout()
+{
+ local _BRANCH=${1}
+ local _URL=${2}
+ local _DEST=${3}
+
+ # Allow an optional 4th argument for the commit
+ local _COMMIT=${4:-FETCH_HEAD}
+ local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi)
+
+ mkdir -p ${_DEST}
+ ( cd ${_DEST} && \
+ if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \
+ echo "Checking out ${_DEST}" && \
+ git fetch ${_URL} ${_BRANCH} && \
+ git checkout ${_COMMIT} && \
+ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+}
+
+checkout_mathcomp()
+{
+ git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+}
+
+# this installs just the ssreflect library of math-comp
+install_ssreflect()
+{
+ echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
+
+ checkout_mathcomp ${mathcomp_CI_DIR}
+ ( cd ${mathcomp_CI_DIR}/mathcomp && \
+ sed -i.bak '/ssrtest/d' Make && \
+ sed -i.bak '/odd_order/d' Make && \
+ sed -i.bak '/all\/all.v/d' Make && \
+ sed -i.bak '/character/d' Make && \
+ sed -i.bak '/real_closed/d' Make && \
+ sed -i.bak '/solvable/d' Make && \
+ sed -i.bak '/field/d' Make && \
+ sed -i.bak '/fingroup/d' Make && \
+ sed -i.bak '/algebra/d' Make && \
+ make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+
+ echo -en 'travis_fold:end:ssr.install\\r'
+
+}
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
new file mode 100755
index 0000000000..c78ffdc2c0
--- /dev/null
+++ b/dev/ci/ci-compcert.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
+
+opam install -j ${NJOBS} -y menhir
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
+
+# Patch to avoid the upper version limit
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
new file mode 100755
index 0000000000..40eff03b78
--- /dev/null
+++ b/dev/ci/ci-coquelicot.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
+
+install_ssreflect
+
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
+
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
new file mode 100755
index 0000000000..0e791ebbfd
--- /dev/null
+++ b/dev/ci/ci-cpdt.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget http://adam.chlipala.net/cpdt/cpdt.tgz
+tar xvfz cpdt.tgz
+
+( cd cpdt && make clean && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
new file mode 100755
index 0000000000..93d39aab07
--- /dev/null
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
+
+git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
+
+( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
new file mode 100755
index 0000000000..c62aa1d859
--- /dev/null
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
+
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
+
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
new file mode 100755
index 0000000000..ec19bd9939
--- /dev/null
+++ b/dev/ci/ci-flocq.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
+
+git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
+
+( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
new file mode 100755
index 0000000000..4e5aa2687b
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
+
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
+
+( cd ${GeoCoq_CI_DIR} && \
+ ./configure.sh && \
+ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \
+ sed -i.bak '/Elements\/Book_1\.v/d' Make && \
+ sed -i.bak '/Elements\/Book_3\.v/d' Make && \
+ coq_makefile -f Make -o Makefile && \
+ make -j ${NJOBS} )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
new file mode 100755
index 0000000000..1bf6e9a872
--- /dev/null
+++ b/dev/ci/ci-hott.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+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} )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
new file mode 100755
index 0000000000..262dd6fa01
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
+
+Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
+
+install_ssreflect
+
+# Setup Iris first, as it is needed to compute the dependencies
+
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins
+
+# Setup stdpp
+stdpp_CI_GITURL=${IRIS_DEP[1]}.git
+stdpp_CI_COMMIT=${IRIS_DEP[2]}
+
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
+
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Build iris now
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
new file mode 100755
index 0000000000..beb75773b7
--- /dev/null
+++ b/dev/ci/ci-math-classes.sh
@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+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
+
+# Setup Math-Classes
+
+git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+
+( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+
+# Setup Corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
new file mode 100755
index 0000000000..bb8188da4e
--- /dev/null
+++ b/dev/ci/ci-math-comp.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
+
+# odd_order takes too much time for travis.
+( cd ${mathcomp_CI_DIR}/mathcomp && \
+ sed -i.bak '/PFsection/d' Make && \
+ sed -i.bak '/stripped_odd_order_theorem/d' Make && \
+ make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..e31691179e
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+
+# Setup UniCoq
+
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
+
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+
+# Setup MetaCoq
+
+git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
+
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
new file mode 100755
index 0000000000..7d23ccad97
--- /dev/null
+++ b/dev/ci/ci-sf.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# XXX: Needs fixing to properly set the build directory.
+wget ${sf_CI_TARURL}
+tar xvfz sf.tgz
+
+( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
+
+
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
new file mode 100755
index 0000000000..700105aed4
--- /dev/null
+++ b/dev/ci/ci-template.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Template_CI_BRANCH=master
+Template_CI_GITURL=https://github.com/Template/Template
+Template_CI_DIR=${CI_BUILD_DIR}/Template
+
+git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
+
+( cd ${Template_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
new file mode 100755
index 0000000000..ce26399378
--- /dev/null
+++ b/dev/ci/ci-tlc.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+tlc_CI_DIR=${CI_BUILD_DIR}/tlc
+
+git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
+
+( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
new file mode 100755
index 0000000000..175b82b5f9
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
+
+( cd ${UniMath_CI_DIR} && \
+ sed -i.bak '/Folds/d' Makefile && \
+ sed -i.bak '/HomologicalAlgebra/d' Makefile && \
+ make -j ${NJOBS} BUILD_COQ=no )
+
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
new file mode 100644
index 0000000000..0285747432
--- /dev/null
+++ b/dev/ci/ci-user-overlay.sh
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+# Add user overlays here. You can use some logic to detect if you are
+# in your travis branch and conditionally enable the overlay.
+
+# Some useful Travis variables:
+# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
+#
+# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
+# the name of the branch currently being built; whereas for builds
+# triggered by a pull request this is the name of the branch
+# targeted by the pull request (in many cases this will be master).
+#
+# - TRAVIS_COMMIT: The commit that the current build is testing.
+#
+# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
+# a pull request, “false” if it’s not a pull request.
+#
+# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
+# the name of the branch from which the PR originated. "" if the
+# current job is a push build.
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 08:11:09 +0000