4 files changed, 24 insertions, 13 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 48e01e9e93..5566a51175 100644..100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -142,7 +142,7 @@
 ########################################################################
 # Equations
 ########################################################################
-: "${Equations_CI_BRANCH:=8.8+alpha}"
+: "${Equations_CI_BRANCH:=master}"
 : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
 
 ########################################################################
@@ -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 0000000000..fdc4c729b6
--- /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 )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 6c8dce5bd0..845addb4cd 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -8,4 +8,4 @@ fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
 git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-( cd "${fiat_crypto_CI_DIR}" && make lite )
+( cd "${fiat_crypto_CI_DIR}" && make lite lite-display )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index b019fa059a..1af0f634c4 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,27 +9,20 @@ lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust"
 
 install_ssreflect
 
-# Add or update the opam repo we need for dependency resolution
-opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
-
 # Setup lambdaRust first
 git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}"
 
 # Extract required version of Iris
-Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url)
-read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')"
+Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup Iris
-git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}"
+git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}"
 
 # Extract required version of std++
-stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url)
-read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')"
+stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup std++
-git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}"
+git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}"
 
 # Build std++
 ( cd "${stdpp_CI_DIR}" && make && make install )