diff options
| author | Jason Gross | 2020-06-20 21:32:58 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-06-24 11:18:47 -0400 |
| commit | f9057bd07cd553b32724593c686ca21d5d7388f2 (patch) | |
| tree | ec0673e474cbaaaf5ba7027cf1d89e0cf3e2fde1 | |
| parent | 82485e9f2a36a7a52a56622a553817436636b00b (diff) | |
Add back fiat-crypto-legacy to the CI
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca.
(I've not added back the nix things, since I'm not sure what purpose
they serve, and I've adjusted the targets slightly.)
The CI build should no longer take an enormously long time to start, and
fiat-crypto-legacy code is actively being used to track down memory
issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825,
and so I'd like to keep f-c-l in the CI at least until #7825 is
finished.
I've been maintaining compatibility of f-c-l with master anyway on the
side, in part to continue some performance experiments with it, and
expect to continue to do so at least until the end of this calendar
year, and it'd be nice for me to get advance warning when a PR is going
to break it on master. (It seems reasonable to me to take it off the CI
again once I'm no longer maintaining it / collecting data from it, and /
or once #7825 is finished.)
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat_crypto_legacy.sh | 13 |
4 files changed, 24 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f6c035553c..d9a22c5cdc 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -742,6 +742,9 @@ library:ci-fiat_crypto: - library:ci-coqprime - plugin:ci-rewriter +library:ci-fiat_crypto_legacy: + extends: .ci-template-flambda + # We cannot use flambda due to # https://github.com/ocaml/ocaml/issues/7842, see # https://github.com/coq/coq/pull/11916#issuecomment-609977375 diff --git a/Makefile.ci b/Makefile.ci index 07f06caa3a..77d8bda671 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,6 +29,7 @@ CI_TARGETS= \ ci-equations \ ci-fcsl_pcm \ ci-fiat_crypto \ + ci-fiat_crypto_legacy \ ci-fiat_crypto_ocaml \ ci-fiat_parsers \ ci-flocq \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 88471a92aa..4973cbb478 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -179,6 +179,13 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## +# fiat_crypto_legacy +######################################################################## +: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" +: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" + +######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh new file mode 100755 index 0000000000..6d0a803401 --- /dev/null +++ b/dev/ci/ci-fiat_crypto_legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto_legacy + +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display" + +( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ + make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) |