From 3ec21c64b3682465ca8e159a187689b207c71de4 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 8 Jan 2019 01:59:52 -0500 Subject: move src/Experiments/NewPipeline/ to src/ --- Makefile | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 6e9ccbb4d..56cbed38a 100644 --- a/Makefile +++ b/Makefile @@ -78,12 +78,12 @@ UNMADE_C_FILES := \ # files that are treated specially SPECIAL_VOFILES := \ src/Specific/%Display.vo \ - src/Experiments/NewPipeline/ExtractionOCaml/%.vo \ - src/Experiments/NewPipeline/ExtractionHaskell/%.vo + src/ExtractionOCaml/%.vo \ + src/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 -NEW_PIPELINE_FILTER := src/Experiments/NewPipeline/% +NEW_PIPELINE_FILTER := src/% LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo \ src/Curves/Weierstrass/Projective.vo \ @@ -92,12 +92,12 @@ 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/RewriterWf1.vo \ - src/Experiments/NewPipeline/RewriterWf2.vo \ - src/Experiments/NewPipeline/RewriterRulesGood.vo \ - src/Experiments/NewPipeline/RewriterProofs.vo \ - src/Experiments/NewPipeline/Toplevel2.vo \ - src/Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo \ + src/RewriterWf1.vo \ + src/RewriterWf2.vo \ + src/RewriterRulesGood.vo \ + src/RewriterProofs.vo \ + src/Toplevel2.vo \ + src/SlowPrimeSynthesisExamples.vo \ src/Experiments/SimplyTypedArithmetic.vo \ $(SPECIFIC_GENERATED_VOFILES) NOBIGMEM_UNMADE_VOFILES := \ @@ -114,12 +114,12 @@ NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.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 $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES)) -PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES)) +PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES)) UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES)) COQ_WITHOUT_NEW_PIPELINE_VOFILES := $(filter-out $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES)) SOME_EARLY_VOFILES := \ - src/Experiments/NewPipeline/Arithmetic.vo \ - src/Experiments/NewPipeline/Rewriter.vo \ + src/Arithmetic.vo \ + src/Rewriter.vo \ src/Experiments/SimplyTypedArithmetic.vo SELECTED_PATTERN := \ @@ -543,33 +543,33 @@ STANDALONE := \ saturated_solinas \ word_by_word_montgomery -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%.ml) : %.ml : %.v src/Experiments/NewPipeline/StandaloneOCamlMain.vo +$(STANDALONE:%=src/ExtractionOCaml/%.ml) : %.ml : %.v src/StandaloneOCamlMain.vo $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp > $@ && rm -f $@.tmp -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%.hs) : %.hs : %.v src/Experiments/NewPipeline/StandaloneHaskellMain.vo src/Experiments/NewPipeline/haskell.sed +$(STANDALONE:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/StandaloneHaskellMain.vo src/haskell.sed $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER_FULL) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp - $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/Experiments/NewPipeline/haskell.sed > $@ && rm -f $@.tmp + $(HIDE)sed 's/\r\n/\n/g; s/\r//g' $@.tmp | sed -f src/haskell.sed > $@ && rm -f $@.tmp # pass -w -20 to disable the unused argument warning -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) : % : %.ml +$(STANDALONE:%=src/ExtractionOCaml/%) : % : %.ml $(TIMER_FULL) ocamlopt -w -20 -o $@ $< -$(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) : % : %.hs +$(STANDALONE:%=src/ExtractionHaskell/%) : % : %.hs $(TIMER_FULL) $(GHC) $(GHCFLAGS) -o $@ $< standalone: standalone-haskell standalone-ocaml -standalone-haskell: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell/%) -standalone-ocaml: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) +standalone-haskell: $(STANDALONE:%=src/ExtractionHaskell/%) +standalone-ocaml: $(STANDALONE:%=src/ExtractionOCaml/%) UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c p521_64.c p521_32.c # p224_solinas_64.c WORD_BY_WORD_MONTGOMERY_C_FILES := p256_64.c p256_32.c p384_64.c p384_32.c secp256k1_64.c secp256k1_32.c p224_64.c p224_32.c FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes -UNSATURATED_SOLINAS := src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas -WORD_BY_WORD_MONTGOMERY := src/Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery +UNSATURATED_SOLINAS := src/ExtractionOCaml/unsaturated_solinas +WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/word_by_word_montgomery ALL_C_FILES := $(UNSATURATED_SOLINAS_C_FILES) $(WORD_BY_WORD_MONTGOMERY_C_FILES) .PHONY: c-files c-files: $(ALL_C_FILES) -- cgit v1.2.3