Trying out opam pin-depends for supplement dependencies, so that we only need...

Trying out opam pin-depends for supplement dependencies, so that we only need the git hash in one place

.gitlab-ci.yml

@@ -136,7 +136,6 @@ build-reloc:
   before_script:
   - make builddep/coq-diaframe-reloc-cijobdep.opam
   variables:
-    OPAM_PINS: "git+https://gitlab.mpi-sws.org/iris/reloc#e904125a"
     MAKE_TARGET: "reloc"
   rules:
     - !reference [.rules_no_trigger, rules]
@@ -154,7 +153,6 @@ build-simuliris:
   before_script:
   - make builddep/coq-diaframe-simuliris-cijobdep.opam
   variables:
-    OPAM_PINS: "git+https://gitlab.mpi-sws.org/iris/simuliris#36e4daa7"
     MAKE_TARGET: "simuliris"
   rules:
     - !reference [.rules_no_trigger, rules]
@@ -203,7 +201,6 @@ build-lambda-rust:
   before_script:
   - make builddep/coq-diaframe-lambda-rust-cijobdep.opam
   variables:
-    OPAM_PINS: "git+https://gitlab.mpi-sws.org/iris/lambda-rust#ef5cb4bd"
     MAKE_TARGET: "lambda-rust"
   rules:
     - !reference [.rules_no_trigger, rules]

CoqMakefile.local

@@ -18,9 +18,9 @@ TESTFILES_HEAPLANG:=$(wildcard tests/heap_lang*.v)
 TESTFILES_BASE:=$(filter-out $(TESTFILES_HEAPLANG),$(TESTFILES))
 NORMALIZER:=tests/test-normalizer.sed
 
-# Non-Coq tests, running some shell scripts
+# Non-Coq tests, running some shell scripts. No longer used
 non-coq-tests:
-	$(HIDE)./tests/test_supplement_dependencies
+	$(HIDE)true
 
 test-base: $(TESTFILES_BASE:.v=.vo)
 

README.md

@@ -167,12 +167,10 @@ Then follow the instructions for the relevant projects below. Beware that the de
 
 #### ReLoC
 
-    opam pin add -n git+https://gitlab.mpi-sws.org/iris/reloc#e904125a
     opam pin add -k path coq-diaframe-reloc-builddep supplements/builddep
 
 #### Simuliris
 
-    opam pin add -n git+https://gitlab.mpi-sws.org/iris/simuliris#36e4daa7
     opam pin add -k path coq-diaframe-simuliris-builddep supplements/builddep
 
 #### Actris
@@ -185,7 +183,6 @@ Then follow the instructions for the relevant projects below. Beware that the de
 
 #### λ-rust
 
-    opam pin add -n git+https://gitlab.mpi-sws.org/iris/lambda-rust#ef5cb4bd
     opam pin add -k path coq-diaframe-lambda-rust-builddep supplements/builddep
 
 After this you should be able to use `make` to compile the examples:

supplements/coq-diaframe-lambda-rust.opam

@@ -10,11 +10,16 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq-diaframe" {= version}
   "coq" { = "8.18.0" }
-  "coq-lambda-rust" { = "dev.2024-02-06.0.ef5cb4bd" | = "dev.2021-10-02.0.e7857d6a" | = "~dev" }
+#  "coq-lambda-rust" { = "dev.2024-02-06.0.ef5cb4bd" | = "dev.2021-10-02.0.e7857d6a" | = "~dev" }
 ]
+pin-depends: [
+  ["coq-lambda-rust.dev" "git+https://gitlab.mpi-sws.org/iris/lambda-rust#ef5cb4bd"]
+]
+
+# ef5cb4bd is version dev.2024-02-06.0.ef5cb4bd
 
-# The weird pin to the 2021-10-02 version is to convince opam to work. In the gitlab CI,
-# we pin it explicitly to the first version. However, in the iris-dev repo there are still
+# The weird pin to the 2021-10-02 version was to convince opam to work. In the gitlab CI,
+# we pinned it explicitly to the first version. However, in the iris-dev repo there are still
 # versions of lambda-rust available, but not recent ones. Since the opam file of 
 # lambda-rust does not have a version field, opam overrides it with the last available one
 # in the iris-dev repo.

supplements/coq-diaframe-reloc.opam

