[ci] add metacoq

5 files changed, 33 insertions, 1 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 5b343a23c5..cf1dc47fab 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -731,10 +731,24 @@ plugin:ci-elpi:
 
 plugin:ci-equations:
   extends: .ci-template
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _build_ci
 
 plugin:ci-fiat_parsers:
   extends: .ci-template
 
+plugin:ci-metacoq:
+  extends: .ci-template
+  stage: stage-3
+  needs:
+  - build:base
+  - plugin:ci-equations
+  dependencies:
+  - build:base
+  - plugin:ci-equations
+
 plugin:ci-mtac2:
   extends: .ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index dfb3f69a8c..f58dd9f37a 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -33,6 +33,7 @@ CI_TARGETS= \
     ci-iris-lambda-rust \
     ci-math-classes \
     ci-math-comp \
+    ci-metacoq \
     ci-mtac2 \
     ci-paramcoq \
     ci-perennial \
@@ -72,6 +73,8 @@ ci-fiat-crypto: ci-coqprime ci-rewriter
 ci-simple-io: ci-ext-lib
 ci-quickchick: ci-ext-lib ci-simple-io
 
+ci-metacoq: ci-equations
+
 # Generic rule, we use make to ease CI integration
 $(CI_TARGETS): ci-%:
 	+./dev/ci/ci-wrapper.sh $*
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..70e3fe5c69 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -330,3 +330,10 @@
 : "${perennial_CI_REF:=master}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )