Merge PR #9018: [devtools] Small script to setup overlays automatically

32 files changed, 126 insertions, 184 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1c5c8efc19..7dda19192d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -362,7 +362,7 @@ validate:edge+flambda:
     OPAM_SWITCH: edge
     OPAM_VARIANT: "+flambda"
 
-ci-aac-tactics:
+ci-aac_tactics:
   <<: *ci-template
 
 ci-bedrock2:
@@ -378,7 +378,7 @@ ci-color:
 ci-compcert:
   <<: *ci-template-flambda
 
-ci-coq-dpdgraph:
+ci-coq_dpdgraph:
   <<: *ci-template
 
 ci-coquelicot:
@@ -438,7 +438,7 @@ ci-paramcoq:
 ci-pidetop:
   <<: *ci-template
 
-ci-plugin-tutorial:
+ci-plugin_tutorial:
   <<: *ci-template
 
 ci-quickchick:
diff --git a/Makefile.ci b/Makefile.ci
index e8fea11bdb..88ea64974a 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -9,12 +9,12 @@
 ##########################################################################
 
 CI_TARGETS= \
-    ci-aac-tactics \
+    ci-aac_tactics \
     ci-bedrock2 \
     ci-bignums \
     ci-color \
     ci-compcert \
-    ci-coq-dpdgraph \
+    ci-coq_dpdgraph \
     ci-coquelicot \
     ci-corn \
     ci-cpdt \
@@ -38,7 +38,7 @@ CI_TARGETS= \
     ci-mtac2 \
     ci-paramcoq \
     ci-pidetop \
-    ci-plugin-tutorial \
+    ci-plugin_tutorial \
     ci-quickchick \
     ci-sf \
     ci-simple-io \
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 71207bb040..0dcabc0b97 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1645,7 +1645,7 @@ function make_addon_bignums {
 
 function make_addon_equations {
   installer_addon_dependency equations
-  if build_prep_overlay Equations; then
+  if build_prep_overlay equations; then
     installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" ""
     # Note: PATH is automatically saved/restored by build_prep / build_post
     PATH=$COQBIN:$PATH
diff --git a/dev/ci/ci-aac-tactics.sh b/dev/ci/ci-aac-tactics.sh
deleted file mode 100755
index 896a0ddf66..0000000000
--- a/dev/ci/ci-aac-tactics.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download aactactics
-
-( cd "${CI_BUILD_DIR}/aactactics" && make && make install )
diff --git a/dev/ci/ci-aac_tactics.sh b/dev/ci/ci-aac_tactics.sh
new file mode 100755
index 0000000000..19f1f43746
--- /dev/null
+++ b/dev/ci/ci-aac_tactics.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download aac_tactics
+
+( cd "${CI_BUILD_DIR}/aac_tactics" && make && make install )
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3137576207..4d5834eeb6 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -113,16 +113,16 @@
 ########################################################################
 # CompCert
 ########################################################################
-: "${CompCert_CI_REF:=master}"
-: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}"
-: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}"
+: "${compcert_CI_REF:=master}"
+: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}"
+: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}"
 
 ########################################################################
 # VST
 ########################################################################
-: "${VST_CI_REF:=master}"
-: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}"
-: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}"
+: "${vst_CI_REF:=master}"
+: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}"
+: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}"
 
 ########################################################################
 # cross-crypto
@@ -153,7 +153,7 @@
 : "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}"
 
 ########################################################################
-# coq-dpdgraph
+# coq_dpdgraph
 ########################################################################
 : "${coq_dpdgraph_CI_REF:=coq-master}"
 : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}"
@@ -162,9 +162,9 @@
 ########################################################################
 # CoLoR
 ########################################################################
-: "${CoLoR_CI_REF:=master}"
-: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}"
-: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}"
+: "${color_CI_REF:=master}"
+: "${color_CI_GITURL:=https://github.com/fblanqui/color}"
+: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}"
 
 ########################################################################
 # SF
@@ -196,16 +196,16 @@
 ########################################################################
 # Equations
 ########################################################################
-: "${Equations_CI_REF:=master}"
-: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}"
-: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}"
+: "${equations_CI_REF:=master}"
+: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}"
+: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}"
 
 ########################################################################
 # Elpi
 ########################################################################
-: "${Elpi_CI_REF:=coq-master}"
-: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
-: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}"
+: "${elpi_CI_REF:=coq-master}"
+: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
+: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}"
 
 ########################################################################
 # fcsl-pcm
@@ -257,11 +257,11 @@
 : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
 
 ########################################################################
-# aac-tactics
+# aac_tactics
 ########################################################################
