fix: Also pin {coq-core, coq-stdlib, coqide-server} for coq >= 8.17

This patch happens to be necessary for coq/opam projects that depend
on coq-core (for example), and not on coq directly.

See-also: rocq-community/gaia#27 (comment)

Author: erikmd

coq/stable/Dockerfile

@@ -1,6 +1,9 @@
 ARG BASE_TAG="latest"
 FROM rocq/base:${BASE_TAG}
 
+# The following variable should be nonempty for coq >= 8.17
+ARG COQ_CORE_PINNED
+
 ARG COQ_EXTRA_OPAM="coq-bignums"
 ENV COQ_EXTRA_OPAM="${COQ_EXTRA_OPAM}"
 
@@ -18,6 +21,10 @@ RUN set -x \
   && eval $(opam env "--switch=${COMPILER}" --set-switch) \
   && opam update -y -u \
   && opam pin add -n -k version coq ${COQ_VERSION} \
+  && if [ -n "${COQ_CORE_PINNED}" ]; then \
+     opam pin add -n -k version coq-core ${COQ_VERSION};
+     opam pin add -n -k version coq-stdlib ${COQ_VERSION};
+     opam pin add -n -k version coqide-server ${COQ_VERSION}; fi \
   && opam install -y -v -j "${NJOBS}" coq ${COQ_EXTRA_OPAM} ${COQ_INSTALL_SERAPI:+coq-serapi} \
   && opam clean -a -c -s --logs \
   && chmod -R g=u /home/coq/.opam \

images.yml

@@ -56,6 +56,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: 'true'
         COQ_EXTRA_OPAM: 'coq-bignums'
         # +- coq-native
         COQ_INSTALL_SERAPI: '{matrix[base][//4.09.1-flambda/]}'
@@ -93,6 +94,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: 'true'
         COQ_EXTRA_OPAM: 'coq-native coq-bignums'
         COQ_INSTALL_SERAPI: 'true'
         # (or any nonempty string) as coq-serapi 8.20.0+_ supports ocaml 4.12.0+
@@ -147,6 +149,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: 'true'
         COQ_EXTRA_OPAM: 'coq-bignums'
         # +- coq-native
         COQ_INSTALL_SERAPI: 'true'
@@ -169,6 +172,7 @@ images:
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
         COQ_EXTRA_OPAM: 'coq-bignums'
+        COQ_CORE_PINNED: 'true'
         # +- coq-native
         COQ_INSTALL_SERAPI: 'true'
   ## coqorg/coq:8.18-native
@@ -189,6 +193,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: 'true'
         COQ_EXTRA_OPAM: 'coq-bignums'
         # +- coq-native
         COQ_INSTALL_SERAPI: 'true'
@@ -210,6 +215,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-bignums'
         # +- coq-native
         COQ_INSTALL_SERAPI: 'true'
@@ -220,6 +226,14 @@ images:
       coq: ['8.16.1']
     build:
       <<: *build_coq_stable_native
+      args:
+        BASE_TAG: 'coq_{matrix[base]}'
+        COQ_VERSION: '{matrix[coq]}'
+        VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
+        COQ_EXTRA_OPAM: 'coq-native coq-bignums'
+        COQ_INSTALL_SERAPI: 'true'
+        # (or any nonempty string) as coq-serapi 8.20.0+_ supports ocaml 4.12.0+
   ## coqorg/coq:8.15
   - matrix:
       default: ['4.07.1-flambda']
@@ -234,6 +248,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-bignums'
         COQ_INSTALL_SERAPI: '{matrix[base][//4.05.0/]}'
         # as coq-serapi does not support ocaml 4.05.0
@@ -264,6 +279,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-native coq-bignums'
         COQ_INSTALL_SERAPI: 'true'
         # (or any nonempty string) as coq-serapi supports ocaml 4.07.1
@@ -330,6 +346,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-native coq-bignums'
         COQ_INSTALL_SERAPI: '{matrix[base][//4.05.0/]}'
         # as coq-serapi does not support ocaml 4.05.0
@@ -359,6 +376,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-native coq-bignums'
         COQ_INSTALL_SERAPI: '{matrix[base][//4.05.0/]}'
         # as coq-serapi does not support ocaml 4.05.0
@@ -373,6 +391,7 @@ images:
         BASE_TAG: 'coq_{matrix[base]}'
         COQ_VERSION: '{matrix[coq]}'
         VCS_REF: 'V{matrix[coq]}'
+        COQ_CORE_PINNED: ''
         COQ_EXTRA_OPAM: 'coq-native coq-bignums'
         COQ_INSTALL_SERAPI: ''
         # as coq-serapi is not compatible with coq 8.7