aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-24 18:37:24 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-24 18:37:24 +0100
commit1d933c489d1f9d064fd54a4487754a86a0aed506 (patch)
tree14ecb62f587e132c168383f5cae2e05314a543e7
parent67319cef77a215163032ea94f28f8c21dcf64f3a (diff)
Revert "Makefile: the initial build of grammar.cma is now directory-driven"
This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022. This commit was wrong, since (at least) the highparsing part depends on the toplevel directory. I still didn't had time to fix that, so in the meantime let's revert it.
-rw-r--r--Makefile9
-rw-r--r--Makefile.build17
-rw-r--r--Makefile.common15
3 files changed, 19 insertions, 22 deletions
diff --git a/Makefile b/Makefile
index 109196bea..5f5397fa7 100644
--- a/Makefile
+++ b/Makefile
@@ -59,11 +59,20 @@ 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 363f5574e..c79b21f40 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -25,20 +25,13 @@ world: revision coq coqide documentation
include Makefile.common
include Makefile.doc
-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))
+# In a first phase, we restrict to the basic .ml4 (the ones without grammar.cma)
ifdef BUILDGRAMMAR
- CURSRCDIRS := $(GRAMSRCDIRS)
- CURFILES := \
- $(filter $(GRAMONLY), $(MLFILES) $(MLIFILES) $(ML4FILES)) grammar/grammar.mllib
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4BASEFILES:.ml4=.ml)
+ CURFILES := $(MLFILES) $(MLIFILES) $(ML4BASEFILES) grammar/grammar.mllib
else
- CURSRCDIRS := $(SRCDIRS)
+ MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
CURFILES := $(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(CFILES) $(VFILES)
endif
@@ -98,7 +91,7 @@ BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
-LOCALINCLUDES := $(addprefix -I , $(CURSRCDIRS) )
+LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
OCAMLC := $(OCAMLC) $(CAMLFLAGS)
diff --git a/Makefile.common b/Makefile.common
index 41b45d97e..7425d99af 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -59,21 +59,16 @@ COQBINARIES:= $(COQMKTOP) \
CSDPCERT:=plugins/micromega/csdpcert$(EXE)
-# 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
+CORESRCDIRS:=\
+ config lib kernel kernel/byterun library \
+ proofs tactics pretyping interp toplevel \
+ parsing printing grammar intf
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) \