aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.circleci/config.yml4
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--.travis.yml3
-rw-r--r--Makefile.ci2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-mtac2.sh (renamed from dev/ci/ci-metacoq.sh)6
6 files changed, 17 insertions, 7 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a55..d6a8e059c 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 7d6b53964..e1c5b5255 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 fe376431e..052979bcb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -117,6 +117,9 @@ matrix:
- 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"
- if: NOT (type = pull_request)
env:
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f8723..37b14ed91 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 5566a5117..5cee72cc7 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
index a66dc1e76..1372acb8e 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 )