From 9954d7306b288b435d930a2ea9fae9319609749b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 15 Nov 2023 12:16:34 +0100
Subject: [PATCH] Split the ci-elpi_hb makefile in two.

This would wreak havoc with the overlay files, and elpi is sensitive enough
as a plugin for this to be extremely annoying.
---
 Makefile.ci                        | 15 +++++++++++++--
 dev/ci/ci-elpi.sh                  | 16 ++++++++++++++++
 dev/ci/{ci-elpi_hb.sh => ci-hb.sh} |  7 -------
 3 files changed, 29 insertions(+), 9 deletions(-)
 create mode 100644 dev/ci/ci-elpi.sh
 rename dev/ci/{ci-elpi_hb.sh => ci-hb.sh} (70%)

diff --git a/Makefile.ci b/Makefile.ci
index 1c7453f7c70e..643ee4bb423c 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -34,8 +34,9 @@ CI_TARGETS= \
     ci-coq_tools \
     ci-coqprime \
     ci-deriving \
-    ci-elpi_hb \
+    ci-elpi \
     ci-elpi_test \
+    ci-hb \
     ci-hb_test \
     ci-engine_bench \
     ci-ext_lib \
@@ -97,7 +98,10 @@ CI_TARGETS= \
     ci-vst \
     ci-waterproof
 
-.PHONY: ci-all $(CI_TARGETS)
+CI_VIRTUAL_TARGETS= \
+    ci-elpi_hb
+
+.PHONY: ci-all $(CI_TARGETS) $(CI_VIRTUAL_TARGETS)
 
 ci-help:
 	echo '*** Coq CI system, please specify a target to build.'
@@ -135,6 +139,8 @@ ci-finmap: ci-mathcomp_1
 ci-bigenough: ci-mathcomp_1
 ci-analysis: ci-elpi_hb ci-finmap ci-bigenough
 
+ci-hb: ci-elpi
+
 ci-elpi_test: ci-elpi_hb
 ci-hb_test: ci-elpi_hb
 
@@ -167,6 +173,10 @@ ci-serapi_test: ci-mathcomp_1 ci-serapi
 
 ci-coq_lsp: ci-serapi
 
+# Virtual targets used by the CI to group compilation of rules in a single job
+
+ci-elpi_hb: ci-elpi ci-hb
+
 # Generic rule, we use make to ease CI integration
 $(CI_TARGETS): ci-%:
 	+./dev/ci/ci-wrapper.sh $*
@@ -178,6 +188,7 @@ $(CI_TARGETS): ci-%:
 NON_CI_GOALS:=$(strip $(filter-out ci-%,$(MAKECMDGOALS)))
 ifneq (,$(NON_CI_GOALS))
 $(CI_TARGETS): $(NON_CI_GOALS)
+$(CI_VIRTUAL_TARGETS): $(NON_CI_GOALS)
 endif
 
 # For emacs:
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
new file mode 100644
index 000000000000..4a9477b58ebe
--- /dev/null
+++ b/dev/ci/ci-elpi.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+set -e
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download elpi
+
+if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
+
+( cd "${CI_BUILD_DIR}/elpi"
+  make build-core
+  make build-apps
+  make install
+)
diff --git a/dev/ci/ci-elpi_hb.sh b/dev/ci/ci-hb.sh
similarity index 70%
rename from dev/ci/ci-elpi_hb.sh
rename to dev/ci/ci-hb.sh
index 0ed46f2242f0..06f3eb264da3 100644
--- a/dev/ci/ci-elpi_hb.sh
+++ b/dev/ci/ci-hb.sh
@@ -5,17 +5,10 @@ set -e
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download elpi
 git_download hierarchy_builder
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
-( cd "${CI_BUILD_DIR}/elpi"
-  make build-core
-  make build-apps
-  make install
-)
-
 ( cd "${CI_BUILD_DIR}/hierarchy_builder"
   make config
   make build