aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml119
-rw-r--r--Makefile5
-rw-r--r--Makefile.ci11
-rwxr-xr-xdev/ci/ci-color.sh8
-rw-r--r--dev/ci/ci-common.sh52
-rwxr-xr-xdev/ci/ci-compcert.sh13
-rwxr-xr-xdev/ci/ci-coquelicot.sh12
-rwxr-xr-xdev/ci/ci-cpdt.sh10
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh9
-rwxr-xr-xdev/ci/ci-flocq.sh9
-rwxr-xr-xdev/ci/ci-geocoq.sh16
-rwxr-xr-xdev/ci/ci-hott.sh8
-rwxr-xr-xdev/ci/ci-iris-coq.sh17
-rwxr-xr-xdev/ci/ci-math-classes.sh12
-rwxr-xr-xdev/ci/ci-math-comp.sh13
-rwxr-xr-xdev/ci/ci-metacoq.sh16
-rwxr-xr-xdev/ci/ci-sf.sh11
-rwxr-xr-xdev/ci/ci-tlc.sh8
-rwxr-xr-xdev/ci/ci-unimath.sh15
19 files changed, 364 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 000000000..de16f2d0b
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,119 @@
+dist: trusty
+sudo: required
+# Until Ocaml becomes a language, we set a known one.
+language: c
+cache:
+ apt: true
+ directories:
+ - $HOME/.opam
+addons:
+ apt:
+ sources:
+ - avsm
+ packages:
+ - opam
+ - aspcud
+ - gcc-multilib
+env:
+ global:
+ - NJOBS=2
+ # system is == 4.02.3
+ - COMPILER="system"
+ # Main test suites
+ matrix:
+ - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
+ - TEST_TARGET="validate" TW="travis_wait"
+ - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
+ - TEST_TARGET="ci-color"
+ - TEST_TARGET="ci-compcert"
+ - TEST_TARGET="ci-coquelicot"
+ - TEST_TARGET="ci-cpdt"
+ - TEST_TARGET="ci-geocoq"
+ - TEST_TARGET="ci-fiat-crypto"
+ - TEST_TARGET="ci-flocq"
+ - TEST_TARGET="ci-hott"
+ - TEST_TARGET="ci-iris-coq"
+ - TEST_TARGET="ci-math-classes"
+ - TEST_TARGET="ci-math-comp"
+ - TEST_TARGET="ci-sf"
+ - TEST_TARGET="ci-unimath"
+ # Not ready yet for 8.7
+ # - TEST_TARGET="ci-metacoq"
+ # - TEST_TARGET="ci-tlc"
+
+matrix:
+
+ allow_failures:
+ - env: TEST_TARGET="ci-cpdt"
+
+ # Full Coq test-suite with two compilers
+ # [TODO: use yaml refs and avoid duplication for packages list]
+ include:
+ - env:
+ - TEST_TARGET="test-suite"
+ - EXTRA_CONF="-coqide opt -with-doc yes"
+ - EXTRA_OPAM="lablgtk-extras hevea"
+ addons:
+ apt:
+ sources:
+ - avsm
+ packages:
+ - opam
+ - aspcud
+ - libgtk2.0-dev
+ - libgtksourceview2.0-dev
+ - texlive-latex-base
+ - texlive-latex-recommended
+ - texlive-latex-extra
+ - texlive-math-extra
+ - texlive-fonts-recommended
+ - texlive-fonts-extra
+ - latex-xcolor
+ - ghostscript
+ - transfig
+ - imagemagick
+ - env:
+ - TEST_TARGET="test-suite"
+ - COMPILER="4.04.0"
+ - EXTRA_CONF="-coqide opt -with-doc yes"
+ - EXTRA_OPAM="lablgtk-extras hevea"
+ addons:
+ apt:
+ sources:
+ - avsm
+ packages:
+ - opam
+ - aspcud
+ - libgtk2.0-dev
+ - libgtksourceview2.0-dev
+ - texlive-latex-base
+ - texlive-latex-recommended
+ - texlive-latex-extra
+ - texlive-math-extra
+ - texlive-fonts-recommended
+ - texlive-fonts-extra
+ - latex-xcolor
+ - ghostscript
+ - transfig
+ - imagemagick
+
+install:
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- eval $(opam config env)
+- opam config var root
+- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM}
+- opam list
+
+script:
+
+- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
+- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
+- echo -en 'travis_fold:end:coq.config\\r'
+
+- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
+- make -j ${NJOBS}
+- echo -en 'travis_fold:end:coq.build\\r'
+
+- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
+- ${TW} make -j ${NJOBS} ${TEST_TARGET}
+- echo -en 'travis_fold:end:coq.test\\r'
diff --git a/Makefile b/Makefile
index 1dd4efca2..e84d5e377 100644
--- a/Makefile
+++ b/Makefile
@@ -246,6 +246,11 @@ devdocclean:
rm -f $(OCAMLDOCDIR)/html/*.html
###########################################################################
+# Continuous Intregration Tests
+###########################################################################
+include Makefile.ci
+
+###########################################################################
# Emacs tags
###########################################################################
diff --git a/Makefile.ci b/Makefile.ci
new file mode 100644
index 000000000..e4b5832f6
--- /dev/null
+++ b/Makefile.ci
@@ -0,0 +1,11 @@
+CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
+ ci-color ci-math-classes ci-tlc ci-fiat-crypto \
+ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
+ ci-unimath
+
+.PHONY: $(CI_TARGETS)
+
+# Generic rule, we use make to easy travis integraton with mixed rules
+$(CI_TARGETS): ci-%:
+ ./dev/ci/ci-$*.sh
+
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
new file mode 100755
index 000000000..78ae7f02f
--- /dev/null
+++ b/dev/ci/ci-color.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color
+
+( cd color && make -j ${NJOBS} )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
new file mode 100644
index 000000000..412da626f
--- /dev/null
+++ b/dev/ci/ci-common.sh
@@ -0,0 +1,52 @@
+#!/bin/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
+
+# Maybe we should just use Ruby...
+mathcomp_CI_BRANCH=master
+mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git
+
+# git_checkout branch
+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'`" )
+}
+
+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 math-comp
+ ( cd math-comp/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 000000000..ec09389f8
--- /dev/null
+++ b/dev/ci/ci-compcert.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+CompCert_CI_BRANCH=master
+CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+
+opam install -j ${NJOBS} -y menhir
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+
+# 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} )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
new file mode 100755
index 000000000..94bd5e468
--- /dev/null
+++ b/dev/ci/ci-coquelicot.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+install_ssreflect
+
+# Setup coquelicot
+git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot
+
+( cd coquelicot && ./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 000000000..18d756180
--- /dev/null
+++ b/dev/ci/ci-cpdt.sh
@@ -0,0 +1,10 @@
+#!/bin/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 000000000..c669195dd
--- /dev/null
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -0,0 +1,9 @@
+#!/bin/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
+
+( cd fiat-crypto && make -j ${NJOBS} )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
new file mode 100755
index 000000000..345924e40
--- /dev/null
+++ b/dev/ci/ci-flocq.sh
@@ -0,0 +1,9 @@
+#!/bin/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
+
+( cd flocq && ./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 000000000..ce870e52b
--- /dev/null
+++ b/dev/ci/ci-geocoq.sh
@@ -0,0 +1,16 @@
+#!/bin/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
+
+git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq
+
+( cd GeoCoq && \
+ ./configure.sh && \
+ sed -i.bak '/Ch16_coordinates_with_functions\.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 000000000..0c07564c0
--- /dev/null
+++ b/dev/ci/ci-hott.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT
+
+( cd HoTT && ./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 000000000..c21af976f
--- /dev/null
+++ b/dev/ci/ci-iris-coq.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+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 )
+
+# Setup Iris
+git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq
+
+( cd iris-coq && make -j ${NJOBS} )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
new file mode 100755
index 000000000..4450dc071
--- /dev/null
+++ b/dev/ci/ci-math-classes.sh
@@ -0,0 +1,12 @@
+#!/bin/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 )
+
+git_checkout v8.6 https://github.com/c-corn/corn.git corn
+( cd corn && make -j ${NJOBS} )
+
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
new file mode 100755
index 000000000..2eb150cb5
--- /dev/null
+++ b/dev/ci/ci-math-comp.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+checkout_mathcomp math-comp
+
+# odd_order takes too much time for travis.
+( cd math-comp/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 000000000..91a33695b
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# $0 is not the safest way, but...
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+# MetaCoq + UniCoq
+
+git_checkout master https://github.com/unicoq/unicoq.git unicoq
+
+( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+
+git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq
+
+( cd MetaCoq && 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 000000000..5e41211f1
--- /dev/null
+++ b/dev/ci/ci-sf.sh
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz
+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-tlc.sh b/dev/ci/ci-tlc.sh
new file mode 100755
index 000000000..b94632492
--- /dev/null
+++ b/dev/ci/ci-tlc.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc
+
+( cd tlc && make -j ${NJOBS} )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
new file mode 100755
index 000000000..15e619acb
--- /dev/null
+++ b/dev/ci/ci-unimath.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+UniMath_CI_BRANCH=master
+UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git
+
+git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath
+
+( cd UniMath && \
+ 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-05-19 04:31:04 +0000