CI: add fcsl-pcm

.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

.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

.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"

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 \

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}"

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 )