aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-08-24 09:58:33 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-08-24 09:58:33 -0400
commitf2ee602badfe272fc55f3d35f62a7abdf72a9ee5 (patch)
tree99a7211cf7deb627c953bf21cdb374c2e0ca0330 /Makefile
parent64825ae187b354e4a6647105ce52544abdb6f4ae (diff)
Add util target as a sort of common target
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 7 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 8d1467c64..e2e555a46 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,7 @@ INSTALLDEFAULTROOT := Crypto
old-pipeline-nobigmem print-old-pipeline-nobigmem \
old-pipeline-lite print-old-pipeline-lite \
nobigmem print-nobigmem \
+ util \
specific-c specific-display display \
specific non-specific lite only-heavy printlite lite-display print-lite-display \
new-pipeline pre-standalone \
@@ -54,7 +55,7 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc
-include Makefile.coq
endif
-ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite print-lite-display lite-display nobigmem print-nobigmem new-pipeline pre-standalone old-pipeline-nobigmem print-old-pipeline-nobigmem old-pipeline-lite print-old-pipeline-lite,$(MAKECMDGOALS)),)
+ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite print-lite-display lite-display nobigmem print-nobigmem new-pipeline pre-standalone old-pipeline-nobigmem print-old-pipeline-nobigmem old-pipeline-lite print-old-pipeline-lite util,$(MAKECMDGOALS)),)
-include etc/coq-scripts/Makefile.vo_closure
else
include etc/coq-scripts/Makefile.vo_closure
@@ -113,6 +114,7 @@ NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := $(filter $(NO_CURVES_PROOFS_UNMA
REAL_SPECIFIC_GENERATED_VOFILES := $(filter $(SPECIFIC_GENERATED_VOFILES),$(VOFILES))
NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES))
+UTIL_PRE_VO_FILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
SELECTED_PATTERN := \
src/Specific/X25519/C64/% \
@@ -156,6 +158,9 @@ endif
ifneq ($(filter only-heavy,$(MAKECMDGOALS)),)
HEAVY_VOFILES := $(call vo_closure,$(LITE_UNMADE_VOFILES))
endif
+ifneq ($(filter util,$(MAKECMDGOALS)),)
+UTIL_VOFILES := $(call vo_closure,$(UTIL_PRE_VOFILES))
+endif
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))
@@ -187,6 +192,7 @@ lite-display: $(LITE_DISPLAY_VOFILES:.vo=.log)
nobigmem: $(NOBIGMEM_VOFILES)
old-pipeline-nobigmem: $(OLD_PIPELINE_NOBIGMEM_VOFILES)
only-heavy: $(HEAVY_VOFILES)
+util: $(UTIL_VOFILES)
curves-proofs: $(CURVES_PROOFS_VOFILES)
no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES)
no-curves-proofs-non-specific: $(NO_CURVES_PROOFS_NON_SPECIFIC_VOFILES)