diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-15 16:01:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-15 16:01:11 -0500 |
| commit | efe4ef7c8459fb6ae750cffd5999833dc0ff098f (patch) | |
| tree | 88765ed90b1debde4976f4b2d75e9a5ed1511936 /Makefile | |
| parent | 5bddc2b336b16ec64c0900260889228856407df3 (diff) | |
Add rudimentary Java and C notation files, display
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 13 |
1 files changed, 13 insertions, 0 deletions
@@ -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 |