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.)
---
 .gitlab-ci.yml                  |  3 +++
 Makefile.ci                     |  1 +
 dev/ci/ci-basic-overlay.sh      |  7 +++++++
 dev/ci/ci-fiat_crypto_legacy.sh | 13 +++++++++++++
 4 files changed, 24 insertions(+)
 create mode 100755 dev/ci/ci-fiat_crypto_legacy.sh

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
@@ -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
 ########################################################################
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} )
-- 
cgit v1.2.3


From 40308a1fb2c053b20fe35622e3816cba02b171c0 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2020 17:28:57 -0400
Subject: [ci] [fiat-crypto-legacy] allow_failure: true

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d9a22c5cdc..7915cc34fb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -744,6 +744,7 @@ library:ci-fiat_crypto:
 
 library:ci-fiat_crypto_legacy:
   extends: .ci-template-flambda
+  allow_failure: true # See https://github.com/coq/coq/wiki/Coq-Call-2020-06-24#adding-back-fiat-crypto-legacy
 
 # We cannot use flambda due to
 # https://github.com/ocaml/ocaml/issues/7842, see
-- 
cgit v1.2.3