Makefile.ci

##########################################################################
##         #      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-iris \
    ci-math_classes \
    ci-mathcomp \
    ci-mathcomp_word \
    ci-mczify \
    ci-finmap \
    ci-bigenough \
    ci-analysis \
    ci-menhir \
    ci-mtac2 \
    ci-paramcoq \
    ci-quickchick \
    ci-relation_algebra \
    ci-simple_io \
    ci-unicoq

CI_TARGETS= \
    $(CI_PLATFORM_FULL) \
    ci-argosy \
    ci-async_test \
    ci-atbr \
    ci-autosubst \
    ci-autosubst_ocaml \
    ci-bbv \
    ci-bedrock2 \
    ci-bedrock2_examples \
    ci-category_theory \
    ci-ceres \
    ci-coinduction \
    ci-color \
    ci-compcert \
    ci-coqutil \
    ci-cross_crypto \
    ci-coq_performance_tests \
    ci-coq_tools \
    ci-deriving \
    ci-elpi_test \
    ci-hb_test \
    ci-engine_bench \
    ci-equations_test \
    ci-fcsl_pcm \
    ci-fiat_crypto \
    ci-fiat_crypto_legacy \
    ci-fiat_crypto_ocaml \
    ci-fiat_parsers \
    ci-fourcolor \
    ci-http \
    ci-itree \
    ci-itree_io \
    ci-jasmin \
    ci-json \
    ci-kami \
    ci-mathcomp_test \
    ci-metacoq \
    ci-neural_net_interp \
    ci-oddorder \
    ci-paco \
    ci-parsec \
    ci-perennial \
    ci-quickchick_test \
    ci-rewriter \
    ci-riscv_coq \
    ci-rupicola \
    ci-sf \
    ci-smtcoq \
    ci-smtcoq_trakt \
    ci-stalmarck \
    ci-stdlib_doc \
    ci-stdlib_test \
    ci-tactician \
    ci-tlc \
    ci-trakt \
    ci-verdi_raft \
    ci-vst \
    ci-waterproof

CI_VIRTUAL_TARGETS= \
    ci-elpi_hb \
    ci-platform_full

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

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

ci-all: $(CI_TARGETS)

ci-category_theory: ci-equations

ci-color: ci-bignums

ci-mathcomp: ci-elpi_hb

ci-coqprime: ci-bignums
ci-coquelicot: ci-mathcomp
ci-deriving: ci-mathcomp
ci-math_classes: ci-bignums

ci-corn: ci-math_classes

ci-mtac2: ci-unicoq

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_ocaml: ci-fiat_crypto

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

ci-hb: ci-elpi

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

ci-trakt: ci-elpi

ci-jasmin: ci-mathcomp_word

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-itree: ci-ext_lib ci-paco
ci-itree_io: ci-itree ci-simple_io

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_test: ci-equations

ci-metacoq: ci-equations

ci-vst: ci-compcert

ci-compcert: ci-menhir ci-flocq

ci-relation_algebra: ci-aac_tactics ci-mathcomp

ci-serapi: ci-coq_lsp

ci-smtcoq_trakt: ci-trakt

ci-refman: ci-platform_full

# 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 $*

# 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: