8 files changed, 68 insertions, 43 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index fa8962a06f..6663fbecf8 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -10,12 +10,14 @@ We are currently running tests on the following platforms:
 - GitLab CI is the main CI platform. It tests the compilation of Coq,
   of the documentation, and of CoqIDE on Linux with several versions
   of OCaml and with warnings as errors; it runs the test-suite and
-  tests the compilation of several external developments.
+  tests the compilation of several external developments. It also runs
+  a linter that checks whitespace discipline. A [pre-commit
+  hook](../tools/pre-commit) is automatically installed by
+  `./configure`. It should allow complying with this discipline
+  without pain.
 
 - Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS. It also runs a linter that checks whitespace discipline. A
-  [pre-commit hook](../tools/pre-commit) is automatically installed by
-  `./configure`. It should allow complying with this discipline without pain.
+  macOS.
 
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index e0f4f50fa9..8dee465cf4 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -150,11 +150,11 @@
 : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
 
 ########################################################################
-# formal-topology
+# fiat_crypto_legacy
 ########################################################################
-: "${formal_topology_CI_REF:=ci}"
-: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}"
-: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}"
+: "${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
@@ -240,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}"
@@ -273,3 +266,26 @@
 : "${relation_algebra_CI_REF:=master}"
 : "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}"
 : "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}"
+
+########################################################################
+# StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft
+########################################################################
+: "${struct_tact_CI_REF:=master}"
+: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}"
+: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}"
+
+: "${inf_seq_ext_CI_REF:=master}"
+: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}"
+: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}"
+
+: "${cheerios_CI_REF:=master}"
+: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}"
+: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}"
+
+: "${verdi_CI_REF:=master}"
+: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}"
+: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}"
+
+: "${verdi_raft_CI_REF:=master}"
+: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
+: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
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-formal-topology.sh b/dev/ci/ci-formal-topology.sh
deleted file mode 100755
index 8be5a06ed2..0000000000
--- a/dev/ci/ci-formal-topology.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download formal_topology
-
-( cd "${CI_BUILD_DIR}/formal_topology" && make )
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/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh
new file mode 100755
index 0000000000..3bcd52c464
--- /dev/null
+++ b/dev/ci/ci-verdi-raft.sh
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download struct_tact
+
+( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install )
+
+git_download inf_seq_ext
+
+( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install )
+
+git_download cheerios
+
+( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install )
+
+git_download verdi
+
+( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install )
+
+git_download verdi_raft
+
+( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make )
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 386a3de204..5f819f31f9 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -26,12 +26,12 @@ if %ARCH% == 64 (
 
 SET CYGROOT=C:\ci\cygwin%ARCH%
 SET DESTCOQ=C:\ci\coq%ARCH%
+SET CYGCACHE=C:\ci\cache\cgwin
 
 CALL :MakeUniqueFolder %CYGROOT% CYGROOT
 CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
 
 powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')"
-SET CYGCACHE=%CYGROOT%\var\cache\setup
 SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/%
 SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
 SET COQREGTESTING=Y
@@ -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= "
 )