-: "${aactactics_CI_REF:=master}"
-: "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
-: "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}"
+: "${aac_tactics_CI_REF:=master}"
+: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}"
+: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}"
 
 ########################################################################
 # paramcoq
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index dc696f69d9..a0094b1006 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download CoLoR
+git_download color
 
-( cd "${CI_BUILD_DIR}/CoLoR" && make )
+( cd "${CI_BUILD_DIR}/color" && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 7a450d0d48..a5aa54144c 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -46,8 +46,11 @@ for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
     . "${overlay}"
 done
+
+set +x
 # shellcheck source=ci-basic-overlay.sh
 . "${ci_dir}/ci-basic-overlay.sh"
+set -x
 
 # [git_download project] will download [project] and unpack it
 # in [$CI_BUILD_DIR/project] if the folder does not exist already;
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 01c35ceb4a..59a85e4726 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -3,7 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download CompCert
+git_download compcert
 
-( cd "${CI_BUILD_DIR}/CompCert" && \
+( cd "${CI_BUILD_DIR}/compcert" && \
   ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq_dpdgraph.sh
index 2373ea6c62..2373ea6c62 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq_dpdgraph.sh
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index 9b4a06fd5b..d60bf34ba2 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Elpi
+git_download elpi
 
-( cd "${CI_BUILD_DIR}/Elpi" && make && make install )
+( cd "${CI_BUILD_DIR}/elpi" && make && make install )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 998d50faa7..b58a794da2 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -3,7 +3,7 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Equations
+git_download equations
 
-( cd "${CI_BUILD_DIR}/Equations" && coq_makefile -f _CoqProject -o Makefile && \
+( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \
   make && make test-suite && make examples && make install)
diff --git a/dev/ci/ci-plugin-tutorial.sh b/dev/ci/ci-plugin_tutorial.sh
index 6c26a71a21..6c26a71a21 100755
--- a/dev/ci/ci-plugin-tutorial.sh
+++ b/dev/ci/ci-plugin_tutorial.sh
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 0fec19205a..169d1a41db 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download VST
+git_download vst
 
-( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true )
+( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
deleted file mode 100644
index d812df3ec0..0000000000
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
-    mathcomp_CI_REF=ssr-merge
-    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp
-fi
diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
deleted file mode 100644
index 575df07425..0000000000
--- a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-_OVERLAY_BRANCH=pure-sharing-flag
-
-if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
-    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
deleted file mode 100644
index 019cb8054d..0000000000
--- a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then
-    cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification
-    cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto
-fi
diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
deleted file mode 100644
index 3a6480a5a1..0000000000
--- a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then
-
-    ltac2_CI_BRANCH=master+globenv-coq-pr7288
-    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/08456-fix-6764.sh b/dev/ci/user-overlays/08456-fix-6764.sh
deleted file mode 100644
index 3b951d9c07..0000000000
--- a/dev/ci/user-overlays/08456-fix-6764.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8456" ] || [ "$CI_BRANCH" = "fix-6764" ]; then
-    Elpi_CI_REF=overlay/8456
-fi
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
deleted file mode 100755
index 4605255d5e..0000000000
--- a/dev/ci/user-overlays/08515-command-atts.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
-    ltac2_CI_REF=command-atts
-    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
-
-    Equations_CI_REF=command-atts
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    plugin_tutorial_CI_REF=command-atts
-    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
-fi
diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh
deleted file mode 100644
index c08f44fc50..0000000000
--- a/dev/ci/user-overlays/08552-gares-elpi-11.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then
-    Elpi_CI_REF=coq-master-elpi-1.1
-fi
diff --git a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh b/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
deleted file mode 100644
index 484ad8f9e6..0000000000
--- a/dev/ci/user-overlays/08554-herbelin-master+fix8553-change-under-binders.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8554" ] || [ "$CI_BRANCH" = "master+fix8553-change-under-binders" ]; then
-
-    ltac2_CI_BRANCH=master+fix-pr8554-change-takes-env
-    ltac2_CI_REF=master+fix-pr8554-change-takes-env
-    ltac2_CI_GITURL=https://github.com/herbelin/ltac2
-
-    Equations_CI_BRANCH=master+fix-pr8554-change-takes-env
-    Equations_CI_REF=master+fix-pr8554-change-takes-env
-    Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh b/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
deleted file mode 100644
index 41c2ad6fef..0000000000
--- a/dev/ci/user-overlays/08555-maximedenes-rm-section-path.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8555" ] || [ "$CI_BRANCH" = "rm-section-path" ]; then
-
-    ltac2_CI_REF=rm-section-path
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    Equations_CI_REF=rm-section-path
-    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
deleted file mode 100644
index 9d723dc7f2..0000000000
--- a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-_OVERLAY_BRANCH=name-abstract-univ-context
-
-if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    Elpi_CI_REF="$_OVERLAY_BRANCH"
-    Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
-
-    Equations_CI_REF="$_OVERLAY_BRANCH"
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
deleted file mode 100644
index bd3e1bf7ff..0000000000
--- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then
-    plugin_tutorial_CI_REF=pr8671-fix
-    plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
-
-fi
diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
deleted file mode 100644
index 98530c825a..0000000000
--- a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then
-
-    Elpi_CI_REF=kernel-entries-cleanup
-    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
-
-    Equations_CI_REF=kernel-entries-cleanup
-    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
deleted file mode 100644
index 81ed91f52b..0000000000
--- a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
-
-    Elpi_CI_REF=master+generalized-evar-printers-pr8688
-    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
deleted file mode 100644
index b3a9f67e00..0000000000
--- a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
-
-    # ltac2_CI_REF=rm-section-path
-    # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    plugin_tutorial_CI_REF=vernac+monify_hook
-    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
-
-    Elpi_CI_REF=vernac+monify_hook
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-    Equations_CI_REF=vernac+monify_hook
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
deleted file mode 100644
index 4536c62c64..0000000000
--- a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-_OVERLAY_BRANCH=rm-implicit-tactic
-
-if [ "$CI_PULL_REQUEST" = "8779" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    ltac2_CI_REF="$_OVERLAY_BRANCH"
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-fi
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh
deleted file mode 100644
index 8ad8cba243..0000000000
--- a/dev/ci/user-overlays/08844-split-tactics.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then
-    Equations_CI_REF=split-tactics
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-
-    ltac2_CI_REF=split-tactics
-    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
-
-    fiat_parsers_CI_REF=split-tactics
-    fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat
-fi
diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
deleted file mode 100644
index 76aa37d380..0000000000
--- a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh
+++ /dev/null
@@ -1,5 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then
-    HoTT_CI_REF=fix-for-numeral-notations
-    HoTT_CI_GITURL=https://github.com/JasonGross/HoTT
-    HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive
-fi
diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh
new file mode 100755
index 0000000000..314ac07e68
--- /dev/null
+++ b/dev/tools/create_overlays.sh
@@ -0,0 +1,78 @@
+#!/usr/bin/env bash
+
+# TODO:
+#
+# - Check if the branch already exists in the remote => checkout
+# - Better error handling
+# - Just checkout, don't build
+# - Rebase functionality
+#
+
+set -x
+set -e
+set -o pipefail
+
+# setup_contrib_git("_build_ci/fiat", "https://github.com/ejgallego/fiat-core.git")
+setup_contrib_git() {
+
+    local _DIR=$1
+    local _GITURL=$2
+
+    ( cd $_DIR
+      git checkout -b $OVERLAY_BRANCH         || true # allow the branch to exist already
+      git remote add $DEVELOPER_NAME $_GITURL || true # allow the remote to exist already
+    )
+
+}
+
+if [ $# -lt 3 ]; then
+  echo "usage: $0 github_username pr_number contrib1 ... contribN"
+  exit 1
+fi
+
+set +x
+. dev/ci/ci-basic-overlay.sh
+set -x
+
+DEVELOPER_NAME=$1
+shift
+PR_NUMBER=$1
+shift
+OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD)
+OVERLAY_FILE=$(mktemp overlay-XXXX)
+
+# Create the overlay file
+printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then \n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE"
+
+# We first try to build the contribs
+while test $# -gt 0
+do
+    _CONTRIB_NAME=$1
+    _CONTRIB_GITURL=${_CONTRIB_NAME}_CI_GITURL
+    _CONTRIB_GITURL=${!_CONTRIB_GITURL}
+    echo "Processing Contrib $_CONTRIB_NAME"
+
+    # check _CONTRIB_GIT exists and it is of the from github...
+
+    _CONTRIB_DIR=_build_ci/$_CONTRIB_NAME
+
+    # extract the relevant part of the repository
+    _CONTRIB_GITSUFFIX=${_CONTRIB_GITURL#https://github.com/*/}
+    _CONTRIB_GITURL="https://github.com/$DEVELOPER_NAME/$_CONTRIB_GITSUFFIX"
+    _CONTRIB_GITPUSHURL="git@github.com:$DEVELOPER_NAME/${_CONTRIB_GITSUFFIX}.git"
+
+    # This should work better: for example we should be able not to
+    # build but just to checkout.
+    make ci-$_CONTRIB_NAME || true
+    setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL
+
+    echo "    ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE
+    echo "    ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE
+    echo "" >> $OVERLAY_FILE
+    shift
+done
+
+# End the file; copy to overlays folder.
+echo "fi" >> $OVERLAY_FILE
+PR_NUMBER=$(printf '%05d' "$PR_NUMBER")
+mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-$OVERLAY_BRANCH.sh