aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.travis.yml36
-rw-r--r--Makefile11
2 files changed, 29 insertions, 18 deletions
diff --git a/.travis.yml b/.travis.yml
index b4235e2bf..2787410fe 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -18,25 +18,25 @@ addons:
matrix:
fast_finish: true
include:
- - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="master" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="v8.7" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: COQ_VERSION="v8.7" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: COQ_VERSION="v8.7" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: COQ_VERSION="8.7.0" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
- - env: COQ_VERSION="8.7.0" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
- - env: COQ_VERSION="8.7.0" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
- - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
- - env: TARGETS="printlite lite" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="master" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: COQ_VERSION="8.7.0" TARGETS="no-curves-proofs-non-specific fast-autogenerated-deps" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: COQ_VERSION="8.7.0" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: COQ_VERSION="8.7.0" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: TARGETS="printlite lite" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
allow_failures:
- - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="master" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
- - env: COQ_VERSION="v8.7" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: COQ_VERSION="v8.7" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: COQ_VERSION="v8.7" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
- - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
+ - env: COQ_VERSION="master" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="master" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="master" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-master-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: COQ_VERSION="v8.7" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily"
+ - env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.0" COQ_PACKAGE="coq-8.7.0" PPA="ppa:jgross-h/many-coq-versions"
before_install:
- if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
diff --git a/Makefile b/Makefile
index ee92d04ac..a653be996 100644
--- a/Makefile
+++ b/Makefile
@@ -140,6 +140,17 @@ display: $(DISPLAY_VO:.vo=.log) coqprime
regenerate-curves::
./regenerate-curves.sh
+# extra target for faster coqdep
+.PHONY: src/Specific/.autgenerated-deps
+src/Specific/.autgenerated-deps:
+ $(SHOW)'COQDEP $@'
+ $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(SPECIFIC_GENERATED_VOFILES:.vo=.v) $(redir_if_ok)
+
+.PHONY: fast-autogenerated-deps
+fast-autogenerated-deps: src/Specific/.autgenerated-deps
+ $(SHOW)'CP .v.d'
+ $(HIDE)for i in $(SPECIFIC_GENERATED_VOFILES:.vo=.v.d); do cp -f src/Specific/.autgenerated-deps $$i; done
+
printlite::
@echo 'Files Made:'
@for i in $(sort $(LITE_VOFILES)); do echo $$i; done