From bc0239c0f6f5bafcf264cbabf3d783ca1146360d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 3 Nov 2016 20:25:30 -0400 Subject: separate Ed25519Extraction.v, add extraction to Makefile @JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment --- Makefile | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 6a643fa7b..e1f99befe 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,8 @@ HIDE := $(if $(VERBOSE),,@) .PHONY: coq clean update-_CoqProject cleanall install \ install-coqprime clean-coqprime coqprime \ - specific non-specific + specific non-specific \ + extraction ghc SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' @@ -84,6 +85,21 @@ Makefile.coq: Makefile _CoqProject $(SHOW)'COQ_MAKEFILE -f _CoqProject > $@' $(HIDE)$(COQBIN)coq_makefile -f _CoqProject | sed s'|^\(-include.*\)$$|ifneq ($$(filter-out $(FAST_TARGETS),$$(MAKECMDGOALS)),)~\1~else~ifeq ($$(MAKECMDGOALS),)~\1~endif~endif|g' | tr '~' '\n' | sed s'/^clean:$$/clean::/g' | sed s'/^Makefile: /Makefile-old: /g' | sed s'/^printenv:$$/printenv::/g' > $@ +src/Experiments/Ed25519_noimports.hs: src/Experiments/Ed25519Extraction.vo src/Experiments/Ed25519Extraction.v + +src/Experiments/Ed25519.hs: src/Experiments/Ed25519_noimports.hs src/Experiments/Ed25519_imports.hs + ( cd src/Experiments && \ + < Ed25519_noimports.hs \ + sed "/import qualified Prelude/r Ed25519_imports.hs" | \ + sed 's/ Ed25519_noimports / Ed25519 /g' \ + > Ed25519.hs ) + +src/Experiments/Ed25519.o src/Experiments/Ed25519.core: src/Experiments/Ed25519.hs + ( cd src/Experiments && ghc -O3 Ed25519.hs -ddump-simpl > Ed25519.core ) + +extraction: src/Experiments/Ed25519.hs +ghc: src/Experiments/Ed25519.core + clean:: rm -f Makefile.coq -- cgit v1.2.3