From f725580ecffa96cb0bfd526737586f7a36499286 Mon Sep 17 00:00:00 2001
From: Beta Ziliani <bziliani@famaf.unc.edu.ar>
Date: Wed, 25 Apr 2018 14:17:51 -0300
Subject: [PATCH] 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 => ci-mtac2.sh} | 6 +++---
 6 files changed, 17 insertions(+), 7 deletions(-)
 rename dev/ci/{ci-metacoq.sh => ci-mtac2.sh} (61%)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a55205..d6a8e059c1b8 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 7d6b539644c7..e1c5b5255ad3 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 fe376431e38a..052979bcb3a7 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 6b30f8723217..37b14ed91851 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 5566a5117514..5cee72cc7341 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-mtac2.sh
similarity index 61%
rename from dev/ci/ci-metacoq.sh
rename to dev/ci/ci-mtac2.sh
index a66dc1e762ce..1372acb8e554 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
 
 # Setup UniCoq
 
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
 
 # Setup MetaCoq
 
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
 
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )