[ci] function to declare projects

incidentally the "projects" array can be queried to get the list
of projects

2 files changed, 105 insertions, 186 deletions

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 18fdd83218..98c5d98240 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -1,54 +1,72 @@
 #!/usr/bin/env bash
 
-# This is the basic overlay set for repositories in the CI.
-
-# Maybe we should just use Ruby to have real objects...
-
-# : "${foo:=bar}" sets foo to "bar" if it is unset or null
+# This is the list of repositories used by the CI scripts, unless overridden
+# by a call to the "overlay" function in ci-common
+
+declare -a projects # the list of project repos that can be be overlayed
+
+# checks if the given argument is a known project
+function is_in_projects {
+    local rc=1
+    for x in ${!projects[@]}; do
+      if [ "$1" = "$x" ]; then rc=0; fi;
+    done
+    return rc
+}
+
+# project <name> <giturl> <ref> [<archiveurl>]
+#   [<archiveurl>] defaults to <giturl>/archive on github.com
+#   and <giturl>/-/archive on gitlab
+function project {
+
+  local var_ref=${1}_CI_REF
+  local var_giturl=${1}_CI_GITURL
+  local var_archiveurl=${1}_CI_ARCHIVEURL
+  local giturl=$2
+  local ref=$3
+  local archiveurl=$4
+  case $giturl in
+    *github.com*) archiveurl=${archiveurl:-$giturl/archive} ;;
+    *gitlab*) archiveurl=${archiveurl:-$giturl/-/archive} ;;
+  esac
+
+  # register the project in the list of projects
+  projects[${#projects[*]}]=$1
+
+  # bash idiom for setting a variable if not already set
+  : "${!var_ref:=$ref}"
+  : "${!var_giturl:=$giturl}"
+  : "${!var_archiveurl:=$archiveurl}"
+
+}
 
 ########################################################################
 # MathComp
 ########################################################################
-: "${mathcomp_CI_REF:=master}"
-: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}"
-: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}"
+project mathcomp "https://github.com/math-comp/math-comp" "master"
 
-: "${fourcolor_CI_REF:=master}"
-: "${fourcolor_CI_GITURL:=https://github.com/math-comp/fourcolor}"
-: "${fourcolor_CI_ARCHIVEURL:=${fourcolor_CI_GITURL}/archive}"
+project fourcolor "https://github.com/math-comp/fourcolor" "master"
 
-: "${oddorder_CI_REF:=master}"
-: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}"
-: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}"
+project oddorder "https://github.com/math-comp/odd-order" "master"
 
 ########################################################################
 # UniMath
 ########################################################################
-: "${unimath_CI_REF:=master}"
-: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}"
-: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}"
+project unimath "https://github.com/UniMath/UniMath" "master"
 
 ########################################################################
 # Unicoq + Mtac2
 ########################################################################
-: "${unicoq_CI_REF:=master}"
-: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
-: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
+project unicoq "https://github.com/unicoq/unicoq" "master"
 
-: "${mtac2_CI_REF:=master}"
-: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
-: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
+project mtac2 "https://github.com/Mtac2/Mtac2" "master"
 
 ########################################################################
 # Mathclasses + Corn
 ########################################################################
-: "${math_classes_CI_REF:=master}"
-: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}"
-: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}"
+project math_classes "https://github.com/coq-community/math-classes" "master"
 
-: "${corn_CI_REF:=master}"
-: "${corn_CI_GITURL:=https://github.com/coq-community/corn}"
-: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}"
+project corn "https://github.com/coq-community/corn" "master"
 
 ########################################################################
 # Iris
@@ -56,342 +74,238 @@
 
 # NB: stdpp and Iris refs are gotten from the opam files in the Iris
 # and lambdaRust repos respectively.
-: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
-: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
+project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" ""
 
-: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
-: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
+project iris "https://gitlab.mpi-sws.org/iris/iris" ""
 
