##########################################################################
##         #      The Rocq Prover / The Rocq Development Team           ##
##  v      #         Copyright INRIA, CNRS and contributors             ##
## <O___,, # (see version control and CREDITS file for authors & dates) ##
##   \VV/  ###############################################################
##    //   #    This file is distributed under the terms of the         ##
##         #     GNU Lesser General Public License Version 2.1          ##
##         #     (see LICENSE file for the text of the license)         ##
##########################################################################

CI_PLATFORM_FULL= \
    ci-itauto \
    ci-aac_tactics \
    ci-bignums \
    ci-coq_dpdgraph \
    ci-coquelicot \
    ci-corn \
    ci-coqprime \
    ci-elpi \
    ci-hb \
    ci-ext_lib \
    ci-equations \
    ci-flocq \
    ci-coqhammer \
    ci-hott \
    ci-iris \
    ci-math_classes \
    ci-mathcomp \
    ci-mathcomp_word \
    ci-mczify \
    ci-finmap \
    ci-bigenough \
    ci-analysis \
    ci-analysis_stdlib \
    ci-menhir \
    ci-mtac2 \
    ci-paramcoq \
    ci-quickchick \
    ci-reduction_effects \
    ci-relation_algebra \
    ci-simple_io \
    ci-stdlib \
    ci-unicoq

CI_TARGETS:=$(filter-out ci-common,$(patsubst dev/ci/scripts/%.sh,%,$(wildcard dev/ci/scripts/ci-*.sh)))

CI_VIRTUAL_TARGETS= \
    ci-elpi_hb \
    ci-platform_full

.PHONY: ci-all ci-update ci-reset $(CI_TARGETS) $(CI_VIRTUAL_TARGETS)

ci-help:
	echo '*** Coq CI system, please specify a target to build.'
	false

ci-all: $(CI_TARGETS)

ci-argosy: ci-stdlib

ci-atbr: ci-stdlib

ci-bignums: ci-stdlib

ci-category_theory: ci-equations

ci-coinduction: ci-stdlib

ci-color: ci-bignums

ci-lean_importer: ci-stdlib

ci-mathcomp: ci-elpi_hb ci-micromega

ci-coqprime: ci-bignums
ci-coquelicot: ci-mathcomp ci-stdlib
ci-deriving: ci-mathcomp ci-stdlib
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-elpi

ci-mtac2: ci-unicoq ci-stdlib

ci-coqutil: ci-stdlib
ci-rewriter: ci-stdlib
ci-bedrock2: ci-coqutil
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-coqprime
ci-fiat_crypto_ocaml: ci-fiat_crypto
ci-fiat_parsers: ci-stdlib

ci-fourcolor: ci-mathcomp
ci-oddorder: ci-mathcomp
ci-fcsl_pcm: ci-mathcomp ci-stdlib
ci-mczify: ci-mathcomp ci-stdlib
ci-mathcomp_test: ci-mathcomp
ci-mathcomp_word: ci-mathcomp ci-stdlib
ci-finmap: ci-mathcomp
ci-bigenough: ci-mathcomp
ci-analysis: ci-elpi_hb ci-finmap ci-bigenough
ci-analysis_stdlib: ci-analysis ci-stdlib

ci-hb: ci-elpi

ci-elpi_test: ci-elpi ci-stdlib
ci-hb_test: ci-hb

ci-trakt: ci-elpi ci-stdlib

ci-engine_bench: ci-stdlib

ci-ext_lib: ci-stdlib

ci-itauto: ci-stdlib

ci-jasmin: ci-mathcomp_word ci-itree

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-equations: ci-stdlib
ci-equations_test: ci-equations

ci-flocq: ci-stdlib

ci-menhir: ci-stdlib

ci-metarocq: ci-equations ci-ext_lib

ci-neural_net_interp: ci-stdlib

ci-vst: ci-compcert

ci-compcert: ci-menhir ci-flocq

ci-paramcoq: ci-stdlib

ci-aac_tactics: ci-stdlib
ci-relation_algebra: ci-aac_tactics ci-mathcomp

ci-rocq_lsp: ci-stdlib

ci-sf: ci-stdlib

ci-smtcoq: ci-stdlib ci-trakt

ci-stalmarck: ci-stdlib

ci-stdlib_test: ci-stdlib
ci-stdlib_doc: ci-stdlib

ci-waterproof: ci-stdlib

ci-refman: ci-mathcomp ci-mczify

# Virtual targets used by the CI to group compilation of rules in a single job

ci-elpi_hb: ci-elpi ci-hb

ci-platform_full: $(CI_PLATFORM_FULL)

# Generic rule, we use make to ease CI integration
$(CI_TARGETS): ci-%:
	+./dev/ci/ci-wrapper.sh $*

# Helper to update all CI repositories already downloaded
ci-update:
	./dev/ci/ci-update.sh

# Helper to reset all CI repositories already downloaded
ci-reset:
	./dev/ci/ci-reset.sh

# if we do eg "make states ci-foo", ci-foo will wait for states
# if we just do "make ci-foo" it will just run ci-foo
# (technically the ci-* targets depend on world but it can be
# convenient to run them with less than world compiled)
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:
# Local Variables:
# mode: makefile
# End: