aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-cross-crypto.sh11
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile2
-rwxr-xr-xdev/ci/docker/bionic_coq/hooks/post_push2
4 files changed, 19 insertions, 2 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 1ae2ad0acb..b7faea13ed 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -91,6 +91,12 @@
: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}"
########################################################################
+# cross-crypto
+########################################################################
+: "${cross_crypto_CI_BRANCH:=master}"
+: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}"
+
+########################################################################
# fiat_parsers
########################################################################
: "${fiat_parsers_CI_BRANCH:=master}"
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh
new file mode 100755
index 0000000000..a0d3aa6551
--- /dev/null
+++ b/dev/ci/ci-cross-crypto.sh
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto"
+
+git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}"
+( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive )
+
+( cd "${cross_crypto_CI_DIR}" && make )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 9201001574..689d203a16 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -43,4 +43,4 @@ RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
# BE+flambda switch
RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
- opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+ opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
index 6daf337a72..307680aa51 100755
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -1,6 +1,6 @@
#!/usr/bin/env bash
-COQCI_VERSION=V2018-05-07
+COQCI_VERSION=V2018-05-07-V2
docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
docker push $DOCKER_REPO:$COQCI_VERSION