From ac72003e5f068b9cc7f521c45e497736ef4f0560 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jan 2019 10:45:20 +0100
Subject: [make] support for QUICK

The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
  -native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time

All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
---
 Makefile.vofiles | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

(limited to 'Makefile.vofiles')

diff --git a/Makefile.vofiles b/Makefile.vofiles
index d0ae317335..d5217ef4b7 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -2,14 +2,20 @@
 # This file calls [find] and as such is not suitable for inclusion in
 # the test suite Makefile, unlike Makefile.common.
 
+ifdef QUICK
+VO=vio
+else
+VO=vo
+endif
+
 ###########################################################################
 # vo files
 ###########################################################################
 
-THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
+THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v"))
 ALLVO := $(THEORIESVO) $(PLUGINSVO)
-VFILES := $(ALLVO:.vo=.v)
+VFILES := $(ALLVO:.$(VO)=.v)
 
 ## More specific targets
 
@@ -20,22 +26,27 @@ THEORIESLIGHTVO:= \
 # remove .vo, replace theories and plugins by Coq, and replace slashes by dots
 vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
 
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
+ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
 
 
 # Converting a stdlib filename into native compiler filenames
 # Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*)))))
 
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o)))))
+
+ifdef QUICK
+GLOBFILES:=
+else
+GLOBFILES:=$(ALLVO:.$(VO)=.glob)
+endif
 
-GLOBFILES:=$(ALLVO:.vo=.glob)
 ifdef NATIVECOMPUTE
 NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO))
 else
 NATIVEFILES :=
 endif
-LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
+LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES)
 
 # For emacs:
 # Local Variables:
-- 
cgit v1.2.3