From f725580ecffa96cb0bfd526737586f7a36499286 Mon Sep 17 00:00:00 2001
From: Beta Ziliani
Date: Wed, 25 Apr 2018 14:17:51 -0300
Subject: updating CI for Mtac2

---
 .circleci/config.yml       |  4 ++++
 .gitlab-ci.yml             |  3 +++
 .travis.yml                |  3 +++
 Makefile.ci                |  2 +-
 dev/ci/ci-basic-overlay.sh |  6 +++---
 dev/ci/ci-metacoq.sh       | 19 -------------------
 dev/ci/ci-mtac2.sh         | 19 +++++++++++++++++++
 7 files changed, 33 insertions(+), 23 deletions(-)
 delete mode 100755 dev/ci/ci-metacoq.sh
 create mode 100755 dev/ci/ci-mtac2.sh

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a552..d6a8e059c1 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -207,6 +207,9 @@ jobs:
   math-comp:
     <<: *ci-template
 
+  mtac2:
+    <<: *ci-template
+
   sf:
     <<: *ci-template
     environment:
@@ -251,6 +254,7 @@ workflows:
           requires:
             - build
             - bignums
+      - mtac2: *req-main
       - corn:
           requires:
             - build
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d6b539644..e1c5b5255a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -360,6 +360,9 @@ ci-math-classes:
 ci-math-comp:
   <<: *ci-template
 
+ci-mtac2:
+  <<: *ci-template
+
 ci-sf:
   <<: *ci-template
   variables:
diff --git a/.travis.yml b/.travis.yml
index fe376431e3..052979bcb3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -115,6 +115,9 @@ matrix:
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-math-comp"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-mtac2"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-sf"
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f87232..37b14ed918 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,7 +28,7 @@ CI_TARGETS=ci-bignums \
     ci-ltac2 \
     ci-math-classes \
     ci-math-comp \
-    ci-metacoq \
+    ci-mtac2 \
     ci-sf \
     ci-tlc \
     ci-unimath \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a51175..5cee72cc73 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
 : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
 
 ########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
 ########################################################################
 : "${unicoq_CI_BRANCH:=master}"
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
 
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
 
 ########################################################################
 # Mathclasses + Corn
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
deleted file mode 100755
index a66dc1e762..0000000000
--- a/dev/ci/ci-metacoq.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
-
-# Setup UniCoq
-
-git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
-
-( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && 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 )
diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh
new file mode 100755
index 0000000000..1372acb8e5
--- /dev/null
+++ b/dev/ci/ci-mtac2.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
+
+# Setup UniCoq
+
+git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
+
+( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install )
+
+# Setup MetaCoq
+
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
+
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
-- 
cgit v1.2.3