diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-03 14:56:36 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-08-04 20:00:53 -0400 |
| commit | 4871dfda627597bcee92fc94edf2e37cdfd0ef49 (patch) | |
| tree | 3172f6d257dfaea45d34fc5217ac25e3591ebe87 /Makefile | |
| parent | ba456dc393f88b281407685896b62f83fd914b7f (diff) | |
Move new-pipeline to its own stage
It's starting to get pretty slow.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 10 |
1 files changed, 9 insertions, 1 deletions
@@ -24,6 +24,7 @@ INSTALLDEFAULTROOT := Crypto nobigmem print-nobigmem \ specific-c specific-display display \ specific non-specific lite only-heavy printlite lite-display print-lite-display \ + new-pipeline \ curves-proofs no-curves-proofs no-curves-proofs-non-specific \ 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 \ @@ -51,7 +52,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,$(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,$(MAKECMDGOALS)),) -include etc/coq-scripts/Makefile.vo_closure else include etc/coq-scripts/Makefile.vo_closure @@ -86,6 +87,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Specific/NISTP256/AMD128/fe%.vo \ src/Specific/X25519/C64/ladderstep.vo \ src/Specific/X25519/C32/fe%.vo \ + src/Experiments/NewPipeline/RewriterProofs.vo \ src/Experiments/NewPipeline/Toplevel2.vo \ src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \ src/Experiments/SimplyTypedArithmetic.vo \ @@ -101,6 +103,7 @@ 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)) SELECTED_PATTERN := \ src/Specific/X25519/C64/% \ @@ -150,6 +153,10 @@ endif ifneq ($(filter selected-specific,$(MAKECMDGOALS)),) SELECTED_SPECIFIC_VOFILES := $(call vo_closure,$(SELECTED_SPECIFIC_PRE_VOFILES)) endif +ifneq ($(filter new-pipeline,$(MAKECMDGOALS)),) +NEW_PIPELINE_VOFILES := $(call vo_closure,$(NEW_PIPELINE_PRE_VOFILES)) +endif + specific: $(SPECIFIC_VO) non-specific: $(NON_SPECIFIC_VO) @@ -161,6 +168,7 @@ 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) +new-pipeline: $(NEW_PIPELINE_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) |