From f9057bd07cd553b32724593c686ca21d5d7388f2 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 20 Jun 2020 21:32:58 -0400
Subject: 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.)
---
 dev/ci/ci-basic-overlay.sh | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev/ci/ci-basic-overlay.sh')

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
@@ -178,6 +178,13 @@
 : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
 : "${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
 ########################################################################
-- 
cgit v1.2.3