diff options
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
| -rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 1af0f634c4..6960a8b98a 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -3,32 +3,28 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp" -Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq" -lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust" - install_ssreflect # Setup lambdaRust first -git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" +git_download lambdaRust # Extract required version of Iris -Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" +git_download Iris # Extract required version of std++ -stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" +git_download stdpp # Build std++ -( cd "${stdpp_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) -# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris -( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install ) +# Build and validate Iris +( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) # Build lambdaRust -( cd "${lambdaRust_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) |