From a24640e12177576b4c7fcc299f19df09e6b36d81 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Aug 2018 20:48:03 -0400 Subject: Add some makefile targets for Coq's CI This should allow faster, more parallel runs of Coq's CI --- Makefile | 35 +++++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index c9a94ce59..8db58748c 100644 --- a/Makefile +++ b/Makefile @@ -21,6 +21,8 @@ INSTALLDEFAULTROOT := Crypto .PHONY: coq clean update-_CoqProject cleanall install \ install-coqprime clean-coqprime coqprime coqprime-all \ + old-pipeline-nobigmem print-old-pipeline-nobigmem \ + old-pipeline-lite print-old-pipeline-lite \ nobigmem print-nobigmem \ specific-c specific-display display \ specific non-specific lite only-heavy printlite lite-display print-lite-display \ @@ -52,7 +54,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,$(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,$(MAKECMDGOALS)),) -include etc/coq-scripts/Makefile.vo_closure else include etc/coq-scripts/Makefile.vo_closure @@ -79,6 +81,7 @@ SPECIAL_VOFILES := \ SPECIFIC_GENERATED_VOFILES := src/Specific/solinas%.vo src/Specific/montgomery%.vo # add files to this list to prevent them from being built as final # targets by the "lite" target +NEW_PIPELINE_FILTER := src/Experiments/NewPipeline/% LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo \ src/Curves/Weierstrass/Projective.vo \ @@ -100,13 +103,15 @@ NOBIGMEM_UNMADE_VOFILES := \ src/Curves/Weierstrass/Jacobian.vo \ src/Curves/Weierstrass/Projective.vo \ $(SPECIFIC_GENERATED_VOFILES) +OLD_PIPELINE_LITE_UNMADE_VOFILES := $(LITE_UNMADE_VOFILES) $(NEW_PIPELINE_FILTER) +OLD_PIPELINE_NOBIGMEM_UNMADE_VOFILES := $(NOBIGMEM_UNMADE_VOFILES) $(NEW_PIPELINE_FILTER) REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES) $(UNMADE_VOFILES),$(VOFILES)) CURVES_PROOFS_PRE_VOFILES := $(filter src/Curves/Weierstrass/Jacobian.vo src/Curves/%Proofs.vo,$(REGULAR_VOFILES)) NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo NO_CURVES_PROOFS_NON_SPECIFIC_UNMADE_VOFILES := $(filter $(NO_CURVES_PROOFS_UNMADE_VOFILES) src/Specific/%.vo,$(VOFILES)) REAL_SPECIFIC_GENERATED_VOFILES := $(filter $(SPECIFIC_GENERATED_VOFILES),$(VOFILES)) -NEW_PIPELINE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/%,$(REGULAR_VOFILES)) +NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES)) PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES)) SELECTED_PATTERN := \ @@ -136,10 +141,18 @@ LITE_ALL_UNMADE_VOFILES := $(foreach vo,$(LITE_UNMADE_VOFILES),$(call vo_reverse LITE_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) LITE_DISPLAY_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(DISPLAY_VO)) endif +ifneq ($(filter print-old-pipeline-lite old-pipeline-lite,$(MAKECMDGOALS)),) +OLD_PIPELINE_LITE_ALL_UNMADE_VOFILES := $(foreach vo,$(OLD_PIPELINE_LITE_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) +OLD_PIPELINE_LITE_VOFILES := $(filter-out $(OLD_PIPELINE_LITE_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) +endif ifneq ($(filter nobigmem print-nobigmem,$(MAKECMDGOALS)),) NOBIGMEM_ALL_UNMADE_VOFILES := $(foreach vo,$(NOBIGMEM_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) NOBIGMEM_VOFILES := $(filter-out $(NOBIGMEM_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) endif +ifneq ($(filter old-pipeline-nobigmem print-old-pipeline-nobigmem,$(MAKECMDGOALS)),) +OLD_PIPELINE_NOBIGMEM_ALL_UNMADE_VOFILES := $(foreach vo,$(OLD_PIPELINE_NOBIGMEM_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) +OLD_PIPELINE_NOBIGMEM_VOFILES := $(filter-out $(OLD_PIPELINE_NOBIGMEM_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) +endif ifneq ($(filter only-heavy,$(MAKECMDGOALS)),) HEAVY_VOFILES := $(call vo_closure,$(LITE_UNMADE_VOFILES)) endif @@ -169,8 +182,10 @@ specific: $(SPECIFIC_VO) non-specific: $(NON_SPECIFIC_VO) coq: $(COQ_VOFILES) lite: $(LITE_VOFILES) +old-pipeline-lite: $(OLD_PIPELINE_LITE_VOFILES) lite-display: $(LITE_DISPLAY_VOFILES:.vo=.log) nobigmem: $(NOBIGMEM_VOFILES) +old-pipeline-nobigmem: $(OLD_PIPELINE_NOBIGMEM_VOFILES) only-heavy: $(HEAVY_VOFILES) curves-proofs: $(CURVES_PROOFS_VOFILES) no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES) @@ -225,6 +240,14 @@ printlite:: @echo 'Files Not Made:' @for i in $(sort $(LITE_ALL_UNMADE_VOFILES)); do echo $$i; done +print-old-pipeline-lite:: + @echo 'Files Made:' + @for i in $(sort $(OLD_PIPELINE_LITE_VOFILES)); do echo $$i; done + @echo + @echo + @echo 'Files Not Made:' + @for i in $(sort $(OLD_PIPELINE_LITE_ALL_UNMADE_VOFILES)); do echo $$i; done + print-lite-display:: @echo 'Files Made:' @for i in $(sort $(LITE_DISPLAY_VOFILES)); do echo $$i; done @@ -241,6 +264,14 @@ print-nobigmem:: @echo 'Files Not Made:' @for i in $(sort $(NOBIGMEM_ALL_UNMADE_VOFILES)); do echo $$i; done +print-old-pipeline-nobigmem:: + @echo 'Files Made:' + @for i in $(sort $(OLD_PIPELINE_NOBIGMEM_VOFILES)); do echo $$i; done + @echo + @echo + @echo 'Files Not Made:' + @for i in $(sort $(OLD_PIPELINE_NOBIGMEM_ALL_UNMADE_VOFILES)); do echo $$i; done + ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else ifneq ($(PROFILE),) -- cgit v1.2.3