diff options
| author | Gaëtan Gilbert | 2019-01-17 18:47:46 +0000 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-17 18:47:46 +0000 |
| commit | b2877df2c79147bd2e26e53e43291b9b29a2aab8 (patch) | |
| tree | 5726b6595ef29361743b0af750f1c0524d2aa968 /Makefile.vofiles | |
| parent | 47c6f0ddacf340d4027fce181ee8ac8a0369188f (diff) | |
| parent | 44b5f77f36011e797f0d7d36098296dc7d6c1c51 (diff) | |
Merge PR #9326: [ci] compile with -quick & validate after vio2vo
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot
Diffstat (limited to 'Makefile.vofiles')
| -rw-r--r-- | Makefile.vofiles | 27 |
1 files changed, 19 insertions, 8 deletions
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: |