7 files changed, 33 insertions, 20 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 )
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 3a2df6a81f..84ff94c66a 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -70,7 +70,7 @@ To merge the PR proceed in the following way
 ```
 $ git checkout master
 $ git pull
-$ dev/tools/merge-pr XXXX
+$ dev/tools/merge-pr.sh XXXX
 $ git push upstream
 ```
 where `XXXX` is the number of the PR to be merged and `upstream` is the name
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 1c94f630f2..00d04e6b3d 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -5,7 +5,7 @@ set -o pipefail
 
 API=https://api.github.com/repos/coq/coq
 OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq"
-OFFICIAL_REMOTE_HTTPS_URL="https://github.com/coq/coq"
+OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq"
 
 # This script depends (at least) on git (>= 2.7) and jq.
 # It should be used like this: dev/tools/merge-pr.sh /PR number/
@@ -91,8 +91,10 @@ fi
 REMOTE_URL=$(git remote get-url "$REMOTE" --all)
 if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \
    [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \
-   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
-   [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_HTTPS_URL}.git" ]; then
+   [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \
+   [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \
+   [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \
+   [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
   error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL"
   error "it points to ${BLUE}$REMOTE_URL${RESET} instead"
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index a514b8866a..b56925c370 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -27,8 +27,8 @@ then
 
     # reset work tree and index
     # NB: untracked files which were not added are untouched
-    git apply --cached -R "$index"
-    git apply -R "$tree"
+    git apply --whitespace=nowarn --cached -R "$index"
+    git apply --whitespace=nowarn -R "$tree"
 
     # Fix index
     # For end of file newlines we must go through the worktree
@@ -45,7 +45,7 @@ then
     # making git fail. Don't fail now: we fix the worktree first.
     if [ -s "$fixed_index" ]
     then
-        git apply -R "$fixed_index"
+        git apply --whitespace=nowarn -R "$fixed_index"
     fi
 
     # Fix worktree