Merge PR #6400: Circle CI

5 files changed, 14 insertions, 40 deletions

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"