diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-05-06 22:17:10 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-06-17 13:00:26 -0400 |
| commit | 037df57566b1108af0d13cfcafe9b0f8fdd5937b (patch) | |
| tree | 9310260156d8d1e19215fb4765b5a4e64dc9a9d2 /Makefile | |
| parent | a073821cf7ba0714a30e892af40bd309cd5f2f03 (diff) | |
New pipeline, split among files
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 36 |
1 files changed, 35 insertions, 1 deletions
@@ -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 |