5 files changed, 17 insertions, 26 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e74a7853b9..8dee465cf4 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -150,6 +150,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}"
@@ -233,13 +240,6 @@
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
-# plugin_tutorial
-########################################################################
-: "${plugin_tutorial_CI_REF:=master}"
-: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
-: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
-
-########################################################################
 # menhirlib
 ########################################################################
 : "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 6bf3138346..2af4b58201 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -4,11 +4,11 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 FORCE_GIT=1
-git_download fiat_crypto
+git_download fiat_crypto_legacy
 
 fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
 
-( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
+( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   ./etc/ci/remove_autogenerated.sh && \
   make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 7e8013be9b..bba17314f7 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -10,5 +10,9 @@ git_download fiat_crypto
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
 
+fiat_crypto_CI_TARGETS1="c-files printlite lite"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem"
+
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
-  ulimit -s 32768 && make new-pipeline c-files )
+        ulimit -s 32768 && \
+        make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh
deleted file mode 100755
index 6c26a71a21..0000000000
--- a/dev/ci/ci-plugin_tutorial.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download plugin_tutorial
-
-( cd "${CI_BUILD_DIR}/plugin_tutorial" && \
-  pushd tuto0 && make && popd          && \
-  pushd tuto1 && make && popd          && \
-  pushd tuto2 && make && popd          && \
-  pushd tuto3 && make && popd          )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 386a3de204..2a42a6b58e 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=compcert ^
     -addon=extlib ^
     -addon=quickchick ^
-    -addon=coquelicot
-  REM addons with build issues
-  REM -addon=vst ^
-  REM -addon=aactactics ^
+    -addon=coquelicot ^
+    -addon=vst ^
+    -addon=aactactics
 ) ELSE (
   SET "EXTRA_ADDONS= "
 )