diff options
| -rw-r--r-- | .travis.yml | 42 | ||||
| -rw-r--r-- | Makefile | 38 |
2 files changed, 57 insertions, 23 deletions
diff --git a/.travis.yml b/.travis.yml index 50ec6218b..d4fe9dc4d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -18,24 +18,32 @@ addons: matrix: fast_finish: true include: - - env: COQ_VERSION="master" TARGETS="no-curves-proofs display test bench" 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="v8.7" TARGETS="no-curves-proofs display test bench" 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.6" TARGETS="no-curves-proofs display bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" - - env: COQ_VERSION="v8.6" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" - - env: COQ_VERSION="8.7+beta1" TARGETS="no-curves-proofs display test bench" COQ_PACKAGE="coq-8.7+beta1" PPA="ppa:jgross-h/many-coq-versions" - - env: COQ_VERSION="8.7+beta1" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.7+beta1" PPA="ppa:jgross-h/many-coq-versions" - - env: COQ_VERSION="8.6.1" TARGETS="no-curves-proofs display bench" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" - - env: COQ_VERSION="8.6.1" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" - - env: TARGETS="printlite lite" COQ_VERSION="8.6.1" COQ_PACKAGE="coq-8.6.1" 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 selected-test selected-bench" 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 selected-test selected-bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily" + - env: COQ_VERSION="v8.6" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - env: COQ_VERSION="v8.6" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - env: COQ_VERSION="v8.6" TARGETS="selected-specific selected-specific-display selected-test selected-bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - env: COQ_VERSION="8.7+beta2" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq-8.7+beta2" PPA="ppa:jgross-h/many-coq-versions" + - env: COQ_VERSION="8.7+beta2" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.7+beta2" PPA="ppa:jgross-h/many-coq-versions" + - env: COQ_VERSION="8.7+beta2" TARGETS="selected-specific selected-specific-display selected-test selected-bench" COQ_PACKAGE="coq-8.7+beta2" PPA="ppa:jgross-h/many-coq-versions" + - env: COQ_VERSION="8.6.1" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" + - env: COQ_VERSION="8.6.1" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" + - env: COQ_VERSION="8.6.1" TARGETS="selected-specific selected-specific-display selected-test selected-bench" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" + - env: TARGETS="printlite lite" COQ_VERSION="8.6.1" COQ_PACKAGE="coq-8.6.1" PPA="ppa:jgross-h/many-coq-versions" allow_failures: - - env: COQ_VERSION="master" TARGETS="no-curves-proofs display test bench" 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="v8.7" TARGETS="no-curves-proofs display test bench" 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.6" TARGETS="no-curves-proofs display bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" - - env: COQ_VERSION="v8.6" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - 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 selected-test selected-bench" 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 selected-test selected-bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.7-daily" + - env: COQ_VERSION="v8.6" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - env: COQ_VERSION="v8.6" TARGETS="curves-proofs" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" + - env: COQ_VERSION="v8.6" TARGETS="selected-specific selected-specific-display selected-test selected-bench" COQ_PACKAGE="coq" PPA="ppa:jgross-h/coq-8.6-daily" before_install: - if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi @@ -17,7 +17,8 @@ INSTALLDEFAULTROOT := Crypto install-coqprime clean-coqprime coqprime \ specific-c specific-display display \ specific non-specific lite only-heavy printlite \ - curves-proofs no-curves-proofs \ + curves-proofs no-curves-proofs no-curves-proofs-non-specific \ + selected-specific selected-speicifc-display selected-test selected-bench selected-c \ test bench c SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq @@ -41,7 +42,7 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc -include Makefile.coq endif -ifeq ($(filter curves-proofs no-curves-proofs lite only-heavy printdeps printreversedeps printlite,$(MAKECMDGOALS)),) +ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite,$(MAKECMDGOALS)),) -include etc/coq-scripts/Makefile.vo_closure else include etc/coq-scripts/Makefile.vo_closure @@ -56,20 +57,25 @@ update-_CoqProject:: $(VOFILES): | coqprime # add files to this list to prevent them from being built by default -UNMADE_VOFILES := src/SpecificGen/% src/Specific/%Display.vo +UNMADE_VOFILES := src/Specific/%Display.vo # add files to this list to prevent them from being built as final # targets by the "lite" target -LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/Karatsuba.vo src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.vo src/Specific/X25519/C64/ladderstep.vo +LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/Karatsuba.vo src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.vo src/Specific/X25519/C64/ladderstep.vo src/Specific/X25519/C32/%.vo CURVES_PROOFS_PRE_VOFILES := $(filter src/Curves/%Proofs.vo,$(VOFILES)) NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo +NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/%.vo + +SELECTED_PATTERN := src/Specific/X25519/C64/% src/Specific/NISTP256/AMD64/% third_party/% +SELECTED_SPECIFIC_PRE_VOFILES := $(filter $(SELECTED_PATTERN),$(VOFILES)) COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES)) SPECIFIC_VO := $(filter src/Specific/%,$(VOFILES)) -NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES)) +NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VOFILES)) SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(VOFILES)) DISPLAY_VO := $(SPECIFIC_DISPLAY_VO) DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO)) DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO)) +SELECTED_SPECIFIC_DISPLAY_VO := $(filter $(SELECTED_PATTERN),$(DISPLAY_VO)) # computing the vo_reverse_closure is slow, so we only do it if we're # asked to make the lite target ifneq ($(filter printlite lite,$(MAKECMDGOALS)),) @@ -83,9 +89,16 @@ ifneq ($(filter no-curves-proofs,$(MAKECMDGOALS)),) NO_CURVES_PROOFS_ALL_UNMADE_VOFILES := $(foreach vo,$(NO_CURVES_PROOFS_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) NO_CURVES_PROOFS_VOFILES := $(filter-out $(NO_CURVES_PROOFS_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) endif +ifneq ($(filter no-curves-proofs-non-specific,$(MAKECMDGOALS)),) +NO_CURVES_PROOFS_NON_SPECIFIC_ALL_UNMADE_VOFILES := $(foreach vo,$(NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) +NO_CURVES_PROOFS_NON_SPECIFIC_VOFILES := $(filter-out $(NO_CURVES_PROOFS_NON_SPECIFIC_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) +endif ifneq ($(filter curves-proofs,$(MAKECMDGOALS)),) CURVES_PROOFS_VOFILES := $(call vo_closure,$(CURVES_PROOFS_PRE_VOFILES)) endif +ifneq ($(filter selected-specific,$(MAKECMDGOALS)),) +SELECTED_SPECIFIC_VOFILES := $(call vo_closure,$(SELECTED_SPECIFIC_PRE_VOFILES)) +endif specific: $(SPECIFIC_VO) coqprime non-specific: $(NON_SPECIFIC_VO) coqprime @@ -94,8 +107,12 @@ lite: $(LITE_VOFILES) coqprime only-heavy: $(HEAVY_VOFILES) coqprime curves-proofs: $(CURVES_PROOFS_VOFILES) coqprime no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES) coqprime +no-curves-proofs-non-specific: $(NO_CURVES_PROOFS_NON_SPECIFIC_VOFILES) coqprime specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log) coqprime -specific-c: $(SPECIFIC_DISPLAY_VO:Display.vo=.c) coqprime +specific-c: $(SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SPECIFIC_DISPLAY_VO:Display.vo=.h) coqprime +selected-specific: $(SELECTED_SPECIFIC_VOFILES) coqprime +selected-specific-display: $(SELECTED_SPECIFIC_DISPLAY_VO:.vo=.log) coqprime +selected-c: $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h) coqprime display: $(DISPLAY_VO:.vo=.log) coqprime printlite:: @@ -179,6 +196,10 @@ MEASUREMENTS := \ src/Specific/NISTP256/AMD64/icc/measurements.txt MEASURE_BINARIES := $(addsuffix measure,$(dir $(MEASUREMENTS))) +SELECTED_TEST_BINARIES := $(filter $(SELECTED_PATTERN),$(TEST_BINARIES)) +RUN_SELECTED_TEST_BINARIES := $(filter $(SELECTED_PATTERN),$(RUN_TEST_BINARIES)) +SELECTED_MEASUREMENTS := $(filter $(SELECTED_PATTERN),$(MEASUREMENTS)) + src/Specific/X25519/C64/test src/Specific/X25519/C64/measure: $(DISPLAY_X25519_C64_VO:Display.vo=.c) $(DISPLAY_X25519_C64_VO:Display.vo=.h) src/Specific/X25519/C64/scalarmult.c src/Specific/X25519/C64/test: src/Specific/X25519/C64/compiler.sh src/Specific/X25519/x25519_test.c src/Specific/X25519/C64/test: INCLUDE_FOLDER=src/Specific/X25519/C64 @@ -241,6 +262,9 @@ src/Specific/NISTP256/AMD64/icc/combined.c: liblow/cmovznz.c src/Specific/NISTP2 bench: $(MEASUREMENTS) head -999999 $? +selected-bench: $(SELECTED_MEASUREMENTS) + head -999999 $? + .PHONY: $(RUN_TEST_BINARIES) $(RUN_TEST_BINARIES) : %-run : % @@ -248,6 +272,8 @@ $(RUN_TEST_BINARIES) : %-run : % test: $(RUN_TEST_BINARIES) +selected-test: $(RUN_SELECTED_TEST_BINARIES) + clean:: rm -f Makefile.coq |