From 80b2a82d25fc9117270b9a052e4071d87eb6755f Mon Sep 17 00:00:00 2001
From: Anton Trunov <anton.a.trunov@gmail.com>
Date: Fri, 20 Apr 2018 18:28:34 +0200
Subject: CI: add fcsl-pcm

---
 .circleci/config.yml       |  4 ++++
 .gitlab-ci.yml             |  3 +++
 .travis.yml                |  3 +++
 Makefile.ci                |  1 +
 dev/ci/ci-basic-overlay.sh |  6 ++++++
 dev/ci/ci-fcsl-pcm.sh      | 12 ++++++++++++
 6 files changed, 29 insertions(+)
 mode change 100644 => 100755 dev/ci/ci-basic-overlay.sh
 create mode 100755 dev/ci/ci-fcsl-pcm.sh

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 00db64f26..8b6b43a55 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -165,6 +165,9 @@ jobs:
   geocoq:
     <<: *ci-template
 
+  fcsl-pcm:
+    <<: *ci-template
+
   fiat-crypto:
     <<: *ci-template
 
@@ -240,6 +243,7 @@ workflows:
       - elpi: *req-main
       - equations: *req-main
       - geocoq: *req-main
+      - fcsl-pcm: *req-main
       - fiat-crypto: *req-main
       - fiat-parsers: *req-main
       - flocq: *req-main
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e79ed125e..7d6b53964 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -319,6 +319,9 @@ ci-geocoq:
   <<: *ci-template
   allow_failure: true
 
+ci-fcsl-pcm:
+  <<: *ci-template
+
 # ci-fiat-crypto:
 #   <<: *ci-template
 #   # out of memory error
diff --git a/.travis.yml b/.travis.yml
index 55b4da719..fe376431e 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -85,6 +85,9 @@ matrix:
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-geocoq"
+    - if: NOT (type = pull_request)
+      env:
+      - TEST_TARGET="ci-fcsl-pcm"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-fiat-crypto"
diff --git a/Makefile.ci b/Makefile.ci
index 3c26bf964..6b30f8723 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \
     ci-cpdt \
     ci-elpi \
     ci-equations \
+    ci-fcsl-pcm \
     ci-fiat-crypto \
     ci-fiat-parsers \
     ci-flocq \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
old mode 100644
new mode 100755
index 2adc7d8dc..5566a5117
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -150,3 +150,9 @@
 ########################################################################
 : "${Elpi_CI_BRANCH:=coq-master}"
 : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}"
+
+########################################################################
+# fcsl-pcm
+########################################################################
+: "${fcsl_pcm_CI_BRANCH:=master}"
+: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}"
diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh
new file mode 100755
index 000000000..fdc4c729b
--- /dev/null
+++ b/dev/ci/ci-fcsl-pcm.sh
@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm"
+
+install_ssreflect
+
+git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}"
+
+( cd "${fcsl_pcm_CI_DIR}" && make )
-- 
cgit v1.2.3