@@ -10,8 +10,12 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq-diaframe" {= version}
   "coq-diaframe-heap-lang" {= version}
-  "coq-reloc" { = "dev.2024-02-02.1.e904125a" | = "~dev" }
   "coq" { = "8.18.0" }
 ]
+pin-depends: [
+  ["coq-reloc.dev" "git+https://gitlab.mpi-sws.org/iris/reloc#e904125a"]
+]
 build: [make "-j%{jobs}%" "diaframe-reloc"]
 install: [make "install-diaframe-reloc"]
+
+# e904125a is version dev.2024-02-02.1.e904125

supplements/coq-diaframe-simuliris.opam

@@ -10,7 +10,11 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
 depends: [
   "coq-diaframe" {= version}
   "coq" { = "8.18.0" }
-  "coq-simuliris" { = "dev.2024-02-06.1.36e4daa7" | = "~dev" }
+]
+pin-depends: [
+  ["coq-simuliris.dev" "git+https://gitlab.mpi-sws.org/iris/simuliris#36e4daa7"]
 ]
 build: [make "-j%{jobs}%" "diaframe-simuliris"]
 install: [make "install-diaframe-simuliris"]
+
+# 36e4daa7 is version dev.2024-02-06.1.36e4daa7

tests/test_supplement_dependencies

-#!/bin/bash
-assert_hashes_equal() {
-   SUPPLEMENT_NAME="$1"
-   CI_COMMIT_HASH="$2"
-   OPAM_COMMIT_HASH="$3"
-   README_COMMIT_HASH="$4"
-   if ! [ "$CI_COMMIT_HASH" = "$OPAM_COMMIT_HASH" ] ; then
-      echo "$SUPPLEMENT_NAME CI: $CI_COMMIT_HASH"
-      echo "$SUPPLEMENT_NAME opam: $OPAM_COMMIT_HASH"
-      echo "Detected commit hash mismatch for $SUPPLEMENT_NAME! Please update the opam file accordingly"
-      exit 1
-   fi
-   if ! [ "$CI_COMMIT_HASH" = "$README_COMMIT_HASH" ] ; then
-      echo "$SUPPLEMENT_NAME CI: $CI_COMMIT_HASH"
-      echo "$SUPPLEMENT_NAME README: $README_COMMIT_HASH"
-      echo "Detected commit hash mismatch for $SUPPLEMENT_NAME! Please update the README"
-      exit 1
-   fi
-}
-
-check_lambda_rust () {
-   CI_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/lambda-rust .gitlab-ci.yml | cut -d\" -f2 | cut -d# -f2)
-   OPAM_COMMIT_HASH=$(grep coq-lambda-rust supplements/coq-diaframe-lambda-rust.opam | cut -d= -f2 | cut -d\" -f2 | rev | cut -d. -f1 | rev)
-   README_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/lambda-rust README.md | cut -d# -f2)
-   assert_hashes_equal "λ-rust" "$CI_COMMIT_HASH" "$OPAM_COMMIT_HASH" "$README_COMMIT_HASH"
-}
-
-check_reloc () {
-   CI_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/reloc .gitlab-ci.yml | cut -d\" -f2 | cut -d# -f2)
-   OPAM_COMMIT_HASH=$(grep coq-reloc supplements/coq-diaframe-reloc.opam | cut -d= -f2 | cut -d\" -f2 | rev | cut -d. -f1 | rev)
-   README_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/reloc README.md | cut -d# -f2)
-   assert_hashes_equal "ReLoC" "$CI_COMMIT_HASH" "$OPAM_COMMIT_HASH" "$README_COMMIT_HASH"
-}
-
-check_simuliris () {
-   CI_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/simuliris .gitlab-ci.yml | cut -d\" -f2 | cut -d# -f2)
-   OPAM_COMMIT_HASH=$(grep coq-simuliris supplements/coq-diaframe-simuliris.opam | cut -d= -f2 | cut -d\" -f2 | rev | cut -d. -f1 | rev)
-   README_COMMIT_HASH=$(grep git+https://gitlab.mpi-sws.org/iris/simuliris README.md | cut -d# -f2)
-   assert_hashes_equal "Simuliris" "$CI_COMMIT_HASH" "$OPAM_COMMIT_HASH" "$README_COMMIT_HASH"
-}
-
-set -e
-check_lambda_rust
-check_reloc
-check_simuliris