-: "${autosubst_CI_REF:=coq86-devel}"
-: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}"
-: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}"
+project autosubst "https://github.com/RalfJung/autosubst" "coq86-devel"
 
-: "${iris_string_ident_CI_REF:=master}"
-: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}"
-: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}"
+project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master"
 
-: "${iris_examples_CI_REF:=master}"
-: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}"
-: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}"
+project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master"
 
 ########################################################################
 # HoTT
 ########################################################################
-: "${hott_CI_REF:=master}"
-: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}"
-: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}"
+project hott "https://github.com/HoTT/HoTT" "master"
 
 ########################################################################
 # CoqHammer
 ########################################################################
-: "${coqhammer_CI_REF:=master}"
-: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}"
-: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}"
+project coqhammer "https://github.com/lukaszcz/coqhammer" "master"
 
 ########################################################################
 # GeoCoq
 ########################################################################
-: "${geocoq_CI_REF:=master}"
-: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
-: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}"
+project geocoq "https://github.com/GeoCoq/GeoCoq" "master"
 
 ########################################################################
 # Flocq
 ########################################################################
-: "${flocq_CI_REF:=master}"
-: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
-: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}"
+project flocq "https://gitlab.inria.fr/flocq/flocq" "master"
 
 ########################################################################
 # coq-performance-tests
 ########################################################################
-: "${coq_performance_tests_CI_REF:=master}"
-: "${coq_performance_tests_CI_GITURL:=https://github.com/coq-community/coq-performance-tests}"
-: "${coq_performance_tests_CI_ARCHIVEURL:=${coq_performance_tests_CI_GITURL}/archive}"
+project coq_performance_tests "https://github.com/coq-community/coq-performance-tests" "master"
 
 ########################################################################
 # coq-tools
 ########################################################################
-: "${coq_tools_CI_REF:=master}"
-: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}"
-: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}"
+project coq_tools "https://github.com/JasonGross/coq-tools" "master"
 
 ########################################################################
 # Coquelicot
 ########################################################################
-: "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
-: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
+project coquelicot "https://gitlab.inria.fr/coquelicot/coquelicot" "master"
 
 ########################################################################
 # Coq-interval
 ########################################################################
-: "${interval_CI_REF:=master}"
-: "${interval_CI_GITURL:=https://gitlab.inria.fr/coqinterval/interval}"
-: "${interval_CI_ARCHIVEURL:=${interval_CI_GITURL}/-/archive}"
+project interval "https://gitlab.inria.fr/coqinterval/interval" "master"
 
 ########################################################################
 # Gappa stand alone tool
 ########################################################################
-: "${gappa_tool_CI_REF:=master}"
-: "${gappa_tool_CI_GITURL:=https://gitlab.inria.fr/gappa/gappa}"
-: "${gappa_tool_CI_ARCHIVEURL:=${gappa_tool_CI_GITURL}/-/archive}"
+project gappa_tool "https://gitlab.inria.fr/gappa/gappa" "master"
 
 ########################################################################
 # Gappa plugin
 ########################################################################
-: "${gappa_plugin_CI_REF:=master}"
-: "${gappa_plugin_CI_GITURL:=https://gitlab.inria.fr/gappa/coq}"
-: "${gappa_plugin_CI_ARCHIVEURL:=${gappa_plugin_CI_GITURL}/-/archive}"
+project gappa_plugin "https://gitlab.inria.fr/gappa/coq" "master"
 
 ########################################################################
 # CompCert
 ########################################################################
-: "${compcert_CI_REF:=master}"
-: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}"
-: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}"
+project compcert "https://github.com/AbsInt/CompCert" "master"
 
 ########################################################################
 # VST
 ########################################################################
-: "${vst_CI_REF:=master}"
-: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}"
-: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}"
+project vst "https://github.com/PrincetonUniversity/VST" "master"
 
 ########################################################################
 # cross-crypto
 ########################################################################
