diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 20:36:34 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-16 20:36:34 +0200 |
commit | d0243311634a8d6fa77fb2d0bb36eab96186a605 (patch) | |
tree | 78708423b22b7b5025c4fae1d35a725de6bba830 /Makefile.vofiles | |
parent | 107e42b0776a0979e522e82654435d9f2bea7a80 (diff) |
Modify make system to include Makefile.common in the test suite
Diffstat (limited to 'Makefile.vofiles')
-rw-r--r-- | Makefile.vofiles | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/Makefile.vofiles b/Makefile.vofiles new file mode 100644 index 000000000..fc902c4a8 --- /dev/null +++ b/Makefile.vofiles @@ -0,0 +1,40 @@ + +# This file calls [find] and as such is not suitable for inclusion in +# the test suite Makefile, unlike Makefile.common. + +########################################################################### +# vo files +########################################################################### + +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) + +## More specific targets + +THEORIESLIGHTVO:= \ + $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO)) + +# convert a (stdlib) filename into a module name: +# 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)) + + +# 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_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) + +GLOBFILES:=$(ALLVO:.vo=.glob) +LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ + $(call vo_to_obj,$(ALLVO)) \ + $(VFILES) $(GLOBFILES) + +# For emacs: +# Local Variables: +# mode: makefile +# End: |