From 8dc2adfd102185c6c3c4b61709f2b55aefab2641 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 29 Apr 2017 13:07:45 -0400
Subject: Add bmsherman/topology to the ci

This development of @bmsherman tests universe polymorphism and setoid
rewriting in type, and should build with v8.6 and trunk.
---
 .travis.yml                  |  1 +
 Makefile.ci                  |  2 +-
 dev/ci/ci-basic-overlay.sh   |  6 ++++++
 dev/ci/ci-formal-topology.sh | 28 ++++++++++++++++++++++++++++
 4 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100755 dev/ci/ci-formal-topology.sh

diff --git a/.travis.yml b/.travis.yml
index 77aac23b7..3ed547bb1 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -41,6 +41,7 @@ env:
   - TEST_TARGET="ci-math-classes"
   - TEST_TARGET="ci-math-comp"
   - TEST_TARGET="ci-sf"
+  - TEST_TARGET="ci-formal-topology"
   - TEST_TARGET="ci-unimath"
   - TEST_TARGET="ci-vst"
   # Not ready yet for 8.7
diff --git a/Makefile.ci b/Makefile.ci
index 4c4606aff..013685218 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,7 +1,7 @@
 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-fiat-parsers \
            ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
-           ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade
+           ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade ci-formal-topology
 
 .PHONY: $(CI_TARGETS)
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e0851816c..5da13c100 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -106,6 +106,12 @@
 : ${bedrock_facade_CI_BRANCH:=master}
 : ${bedrock_facade_CI_GITURL:=https://github.com/JasonGross/bedrock.git}
 
+########################################################################
+# formal-topology
+########################################################################
+: ${formal_topology_CI_BRANCH:=ci}
+: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}
+
 ########################################################################
 # CoLoR
 ########################################################################
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
new file mode 100755
index 000000000..ecb36349f
--- /dev/null
+++ b/dev/ci/ci-formal-topology.sh
@@ -0,0 +1,28 @@
+#!/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
+
+formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
+
+# 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} && 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 -j ${NJOBS} )
-- 
cgit v1.2.3