From 8b80c0547a1c2d28af8d7b24a4ee03962c45e3ff Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 15 Apr 2018 14:55:04 -0400
Subject: Add a lite-display target

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 5769450fa..13e943d61 100644
--- a/Makefile
+++ b/Makefile
@@ -16,7 +16,7 @@ INSTALLDEFAULTROOT := Crypto
 .PHONY: coq clean update-_CoqProject cleanall install \
 	install-coqprime clean-coqprime coqprime \
 	specific-c specific-display display \
-	specific non-specific lite only-heavy printlite \
+	specific non-specific lite only-heavy printlite lite-display print-lite-display \
 	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 \
@@ -43,7 +43,7 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc
 -include Makefile.coq
 endif
 
-ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite,$(MAKECMDGOALS)),)
+ifeq ($(filter curves-proofs no-curves-proofs no-curves-proofs-non-specific selected-specific selected-specific-display lite only-heavy printdeps printreversedeps printlite print-lite-display lite-display,$(MAKECMDGOALS)),)
 -include etc/coq-scripts/Makefile.vo_closure
 else
 include etc/coq-scripts/Makefile.vo_closure
@@ -106,9 +106,10 @@ DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
 SELECTED_SPECIFIC_DISPLAY_VO := $(filter $(SELECTED_PATTERN),$(DISPLAY_VO))
 # computing the vo_reverse_closure is slow, so we only do it if we're
 # asked to make the lite target
-ifneq ($(filter printlite lite,$(MAKECMDGOALS)),)
+ifneq ($(filter printlite lite lite-display print-lite-display,$(MAKECMDGOALS)),)
 LITE_ALL_UNMADE_VOFILES := $(foreach vo,$(LITE_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo)))
 LITE_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(COQ_VOFILES))
+LITE_DISPLAY_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(DISPLAY_VO))
 endif
 ifneq ($(filter only-heavy,$(MAKECMDGOALS)),)
 HEAVY_VOFILES := $(call vo_closure,$(LITE_UNMADE_VOFILES))
@@ -132,6 +133,7 @@ specific: $(SPECIFIC_VO) coqprime
 non-specific: $(NON_SPECIFIC_VO) coqprime
 coq: $(COQ_VOFILES) coqprime
 lite: $(LITE_VOFILES) coqprime
+lite-display: $(LITE_DISPLAY_VOFILES:Display.vo=.log) coqprime
 only-heavy: $(HEAVY_VOFILES) coqprime
 curves-proofs: $(CURVES_PROOFS_VOFILES) coqprime
 no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES) coqprime
@@ -184,6 +186,14 @@ printlite::
 	@echo 'Files Not Made:'
 	@for i in $(sort $(LITE_ALL_UNMADE_VOFILES)); do echo $$i; done
 
+print-lite-display::
+	@echo 'Files Made:'
+	@for i in $(sort $(LITE_DISPLAY_VOFILES)); do echo $$i; done
+	@echo
+	@echo
+	@echo 'Files Not Made:'
+	@for i in $(sort $(LITE_ALL_UNMADE_VOFILES)); do echo $$i; done
+
 COQPRIME_FOLDER := coqprime
 ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5
 else
-- 
cgit v1.2.3