From f694544d016b085b3cd10007b9f7716ae2c3b022 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 1 Mar 2014 21:21:09 +0100 Subject: Makefile: the initial build of grammar.cma is now directory-driven In last commit, we used grep to decide whether a .ml4 could be compiled during the initial phase of not. Instead, we now rely on a simpler directory dichotomy: - config lib kernel library pretyping interp parsing grammar are considered initial (and shouldn't contain grammar-dependent .ml4), see $(GRAMSRCDIRS) in Makefile.common - the grammar-dependent .ml4 could be in any other directories Currently, they are in: tactics toplevel plugins/* --- Makefile.common | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'Makefile.common') 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) \ -- cgit v1.2.3