From 037df57566b1108af0d13cfcafe9b0f8fdd5937b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 6 May 2018 22:17:10 -0400
Subject: New pipeline, split among files

---
 Makefile | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 6f1ae4b2e..8981cfe23 100644
--- a/Makefile
+++ b/Makefile
@@ -7,6 +7,9 @@ TIMECMD?=
 STDTIME?=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
+GHC?=ghc
+GHCFLAGS?= # -XStrict
+
 PROFILE?=
 VERBOSE?=
 SHOW := $(if $(VERBOSE),@true "",@echo "")
@@ -21,6 +24,7 @@ INSTALLDEFAULTROOT := Crypto
 	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 \
+	standalone standalone-haskell standalone-ocaml \
 	regenerate-curves
 
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq
@@ -66,7 +70,10 @@ UNMADE_C_FILES := \
 	src/Specific/X25519/C32/fesub.c src/Specific/X25519/C32/feadd.c src/Specific/X25519/C32/fecarry.c \
 	src/Specific/X25519/C32/fesub.h src/Specific/X25519/C32/feadd.h src/Specific/X25519/C32/fecarry.h
 # files that are treated specially
-SPECIAL_VOFILES := src/Specific/%Display.vo
+SPECIAL_VOFILES := \
+	src/Specific/%Display.vo \
+	src/Experiments/NewPipeline/ExtractionOCaml/%.vo \
+	src/Experiments/NewPipeline/ExtractionHaskell/%.vo
 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
@@ -78,6 +85,8 @@ 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/Toplevel2.vo \
+	src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \
 	$(SPECIFIC_GENERATED_VOFILES)
 NOBIGMEM_UNMADE_VOFILES := \
 	src/Curves/Weierstrass/AffineProofs.vo \
@@ -447,6 +456,31 @@ build-bench: $(MEASURE_BINARIES)
 
 build-selected-bench: $(SELECTED_MEASURE_BINARIES)
 
+STANDALONE := \
+	unsaturated_solinas \
+	saturated_solinas
+
+$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%.ml) : %.ml : %.v src/Experiments/NewPipeline/StandaloneOCamlMain.vo
+	$(SHOW)'COQC $< > $@'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
+	$(HIDE)sed s'/\r\n/\n/g' $@.tmp > $@ && rm -f $@.tmp
+
+$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v src/Experiments/NewPipeline/StandaloneHaskellMain.vo src/Experiments/NewPipeline/haskell.sed
+	$(SHOW)'COQC $< > $@'
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp
+	$(HIDE)sed s'/\r\n/\n/g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp
+
+$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml
+	$(TIMER) ocamlopt -o $@ $<
+
+$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs
+	$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $<
+
+standalone: standalone-haskell standalone-ocaml
+
+standalone-haskell: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%)
+standalone-ocaml: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%)
+
 clean::
 	rm -f Makefile.coq remake_curves.log src/Specific/.autgenerated-deps
 
-- 
cgit v1.2.3