|
##########################################################################
## # 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-algebra_tactics \
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= \
$(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-coqtail \
ci-coqutil \
ci-cross_crypto \
ci-coq_lsp \
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-lean_importer \
ci-ltac2_compiler \
ci-mathcomp_test \
ci-metarocq \
ci-neural_net_interp \
ci-oddorder \
ci-paco \
ci-parsec \
ci-perennial \
ci-quickchick_test \
ci-refman \
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-unimath \
ci-verdi_raft \
ci-vsrocq \
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-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-lean_importer: ci-stdlib
ci-mathcomp: ci-elpi_hb
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-cross_crypto: ci-stdlib
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
ci-fcsl_pcm: ci-mathcomp ci-stdlib
ci-mczify: ci-mathcomp ci-stdlib
ci-algebra_tactics: ci-mczify
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-algebra_tactics 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-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-metarocq: 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-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-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 $*
# 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:
[ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
]
|
