From cb1449271906998bb29c00d68c0bee4b58d2803c Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 11 Jul 2018 09:25:46 -0400
Subject: Allow building with an external coqprime

Closes #363
---
 Makefile | 58 ++++++++++++++++++++++++++++++++++------------------------
 1 file changed, 34 insertions(+), 24 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 978b170d8..06efe2ffd 100644
--- a/Makefile
+++ b/Makefile
@@ -60,8 +60,6 @@ update-_CoqProject::
 	$(SHOW)'ECHO > _CoqProject'
 	$(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv bbv'; ((git ls-files 'src/*.v'; (git submodule foreach 'git ls-files "*.v" 2>/dev/null | sed "s|^|$$path/|"' | grep 'bbv/')) | $(SORT_COQPROJECT))) > _CoqProject
 
-$(VOFILES): | coqprime
-
 # add files to this list to prevent them from being built by default
 UNMADE_VOFILES :=
 UNMADE_C_FILES := \
@@ -150,25 +148,25 @@ 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
-coq: $(COQ_VOFILES) coqprime
-lite: $(LITE_VOFILES) coqprime
-lite-display: $(LITE_DISPLAY_VOFILES:.vo=.log) coqprime
-nobigmem: $(NOBIGMEM_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: $(filter-out $(UNMADE_C_FILES),$(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: $(filter-out $(UNMADE_C_FILES),$(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h)) coqprime
-nonautogenerated-specific: $(NONAUTOGENERATED_SPECIFIC_VOFILES) coqprime
-nonautogenerated-specific-display: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:.vo=.log) coqprime
-nonautogenerated-c: $(filter-out $(UNMADE_C_FILES),$(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.h)) coqprime
-display: $(DISPLAY_VO:.vo=.log) coqprime
+specific: $(SPECIFIC_VO)
+non-specific: $(NON_SPECIFIC_VO)
+coq: $(COQ_VOFILES)
+lite: $(LITE_VOFILES)
+lite-display: $(LITE_DISPLAY_VOFILES:.vo=.log)
+nobigmem: $(NOBIGMEM_VOFILES)
+only-heavy: $(HEAVY_VOFILES)
+curves-proofs: $(CURVES_PROOFS_VOFILES)
+no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES)
+no-curves-proofs-non-specific: $(NO_CURVES_PROOFS_NON_SPECIFIC_VOFILES)
+specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log)
+specific-c: $(filter-out $(UNMADE_C_FILES),$(SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SPECIFIC_DISPLAY_VO:Display.vo=.h))
+selected-specific: $(SELECTED_SPECIFIC_VOFILES)
+selected-specific-display: $(SELECTED_SPECIFIC_DISPLAY_VO:.vo=.log)
+selected-c: $(filter-out $(UNMADE_C_FILES),$(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h))
+nonautogenerated-specific: $(NONAUTOGENERATED_SPECIFIC_VOFILES)
+nonautogenerated-specific-display: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:.vo=.log)
+nonautogenerated-c: $(filter-out $(UNMADE_C_FILES),$(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.h))
+display: $(DISPLAY_VO:.vo=.log)
 
 regenerate-curves::
 	./regenerate-curves.sh
@@ -224,7 +222,6 @@ print-nobigmem::
 	@echo 'Files Not Made:'
 	@for i in $(sort $(NOBIGMEM_ALL_UNMADE_VOFILES)); do echo $$i; done
 
-COQPRIME_FOLDER := coqprime
 ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5
 else
 ifneq ($(PROFILE),)
@@ -239,9 +236,16 @@ else
 CURDIR_SAFE := $(CURDIR)
 endif
 
+EXTERNAL_DEPENDENCIES?=
+
+ifneq ($(EXTERNAL_DEPENDENCIES),1)
+
+COQPRIME_FOLDER := coqprime
 COQPATH?=${CURDIR_SAFE}/$(COQPRIME_FOLDER)/src
 export COQPATH
 
+$(VOFILES): | coqprime
+
 coqprime:
 	(cd $(COQPRIME_FOLDER) && $(COQBIN)coq_makefile -f _CoqProject -o Makefile)
 	$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) src/Coqprime/PrimalityTest/Zp.vo
@@ -255,6 +259,12 @@ clean-coqprime:
 install-coqprime:
 	$(MAKE) --no-print-directory -C $(COQPRIME_FOLDER) install
 
+cleanall:: clean-coqprime
+
+install: install-coqprime
+
+endif
+
 etc/tscfreq: etc/tscfreq.c
 	gcc etc/tscfreq.c -s -Os -o etc/tscfreq
 
@@ -506,9 +516,9 @@ curve25519_32.c:
 clean::
 	rm -f Makefile.coq remake_curves.log src/Specific/.autgenerated-deps
 
-cleanall:: clean clean-coqprime
+cleanall:: clean
 
-install: coq install-coqprime
+install: coq
 
 printenv::
 	@echo "COQPATH =        $$COQPATH"
-- 
cgit v1.2.3