diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-24 18:37:24 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-24 18:37:24 +0100 |
commit | 1d933c489d1f9d064fd54a4487754a86a0aed506 (patch) | |
tree | 14ecb62f587e132c168383f5cae2e05314a543e7 | |
parent | 67319cef77a215163032ea94f28f8c21dcf64f3a (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-- | Makefile | 9 | ||||
-rw-r--r-- | Makefile.build | 17 | ||||
-rw-r--r-- | Makefile.common | 15 |
3 files changed, 19 insertions, 22 deletions
@@ -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) \ |