CI: build Iris examples instead of lambda-Rust

2 files changed, 24 insertions, 10 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 2725e6b56c..75d9efaadc 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -62,9 +62,17 @@
 : "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
 : "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
 
-: "${lambda_rust_CI_REF:=master}"
-: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
-: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}"
+: "${autosubst_CI_REF:=coq86-devel}"
+: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}"
+: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}"
+
+: "${iris_string_ident_CI_REF:=master}"
+: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}"
+: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}"
+
+: "${iris_examples_CI_REF:=master}"
+: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}"
+: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
diff --git a/dev/ci/ci-lambda_rust.sh b/dev/ci/ci-iris.sh
index 1ef0c2cb8f..93ec2233d3 100755
--- a/dev/ci/ci-lambda_rust.sh
+++ b/dev/ci/ci-iris.sh
@@ -3,13 +3,13 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-install_ssreflect
-
-# Setup lambda_rust first
-git_download lambda_rust
+# Setup iris_examples and separate dependencies first
+git_download autosubst
+git_download iris_string_ident
+git_download iris_examples
 
 # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup Iris
 git_download iris
@@ -26,5 +26,11 @@ git_download stdpp
 # Build and validate Iris
 ( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
 
-# Build lambda_rust
-( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install )
+# Build autosubst
+( cd "${CI_BUILD_DIR}/autosubst" && make && make install )
+
+# Build iris-string-ident
+( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install )
+
+# Build Iris examples
+( cd "${CI_BUILD_DIR}/iris_examples" && make && make install )