diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.ci | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 14 | ||||
| -rwxr-xr-x | dev/ci/ci-iris.sh (renamed from dev/ci/ci-lambda_rust.sh) | 20 |
4 files changed, 26 insertions, 12 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index cc8a4d34c9..ca5584bcb5 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -803,7 +803,7 @@ library:ci-geocoq: library:ci-hott: extends: .ci-template -library:ci-lambda_rust: +library:ci-iris: extends: .ci-template-flambda library:ci-math_classes: diff --git a/Makefile.ci b/Makefile.ci index 85e4b965f9..af78f252df 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,7 @@ CI_TARGETS= \ ci-geocoq \ ci-coqhammer \ ci-hott \ - ci-lambda_rust \ + ci-iris \ ci-math_classes \ ci-mathcomp \ ci-metacoq \ 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 ) |