aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rwxr-xr-xdev/ci/ci-color.sh9
-rw-r--r--dev/ci/ci-common.sh24
-rwxr-xr-xdev/ci/ci-compcert.sh7
-rwxr-xr-xdev/ci/ci-coquelicot.sh12
-rwxr-xr-xdev/ci/ci-cpdt.sh2
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh11
-rwxr-xr-xdev/ci/ci-fiat-parsers.sh8
-rwxr-xr-xdev/ci/ci-flocq.sh11
-rwxr-xr-xdev/ci/ci-geocoq.sh8
-rwxr-xr-xdev/ci/ci-hott.sh10
-rwxr-xr-xdev/ci/ci-iris-coq.sh21
-rwxr-xr-xdev/ci/ci-math-classes.sh24
-rwxr-xr-xdev/ci/ci-math-comp.sh8
-rwxr-xr-xdev/ci/ci-metacoq.sh22
-rwxr-xr-xdev/ci/ci-sf.sh2
-rwxr-xr-xdev/ci/ci-template.sh12
-rwxr-xr-xdev/ci/ci-tlc.sh10
-rwxr-xr-xdev/ci/ci-unimath.sh7
19 files changed, 142 insertions, 67 deletions
diff --git a/.gitignore b/.gitignore
index 35cdf9b4e..64c49b008 100644
--- a/.gitignore
+++ b/.gitignore
@@ -43,6 +43,7 @@ TAGS
.DS_Store
.pc
bin/
+_build_ci
_build
myocamlbuild_config.ml
config/Makefile
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 78ae7f02f..fbcf9be1d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,8 +1,11 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+Color_CI_SVNURL=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color
+Color_CI_DIR=${CI_BUILD_DIR}/color
-( cd color && make -j ${NJOBS} )
+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
index 412da626f..6f624ab6e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
set -xe
@@ -8,20 +8,30 @@ export PATH=`pwd`/bin:$PATH
ls `pwd`/bin
+# Where we clone and build external developments
+CI_BUILD_DIR=`pwd`/_build_ci
+
# Maybe we should just use Ruby...
mathcomp_CI_BRANCH=master
mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
-# git_checkout branch
+# 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}
- echo "Checking out ${_DEST}"
- git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST}
- ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
+ mkdir -p ${_DEST}
+ ( cd ${_DEST} && \
+ if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \
+ echo "Checking out ${_DEST}" && \
+ git fetch ${_URL} ${_BRANCH} && \
+ git checkout FETCH_HEAD && \
+ echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" )
}
checkout_mathcomp()
@@ -34,8 +44,8 @@ install_ssreflect()
{
echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
- checkout_mathcomp math-comp
- ( cd math-comp/mathcomp && \
+ 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 && \
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index ec09389f8..111222ac7 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,13 +1,14 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
CompCert_CI_BRANCH=master
CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
opam install -j ${NJOBS} -y menhir
-git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( 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
index 94bd5e468..9dfdb8745 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,12 +1,14 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
+Coquelicot_CI_BRANCH=master
+Coquelicot_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git
+Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
+
install_ssreflect
-# Setup coquelicot
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
-( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 18d756180..0e791ebbf 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c669195dd..7fc0dae2c 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,9 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto
+fiat_crypto_CI_BRANCH=master
+fiat_crypto_CI_GITURL=https://github.com/mit-plv/fiat-crypto.git
+fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
-( cd fiat-crypto && make -j ${NJOBS} )
+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
index 15d73078f..0b3312e87 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -1,12 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
fiat_parsers_CI_BRANCH=master
fiat_parsers_CI_GITURL=https://github.com/mit-plv/fiat.git
+fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
-git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} fiat
+git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
-( cd fiat && make -j ${NJOBS} parsers )
+( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 345924e40..30eca7a3e 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,9 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq
+Flocq_CI_BRANCH=master
+Flocq_CI_GITURL=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git
+Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
-( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+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
index 29667b018..7b5950c88 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,15 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-# XXX: replace by generic template
GeoCoq_CI_BRANCH=master
GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git
+GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
-git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
-( cd GeoCoq && \
+( 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 && \
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 0c07564c0..62733c945 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,8 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+HoTT_CI_BRANCH=mz-8.7
+HoTT_CI_GITURL=https://github.com/ejgallego/HoTT.git
+HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
-( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} )
+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
index c21af976f..10f2c2b4b 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -1,17 +1,26 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
+stdpp_CI_BRANCH=master
+stdpp_CI_GITURL=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git
+stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
+
+Iris_CI_BRANCH=master
+Iris_CI_GITURL=https://gitlab.mpi-sws.org/FP/iris-coq.git
+Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
+
install_ssreflect
# Setup stdpp
-git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp
-( cd coq-stdpp && make -j ${NJOBS} && make install )
+git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR}
+
+( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
# Setup Iris
-git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
-( cd iris-coq && make -j ${NJOBS} )
+git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR}
+
+( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 4450dc071..e6a57404f 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,12 +1,24 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes
-( cd math-classes && make -j ${NJOBS} && make install )
+math_classes_CI_BRANCH=v8.6
+math_classes_CI_GITURL=https://github.com/math-classes/math-classes.git
+math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
-git_checkout v8.6 https://github.com/c-corn/corn.git corn
-( cd corn && make -j ${NJOBS} )
+Corn_CI_BRANCH=v8.6
+Corn_CI_GITURL=https://github.com/c-corn/corn.git
+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
index 2eb150cb5..bb8188da4 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -1,13 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-checkout_mathcomp math-comp
+mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+
+checkout_mathcomp ${mathcomp_CI_DIR}
# odd_order takes too much time for travis.
-( cd math-comp/mathcomp && \
+( 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
index 91a33695b..1ea56af29 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,16 +1,24 @@
-#!/bin/bash
+#!/usr/bin/env bash
-# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-# MetaCoq + UniCoq
+unicoq_CI_BRANCH=master
+unicoq_CI_GITURL=https://github.com/unicoq/unicoq.git
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-git_checkout master https://github.com/unicoq/unicoq.git unicoq
+metacoq_CI_BRANCH=master
+metacoq_CI_GITURL=https://github.com/MetaCoq/MetaCoq.git
+metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
-( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+# Setup UniCoq
-git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
-( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( 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
index 5e41211f1..c451bf26a 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
new file mode 100755
index 000000000..700105aed
--- /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
index b94632492..415f9b38f 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,8 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
-git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+tlc_CI_BRANCH=master
+tlc_CI_GITURL=https://gforge.inria.fr/git/tlc/tlc.git
+tlc_CI_DIR=${CI_BUILD_DIR}/tlc
-( cd tlc && make -j ${NJOBS} )
+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
index 15e619acb..4c4b4f1ce 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -1,14 +1,15 @@
-#!/bin/bash
+#!/usr/bin/env bash
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh
UniMath_CI_BRANCH=master
UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
+UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
-git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
-( cd UniMath && \
+( cd ${UniMath_CI_DIR} && \
sed -i.bak '/Folds/d' Makefile && \
sed -i.bak '/HomologicalAlgebra/d' Makefile && \
make -j ${NJOBS} BUILD_COQ=no )
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-03 23:11:31 +0000