diff options
-rw-r--r-- | Makefile | 9 | ||||
-rw-r--r-- | Makefile.build | 17 | ||||
-rw-r--r-- | Makefile.common | 15 |
3 files changed, 22 insertions, 19 deletions
@@ -59,20 +59,11 @@ define find $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') endef -define findx - $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||') -endef - -# We now discriminate .ml4 files according to their need of grammar.cma -# or q_constr.cmo -USEGRAMMAR := '(\*.*camlp4deps.*grammar' - ## Files in the source tree YACCFILES:=$(call find, '*.mly') LEXFILES := $(call find, '*.mll') export MLLIBFILES := $(call find, '*.mllib') -export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR)) export ML4FILES := $(call find, '*.ml4') export CFILES := $(call find, '*.c') diff --git a/Makefile.build b/Makefile.build index 760a4db72..f8895b2ed 100644 --- a/Makefile.build +++ b/Makefile.build @@ -25,13 +25,20 @@ world: revision coq coqide documentation include Makefile.common include Makefile.doc -# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma) +MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) + +# In a first phase (when BUILDGRAMMAR=1), we restrict the considered +# files to some specific directories (up to grammar/), not considering +# the grammar-dependent .ml4 (which are in tactics/ toplevel/ plugins/) + +GRAMONLY := $(addsuffix /%,$(GRAMSRCDIRS)) ifdef BUILDGRAMMAR - MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml) - CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib + CURSRCDIRS := $(GRAMSRCDIRS) + CURFILES := \ + $(filter $(GRAMONLY), $(MLFILES) $(MLIFILES) $(ML4FILES)) grammar/grammar.mllib else - MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) + CURSRCDIRS := $(SRCDIRS) CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES) endif @@ -91,7 +98,7 @@ BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) -LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) +LOCALINCLUDES := $(addprefix -I , $(CURSRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) OCAMLC := $(OCAMLC) $(CAMLFLAGS) diff --git a/Makefile.common b/Makefile.common index 966829d5a..ceafbf474 100644 --- a/Makefile.common +++ b/Makefile.common @@ -59,16 +59,21 @@ COQBINARIES:= $(COQMKTOP) $(COQC) \ CSDPCERT:=plugins/micromega/csdpcert$(EXE) -CORESRCDIRS:=\ - config lib kernel kernel/byterun library \ - proofs tactics pretyping interp toplevel \ - parsing printing grammar intf +# Minimal set of source directories for building grammar.cma +# Invariant: the .ml4 there shouldn't use grammar.cma +# (the grammar-dependent .ml4 are in tactics, toplevel, plugins) +GRAMSRCDIRS:=\ + config lib intf kernel kernel/byterun library \ + pretyping interp proofs parsing grammar + +CORESRCDIRS:= $(GRAMSRCDIRS) printing tactics toplevel PLUGINS:=\ omega romega micromega quote \ setoid_ring xml extraction fourier \ cc funind firstorder Derive \ - rtauto nsatz syntax decl_mode btauto + rtauto nsatz syntax decl_mode \ + btauto SRCDIRS:=\ $(CORESRCDIRS) \ |