[devtools] Small script to setup overlays automatically

This is very preliminary but you should get the idea. The script tries
to build contribs, then creates a branch and sets the remote properly
as to submit a PR.

Usage example:
```
./dev/tools/create_overlays.sh ejgallego 9999 ltac2 elpi
```

This only works for contributions hosted in github for now.

3 files changed, 82 insertions, 1 deletions

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-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/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