diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2017-03-23 12:56:24 +0100 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2017-06-01 17:33:19 +0200 |
| commit | 718d61a54157733bca61ed84c0ba3761cd52720f (patch) | |
| tree | 4c57fa4ad6d75c5fc4f5747289dfed82d83dfc9a /Makefile.common | |
| parent | 7fff12d45c4d86fa5cb9be3883084ffef5911405 (diff) | |
drop vo.itarget files and compute the corresponding the corresponding values automatically instead
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/Makefile.common b/Makefile.common index d5f79d76b..b936eb4c7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -146,14 +146,16 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ## we now retrieve the names of .vo file to compile in */vo.itarget files -THEORIESVO:= $(foreach f, $(wildcard theories/*/vo.itarget), \ - $(addprefix $(dir $(f)),$(shell cat $(f)))) +GENVOFILES := $(GENVFILES:.v=.vo) -PLUGINSVO:= $(foreach f, $(wildcard plugins/*/vo.itarget), \ - $(addprefix $(dir $(f)),$(shell cat $(f)))) +THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \ + $(filter theories/%, $(GENVOFILES)) -ALLVO:= $(THEORIESVO) $(PLUGINSVO) -VFILES:= $(ALLVO:.vo=.v) +PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) \ + $(filter plugins/%, $(GENVOFILES)) + +ALLVO := $(THEORIESVO) $(PLUGINSVO) +VFILES := $(ALLVO:.vo=.v) ## More specific targets @@ -175,11 +177,10 @@ vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theo vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) -LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \ - $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \ - $(call vo_to_obj,$(PLUGINSVO)) \ - $(PLUGINSVO:.vo=.v) $(THEORIESVO:.vo=.v) \ - $(PLUGINSVO:.vo=.glob) $(THEORIESVO:.vo=.glob) +GLOBFILES:=$(ALLVO:.vo=.glob) +LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \ + $(call vo_to_obj,$(ALLVO)) \ + $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: |