6 files changed, 32 insertions, 42 deletions
diff --git a/Makefile.ci b/Makefile.ci
index a17d4ddf7..2a6222e22 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -4,6 +4,7 @@ CI_TARGETS=ci-all \
     ci-compcert \
     ci-coq-dpdgraph \
     ci-coquelicot \
+    ci-corn \
     ci-cpdt \
     ci-equations \
     ci-fiat-crypto \
@@ -24,6 +25,21 @@ CI_TARGETS=ci-all \
 
 .PHONY: $(CI_TARGETS)
 
+_build_ci/.ci-%.done:
+	+./dev/ci/ci-wrapper.sh $*
+
+ci-color: ci-bignums
+
+ci-math-classes: ci-bignums
+
+ci-corn: ci-math-classes
+
+ci-formal-topology: ci-corn
+
 # Generic rule, we use make to ease travis integration with mixed rules
-$(CI_TARGETS): ci-%:
-	+./dev/ci/ci-wrapper.sh ci-$*.sh
+$(CI_TARGETS): ci-%: _build_ci/.ci-%.done
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index c3ae7552a..558e8cbb8 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-corn.sh b/dev/ci/ci-corn.sh
new file mode 100755
index 000000000..54cad5df4
--- /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-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 2556f84a5..53eb55fc4 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-math-classes.sh b/dev/ci/ci-math-classes.sh
index 2837dee96..db4a31e54 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 96acc5a11..a21bf9f38 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -13,7 +13,8 @@ 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}/../.."
@@ -22,3 +23,5 @@ cd "${DIR}/../.."
 travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
 travis_fold 'end' 'coq.test.timing'
+
+touch "_build_ci/.ci-${CI_NAME}.done"