diff options
author | Jason Gross <jgross@mit.edu> | 2018-07-11 09:25:46 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-07-21 03:40:18 +0100 |
commit | cb1449271906998bb29c00d68c0bee4b58d2803c (patch) | |
tree | e777fb67aed388e698fbbf3efd6d79cbf724862f /Makefile | |
parent | de6a1248e2cd74f27434bb01867cf9fa073e8c8a (diff) |
Allow building with an external coqprime
Closes #363
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 58 |
1 files changed, 34 insertions, 24 deletions
@@ -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" |