-: "${cross_crypto_CI_REF:=master}"
-: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}"
-: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}"
+project cross_crypto "https://github.com/mit-plv/cross-crypto" "master"
 
 ########################################################################
 # rewriter
 ########################################################################
-: "${rewriter_CI_REF:=master}"
-: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}"
-: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}"
+project rewriter "https://github.com/mit-plv/rewriter" "master"
 
 ########################################################################
 # fiat_parsers
 ########################################################################
-: "${fiat_parsers_CI_REF:=master}"
-: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}"
-: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}"
+project fiat_parsers "https://github.com/mit-plv/fiat" "master"
 
 ########################################################################
 # fiat_crypto
 ########################################################################
-: "${fiat_crypto_CI_REF:=master}"
-: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}"
-: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}"
+project fiat_crypto "https://github.com/mit-plv/fiat-crypto" "master"
 
 ########################################################################
 # 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}"
+project fiat_crypto_legacy "https://github.com/mit-plv/fiat-crypto" "sp2019latest"
 
 ########################################################################
 # coq_dpdgraph
 ########################################################################
-: "${coq_dpdgraph_CI_REF:=coq-master}"
-: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}"
-: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}"
+project coq_dpdgraph "https://github.com/Karmaki/coq-dpdgraph" "coq-master"
 
 ########################################################################
 # CoLoR
 ########################################################################
-: "${color_CI_REF:=master}"
-: "${color_CI_GITURL:=https://github.com/fblanqui/color}"
-: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}"
+project color "https://github.com/fblanqui/color" "master"
 
 ########################################################################
 # TLC
 ########################################################################
-: "${tlc_CI_REF:=master-for-coq-ci}"
-: "${tlc_CI_GITURL:=https://github.com/charguer/tlc}"
-: "${tlc_CI_ARCHIVEURL:=${tlc_CI_GITURL}/archive}"
+project tlc "https://github.com/charguer/tlc" "master-for-coq-ci"
 
 ########################################################################
 # Bignums
 ########################################################################
-: "${bignums_CI_REF:=master}"
-: "${bignums_CI_GITURL:=https://github.com/coq/bignums}"
-: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}"
+project bignums "https://github.com/coq/bignums" "master"
 
 ########################################################################
 # coqprime
 ########################################################################
-: "${coqprime_CI_REF:=master}"
-: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}"
-: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}"
+project coqprime "https://github.com/thery/coqprime" "master"
 
 ########################################################################
 # bbv
 ########################################################################
-: "${bbv_CI_REF:=master}"
-: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}"
-: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}"
+project bbv "https://github.com/mit-plv/bbv" "master"
 
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_REF:=tested}"
-: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
-: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
+project bedrock2 "https://github.com/mit-plv/bedrock2" "tested"
 
 ########################################################################
 # Equations
 ########################################################################
-: "${equations_CI_REF:=master}"
-: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}"
-: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}"
+project equations "https://github.com/mattam82/Coq-Equations" "master"
 
 ########################################################################
 # Elpi + Hierarchy Builder
 ########################################################################
-: "${elpi_CI_REF:=coq-master}"
-: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}"
-: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}"
+project elpi "https://github.com/LPCIC/coq-elpi" "coq-master"
 
-: "${elpi_hb_CI_REF:=coq-master}"
-: "${elpi_hb_CI_GITURL:=https://github.com/math-comp/hierarchy-builder}"
-: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"
+project elpi_hb "https://github.com/math-comp/hierarchy-builder" "coq-master"
 
 ########################################################################
 # Engine-Bench
 ########################################################################
-: "${engine_bench_CI_REF:=master}"
-: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}"
-: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}"
+project engine_bench "https://github.com/mit-plv/engine-bench" "master"
 
 ########################################################################
 # fcsl-pcm
 ########################################################################
-: "${fcsl_pcm_CI_REF:=master}"
-: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}"
-: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}"
+project fcsl_pcm "https://github.com/imdea-software/fcsl-pcm" "master"
 
 ########################################################################
 # ext-lib
 ########################################################################
