diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-04-15 14:55:04 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-04-15 14:55:04 -0400 |
| commit | 8b80c0547a1c2d28af8d7b24a4ee03962c45e3ff (patch) | |
| tree | 3d57cfade9644a3aff58e1898dc747241d64d413 /Makefile | |
| parent | 4c437527351f2d3dff1c95e1d4f3261bc6b69b1a (diff) | |
Add a lite-display target
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 16 |
1 files changed, 13 insertions, 3 deletions
@@ -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 |