updating CI for Mtac2

validsdp · Apr 25, 2018 · f725580 · f725580
1 parent 6d4d16e
commit f725580
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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 → dev/ci/ci-mtac2.sh b/dev/ci/ci-metacoq.sh → 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 )