From 5f26ee547a9976d1ccfe7cff22d886f7d7df1eef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 26 Nov 2019 15:36:56 -0500 Subject: [ci] Split out the dependencies of fiat-crypto --- .gitlab-ci.yml | 37 ++++++++++++++++++++++++++++++++++++- Makefile.ci | 6 ++++++ dev/ci/ci-basic-overlay.sh | 14 ++++++++++++++ dev/ci/ci-bedrock2.sh | 2 +- dev/ci/ci-coqprime.sh | 8 ++++++++ dev/ci/ci-fiat-crypto.sh | 5 +++-- dev/ci/ci-rewriter.sh | 8 ++++++++ 7 files changed, 76 insertions(+), 4 deletions(-) create mode 100755 dev/ci/ci-coqprime.sh create mode 100755 dev/ci/ci-rewriter.sh diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 493397adee..6afe3bd0a8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -562,7 +562,11 @@ library:ci-argosy: extends: .ci-template library:ci-bedrock2: - extends: .ci-template + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci library:ci-color: extends: .ci-template-flambda @@ -577,6 +581,19 @@ library:ci-color: library:ci-compcert: extends: .ci-template-flambda +library:ci-coqprime: + stage: stage-3 + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci + needs: + - build:edge+flambda + - plugin:ci-bignums + dependencies: + - plugin:ci-bignums + library:ci-coquelicot: extends: .ci-template @@ -588,6 +605,17 @@ library:ci-fcsl-pcm: library:ci-fiat-crypto: extends: .ci-template-flambda + stage: stage-4 + needs: + - build:edge+flambda + - library:ci-bedrock2 + - library:ci-coqprime + - plugin:ci-bignums + - plugin:ci-rewriter + dependencies: + - library:ci-bedrock2 + - library:ci-coqprime + - plugin:ci-rewriter library:ci-fiat-crypto-legacy: extends: .ci-template-flambda @@ -699,3 +727,10 @@ plugin:ci-quickchick: plugin:ci-relation_algebra: extends: .ci-template + +plugin:ci-rewriter: + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci diff --git a/Makefile.ci b/Makefile.ci index e9f7fa2db5..8315c16c64 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -19,6 +19,7 @@ CI_TARGETS= \ ci-coquelicot \ ci-corn \ ci-cross-crypto \ + ci-coqprime \ ci-elpi \ ci-ext-lib \ ci-equations \ @@ -38,6 +39,7 @@ CI_TARGETS= \ ci-perennial \ ci-quickchick \ ci-relation_algebra \ + ci-rewriter \ ci-sf \ ci-simple-io \ ci-stdlib2 \ @@ -56,10 +58,14 @@ ci-all: $(CI_TARGETS) ci-color: ci-bignums +ci-coqprime: ci-bignums + ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter + ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5139113083..de21b17f9f 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -143,6 +143,13 @@ : "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" : "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" +######################################################################## +# rewriter +######################################################################## +: "${rewriter_CI_REF:=master}" +: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}" +: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}" + ######################################################################## # fiat_parsers ######################################################################## @@ -199,6 +206,13 @@ : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" : "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" +######################################################################## +# coqprime +######################################################################## +: "${coqprime_CI_REF:=master}" +: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}" +: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" + ######################################################################## # bedrock2 ######################################################################## diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 2ac78d3c2b..8570c34194 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download bedrock2 -( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install ) diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh new file mode 100755 index 0000000000..a4fd296896 --- /dev/null +++ b/dev/ci/ci-coqprime.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqprime + +( cd "${CI_BUILD_DIR}/coqprime" && make && make install) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index eec9d50ae4..000c418137 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -10,8 +10,9 @@ git_download fiat_crypto # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 -fiat_crypto_CI_TARGETS1="standalone-ocaml c-files rust-files printlite lite" -fiat_crypto_CI_TARGETS2="all" +fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1" +fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite" +fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s 32768 && \ diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh new file mode 100755 index 0000000000..235482ffeb --- /dev/null +++ b/dev/ci/ci-rewriter.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download rewriter + +( cd "${CI_BUILD_DIR}/rewriter" && make && make install) -- cgit v1.2.3