aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.travis.yml1
-rw-r--r--Makefile13
2 files changed, 12 insertions, 2 deletions
diff --git a/.travis.yml b/.travis.yml
index 9c5078643..6cabe6413 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -27,6 +27,7 @@ matrix:
- env: COQ_VERSION="8.7.1" TARGETS="no-curves-proofs-non-specific" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
- env: COQ_VERSION="8.7.1" TARGETS="curves-proofs" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
- env: COQ_VERSION="8.7.1" TARGETS="selected-specific selected-specific-display" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
+ - env: TARGETS="build-selected-test build-selected-bench" COQ_VERSION="8.7.1" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
- env: TARGETS="selected-test selected-bench" COQ_VERSION="8.7.1" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
- env: TARGETS="printlite lite" COQ_VERSION="8.7.1" COQ_PACKAGE="coq-8.7.1" PPA="ppa:jgross-h/many-coq-versions"
allow_failures:
diff --git a/Makefile b/Makefile
index 0042c9cf9..b8f390a26 100644
--- a/Makefile
+++ b/Makefile
@@ -18,8 +18,8 @@ INSTALLDEFAULTROOT := Crypto
specific-c specific-display display \
specific non-specific lite only-heavy printlite \
curves-proofs no-curves-proofs no-curves-proofs-non-specific \
- selected-specific selected-specific-display nonautogenerated-specific nonautogenerated-specific-display nonautogenerated-c selected-test selected-bench selected-c \
- test bench c \
+ selected-specific selected-specific-display nonautogenerated-specific nonautogenerated-specific-display nonautogenerated-c build-selected-test selected-test build-selected-bench selected-bench selected-c \
+ build-test test build-bench bench c \
regenerate-curves
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq
@@ -268,6 +268,7 @@ 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_MEASURE_BINARIES := $(filter $(SELECTED_PATTERN),$(MEASURE_BINARIES))
SELECTED_MEASUREMENTS := $(filter $(SELECTED_PATTERN),$(MEASUREMENTS))
src/Specific/X25519/C64/test src/Specific/X25519/C64/measure: $(filter-out $(UNMADE_C_FILES),$(DISPLAY_X25519_C64_VO:Display.vo=.c) $(DISPLAY_X25519_C64_VO:Display.vo=.h)) src/Specific/X25519/C64/scalarmult.c
@@ -402,8 +403,16 @@ $(RUN_TEST_BINARIES) : %-run : %
test: $(RUN_TEST_BINARIES)
+build-test: $(TEST_BINARIES)
+
selected-test: $(RUN_SELECTED_TEST_BINARIES)
+build-selected-test: $(SELECTED_TEST_BINARIES)
+
+build-bench: $(MEASURE_BINARIES)
+
+build-selected-bench: $(SELECTED_MEASURE_BINARIES)
+
clean::
rm -f Makefile.coq remake_curves.log src/Specific/.autgenerated-deps