From c58dcb75741420e7868593a22fafda112f9c7be9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 30 Oct 2024 16:46:07 +0100
Subject: [PATCH] [CI] Retrieve local CI

---
 Makefile    |  2 ++
 Makefile.ci | 80 ++---------------------------------------------------
 2 files changed, 4 insertions(+), 78 deletions(-)

diff --git a/Makefile b/Makefile
index 94e9b3c141..a78ff1b309 100644
--- a/Makefile
+++ b/Makefile
@@ -13,3 +13,5 @@ refman-html:
 
 stdlib-html:
 	dune build --root . @stdlib-html
+
+include Makefile.ci
diff --git a/Makefile.ci b/Makefile.ci
index d181198de4..6dbb588a33 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -22,7 +22,6 @@ CI_PLATFORM_FULL= \
     ci-equations \
     ci-flocq \
     ci-coqhammer \
-    ci-hott \
     ci-iris \
     ci-math_classes \
     ci-mathcomp \
@@ -35,10 +34,8 @@ CI_PLATFORM_FULL= \
     ci-mtac2 \
     ci-paramcoq \
     ci-quickchick \
-    ci-reduction_effects \
     ci-relation_algebra \
     ci-simple_io \
-    ci-stdlib \
     ci-unicoq
 
 CI_TARGETS= \
@@ -56,10 +53,8 @@ CI_TARGETS= \
     ci-coinduction \
     ci-color \
     ci-compcert \
-    ci-coqtail \
     ci-coqutil \
     ci-cross_crypto \
-    ci-coq_lsp \
     ci-coq_performance_tests \
     ci-coq_tools \
     ci-deriving \
@@ -70,7 +65,6 @@ CI_TARGETS= \
     ci-fcsl_pcm \
     ci-fiat_crypto \
     ci-fiat_crypto_legacy \
-    ci-fiat_crypto_ocaml \
     ci-fiat_parsers \
     ci-fourcolor \
     ci-http \
@@ -79,8 +73,6 @@ CI_TARGETS= \
     ci-jasmin \
     ci-json \
     ci-kami \
-    ci-lean_importer \
-    ci-ltac2_compiler \
     ci-mathcomp_test \
     ci-metacoq \
     ci-neural_net_interp \
@@ -89,25 +81,19 @@ CI_TARGETS= \
     ci-parsec \
     ci-perennial \
     ci-quickchick_test \
-    ci-refman \
     ci-rewriter \
     ci-riscv_coq \
     ci-rupicola \
-    ci-serapi \
-    ci-serapi_test \
     ci-sf \
     ci-smtcoq \
     ci-smtcoq_trakt \
     ci-stalmarck \
     ci-stdlib_doc \
     ci-stdlib_test \
-    ci-stdlib2 \
     ci-tactician \
     ci-tlc \
     ci-trakt \
-    ci-unimath \
     ci-verdi_raft \
-    ci-vscoq \
     ci-vst \
     ci-waterproof
 
@@ -123,18 +109,8 @@ ci-help:
 
 ci-all: $(CI_TARGETS)
 
-ci-argosy: ci-stdlib
-
-ci-atbr: ci-stdlib
-
-ci-bbv: ci-stdlib
-
-ci-bignums: ci-stdlib
-
 ci-category_theory: ci-equations
 
-ci-coinduction: ci-stdlib
-
 ci-color: ci-bignums
 
 ci-mathcomp: ci-elpi_hb
@@ -144,31 +120,16 @@ ci-coquelicot: ci-mathcomp
 ci-deriving: ci-mathcomp
 ci-math_classes: ci-bignums
 
-ci-coqhammer: ci-stdlib
-
-ci-coq_dpdgraph: ci-stdlib
-
-ci-coq_performance_tests: ci-stdlib
-
-ci-coq_tools: ci-stdlib
-
 ci-corn: ci-math_classes
 
-ci-cross_crypto: ci-stdlib
+ci-mtac2: ci-unicoq
 
-ci-mtac2: ci-unicoq ci-stdlib
-
-ci-coqutil: ci-stdlib
-ci-kami: ci-stdlib
-ci-rewriter: ci-stdlib
 ci-riscv_coq: ci-coqutil
 ci-bedrock2: ci-coqutil ci-riscv_coq ci-kami
 ci-bedrock2_examples: ci-bedrock2
 ci-rupicola: ci-bedrock2 ci-coqutil
 ci-fiat_crypto: ci-coqprime ci-rewriter ci-bedrock2 ci-coqutil ci-rupicola
-ci-fiat_crypto_legacy: ci-stdlib
 ci-fiat_crypto_ocaml: ci-fiat_crypto
-ci-fiat_parsers: ci-stdlib
 
 ci-fourcolor: ci-mathcomp
 ci-oddorder: ci-mathcomp
@@ -182,76 +143,39 @@ ci-analysis: ci-elpi_hb ci-finmap ci-bigenough
 
 ci-hb: ci-elpi
 
-ci-elpi: ci-stdlib
 ci-elpi_test: ci-elpi
 ci-hb_test: ci-hb
 
 ci-trakt: ci-elpi
 
-ci-engine_bench: ci-stdlib
-
-ci-ext_lib: ci-stdlib
-
-ci-itauto: ci-stdlib
-
 ci-jasmin: ci-mathcomp_word
 
-ci-autosubst: ci-stdlib
 ci-iris: ci-autosubst
 
 ci-simple_io: ci-ext_lib
 ci-quickchick: ci-ext_lib ci-simple_io ci-mathcomp
 ci-quickchick_test: ci-quickchick
-ci-paco: ci-stdlib
 ci-itree: ci-ext_lib ci-paco
 ci-itree_io: ci-itree ci-simple_io
 
-ci-ceres: ci-stdlib
 ci-parsec: ci-ext_lib ci-ceres
 ci-json: ci-parsec ci-menhir
 ci-async_test: ci-itree_io ci-json ci-quickchick
 ci-http: ci-async_test
 
-ci-equations: ci-stdlib
 ci-equations_test: ci-equations
 
-ci-flocq: ci-stdlib
-
-ci-menhir: ci-stdlib
-
 ci-metacoq: ci-equations
 
-ci-neural_net_interp: ci-stdlib
-
 ci-vst: ci-compcert
 
 ci-compcert: ci-menhir ci-flocq
 
-ci-paramcoq: ci-stdlib
-
-ci-perennial: ci-stdlib
-
-ci-aac_tactics: ci-stdlib
 ci-relation_algebra: ci-aac_tactics ci-mathcomp
 
 ci-serapi: ci-coq_lsp
-ci-coq_lsp: ci-stdlib
-
-ci-sf: ci-stdlib
-
-ci-smtcoq: ci-stdlib
-ci-smtcoq_trakt: ci-stdlib ci-trakt
-
-ci-stalmarck: ci-stdlib
-
-ci-stdlib_test: ci-stdlib
-ci-stdlib_doc: ci-stdlib
-
-ci-tlc: ci-stdlib
-
-ci-verdi_raft: ci-stdlib
 
-ci-waterproof: ci-stdlib
+ci-smtcoq_trakt: ci-trakt
 
 ci-refman: ci-platform_full