diff options
Diffstat (limited to 'Makefile.ci')
-rw-r--r-- | Makefile.ci | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci new file mode 100644 index 00000000..20712b60 --- /dev/null +++ b/Makefile.ci @@ -0,0 +1,67 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \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_TARGETS=ci-bedrock2 \ + ci-bignums \ + ci-color \ + ci-compcert \ + ci-coq-dpdgraph \ + ci-coquelicot \ + ci-corn \ + ci-cpdt \ + ci-elpi \ + ci-ext-lib \ + ci-equations \ + ci-fcsl-pcm \ + ci-fiat-crypto \ + ci-fiat-crypto-legacy \ + ci-fiat-parsers \ + ci-flocq \ + ci-formal-topology \ + ci-geocoq \ + ci-hott \ + ci-iris-lambda-rust \ + ci-ltac2 \ + ci-math-classes \ + ci-math-comp \ + ci-mtac2 \ + ci-quickchick \ + ci-sf \ + ci-simple-io \ + ci-tlc \ + ci-unimath \ + ci-vst + +.PHONY: ci-all $(CI_TARGETS) + +ci-help: + echo '*** Coq CI system, please specify a target to build.' + false + +ci-all: $(CI_TARGETS) + +ci-color: ci-bignums + +ci-math-classes: ci-bignums + +ci-corn: ci-math-classes + +ci-quickchick: ci-ext-lib ci-simple-io + +ci-formal-topology: ci-corn + +# Generic rule, we use make to ease travis integration with mixed rules +$(CI_TARGETS): ci-%: + +./dev/ci/ci-wrapper.sh $* + +# For emacs: +# Local Variables: +# mode: makefile +# End: |