-: "${ext_lib_CI_REF:=master}"
-: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}"
-: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}"
+project ext_lib "https://github.com/coq-community/coq-ext-lib" "master"
 
 ########################################################################
 # simple-io
 ########################################################################
-: "${simple_io_CI_REF:=master}"
-: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}"
-: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}"
+project simple_io "https://github.com/Lysxia/coq-simple-io" "master"
 
 ########################################################################
 # quickchick
 ########################################################################
-: "${quickchick_CI_REF:=master}"
-: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}"
-: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
+project quickchick "https://github.com/QuickChick/QuickChick" "master"
 
 ########################################################################
 # reduction-effects
 ########################################################################
-: "${reduction_effects_CI_REF:=master}"
-: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
-: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+project reduction_effects "https://github.com/coq-community/reduction-effects" "master"
 
 ########################################################################
 # menhirlib
 ########################################################################
 # Note: menhirlib is now in subfolder coq-menhirlib of menhir
-: "${menhirlib_CI_REF:=20201122}"
-: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}"
-: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
+project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122"
 
 ########################################################################
 # aac_tactics
 ########################################################################
-: "${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}"
+project aac_tactics "https://github.com/coq-community/aac-tactics" "master"
 
 ########################################################################
 # paramcoq
 ########################################################################
-: "${paramcoq_CI_REF:=master}"
-: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}"
-: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}"
+project paramcoq "https://github.com/coq-community/paramcoq" "master"
 
 ########################################################################
 # relation_algebra
 ########################################################################
-: "${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}"
+project relation_algebra "https://github.com/damien-pous/relation-algebra" "master"
 
 ########################################################################
 # 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}"
+project struct_tact "https://github.com/uwplse/StructTact" "master"
 
-: "${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}"
+project inf_seq_ext "https://github.com/DistributedComponents/InfSeqExt" "master"
 
-: "${cheerios_CI_REF:=master}"
-: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}"
-: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}"
+project cheerios "https://github.com/uwplse/cheerios" "master"
 
-: "${verdi_CI_REF:=master}"
-: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}"
-: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}"
+project verdi "https://github.com/uwplse/verdi" "master"
 
-: "${verdi_raft_CI_REF:=master}"
-: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}"
-: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}"
+project verdi_raft "https://github.com/uwplse/verdi-raft" "master"
 
 ########################################################################
 # stdlib2
 ########################################################################
-: "${stdlib2_CI_REF:=master}"
-: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}"
-: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}"
+project stdlib2 "https://github.com/coq/stdlib2" "master"
 
 ########################################################################
 # argosy
 ########################################################################
-: "${argosy_CI_REF:=master}"
-: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}"
-: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}"
+project argosy "https://github.com/mit-pdos/argosy" "master"
 
 ########################################################################
 # perennial
 ########################################################################
-: "${perennial_CI_REF:=coq/tested}"
-: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
-: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+project perennial "https://github.com/mit-pdos/perennial" "coq/tested"
 
 ########################################################################
 # metacoq
 ########################################################################
-: "${metacoq_CI_REF:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
-: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
+project metacoq "https://github.com/MetaCoq/metacoq" "master"
 
 ########################################################################
 # SF suite
 ########################################################################
-: "${sf_CI_REF:=master}"
-: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
-: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
+project sf "https://github.com/DeepSpec/sf" "master"
 
 ########################################################################
 # Coqtail
 ########################################################################
-: "${coqtail_CI_REF:=master}"
-: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}"
-: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}"
+project coqtail "https://github.com/whonore/Coqtail" "master"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 1a4ebc0e90..98ad834b4c 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -55,6 +55,11 @@ overlay()
     local ov_url=$2
     local ov_ref=$3
 
+    if ! is_in_projects "$1"; then
+      echo "Error: $1 is not a known project which can be overlayed"
+      exit 1
+    fi
+
     overlays[${project}_URL]=$ov_url
     overlays[${project}_REF]=$ov_ref
 }