From efe4ef7c8459fb6ae750cffd5999833dc0ff098f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 15 Feb 2017 16:01:11 -0500
Subject: Add rudimentary Java and C notation files, display

---
 Makefile | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 69fea5af6..a43027027 100644
--- a/Makefile
+++ b/Makefile
@@ -12,6 +12,7 @@ HIDE := $(if $(VERBOSE),,@)
 
 .PHONY: coq clean update-_CoqProject cleanall install \
 	install-coqprime clean-coqprime coqprime \
+	display \
 	specific non-specific \
 	small-specific-gen medium-specific-gen specific-gen \
 	extraction ghc
@@ -54,12 +55,16 @@ SPECIFIC_GEN_VO := $(filter src/SpecificGen/%,$(VOFILES))
 MEDIUM_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF5211_32%,$(SPECIFIC_GEN_VO))
 SMALL_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF41417_32%,$(MEDIUM_SPECIFIC_GEN_VO))
 NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES))
+DISPLAY_VO := $(filter src/Specific/%Display.vo src/SpecificGen/%Display.vo,$(VOFILES))
+DISPLAY_JAVA_VO := $(filter src/Specific/%JavaDisplay.vo src/SpecificGen/%JavaDisplay.vo,$(DISPLAY_VO))
+DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
 
 specific: $(SPECIFIC_VO) coqprime
 specific-gen: $(SPECIFIC_GEN_VO) coqprime
 medium-specific-gen: $(MEDIUM_SPECIFIC_GEN_VO) coqprime
 small-specific-gen: $(SMALL_SPECIFIC_GEN_VO) coqprime
 non-specific: $(NON_SPECIFIC_VO) coqprime
+display: $(DISPLAY_VO:.vo=.log) coqprime
 coq: $(COQ_VOFILES) coqprime
 
 ifneq ($(filter 8.4%,$(COQ_VERSION)),) # 8.4
@@ -92,6 +97,14 @@ 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' > $@
 
+$(DISPLAY_NON_JAVA_VO:.vo=.log) : %Display.log : %.vo %Display.v src/Reflection/Z/CNotations.vo
+	$(SHOW)"COQC $*Display > $@"
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*Display.v > $@.tmp && mv -f $@.tmp $@
+
+$(DISPLAY_JAVA_VO:.vo=.log) : %JavaDisplay.log : %.vo %JavaDisplay.v src/Reflection/Z/CNotations.vo
+	$(SHOW)"COQC $*JavaDisplay > $@"
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $*JavaDisplay.v > $@.tmp && mv -f $@.tmp $@
+
 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
-- 
cgit v1.2.3