Makefile: cleanup of variables containing lists of files, such as MLFILES

 - We clarify their definition via some custom make function: find, diff...
 - We avoid duplications via some $(sort ...)
 - Some name changes:
    * old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from
      .mly and .mll aren't in it anymore).
    * new $(MLFILES) contains all .ml, either static or generated from
      .mly .mll .ml4 or _mod.ml made out of .mllib
    * $(ML4FILESML) is now $(GENML4FILES)
    ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 72 insertions, 46 deletions

diff --git a/Makefile b/Makefile
index f6bafc5a1b..7fc5e331b5 100644
--- a/Makefile
+++ b/Makefile
@@ -66,6 +66,10 @@
 # but doesn't care if this build fails. This can be quite surprising,
 # see in particular the -include in Makefile.stage*
 
+###########################################################################
+# File lists
+###########################################################################
+
 # !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
 # !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt         !!
 export FIND_VCS_CLAUSE:='(' \
@@ -78,36 +82,60 @@ export FIND_VCS_CLAUSE:='(' \
   -name "$${GIT_DIR}" -o \
   -name '_build' \
 ')' -prune -o
-export PRUNE_CHECKER := -wholename ./checker/\* -prune -o
 
-FIND_PRINTF_P:=-print | sed 's|^\./||'
+define find
+ $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
+endef
+
+## Files in the source tree
+
+export YACCFILES:=$(call find, '*.mly')
+export LEXFILES := $(call find, '*.mll')
+export MLLIBFILES := $(call find, '*.mllib')
+export ML4FILES := $(call find, '*.ml4')
+export CFILES := $(call find, '*.c')
+
+# NB: The lists of currently existing .ml and .mli files will change
+# before and after a build or a make clean. Hence we do not export
+# these variables, but cleaned-up versions (see below MLFILES and co)
+
+EXISTINGML := $(call find, '*.ml')
+EXISTINGMLI := $(call find, '*.mli')
+
+## Files that will be generated
 
-export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P))
-export LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P))
 export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
   scripts/tolink.ml kernel/copcodes.ml
 export GENMLIFILES:=$(YACCFILES:.mly=.mli)
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
-export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIND_PRINTF_P) | \
-  while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \
-  $(GENMLFILES)
-export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
-  $(GENMLIFILES)
-export MLLIBFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mllib' ')' $(FIND_PRINTF_P))
-export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-#export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
-#  $(GENVFILES)
-export CFILES   := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) '(' -name '*.c' ')' -print)
-
-export ML4FILESML:= $(ML4FILES:.ml4=.ml)
+export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
+export GENML4FILES:= $(ML4FILES:.ml4=.ml)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
 
-# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior
-MAKEFLGS:=--warn-undefined-variable --no-builtin-rules
+# NB: all files in $(GENFILES) can be created initially, while
+# .ml files in $(GENML4FILES) might need some intermediate building.
+# That's why we keep $(GENML4FILES) out of $(GENFILES)
+
+## More complex file lists
+
+define diff
+ $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))
+endef
+
+export MLSTATICFILES := \
+ $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLFILES := \
+ $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD))
+export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
+export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml))
 
 include Makefile.common
 
+###########################################################################
+# Starting rules
+###########################################################################
+
 NOARG: world
 
 .PHONY: NOARG help always tags otags
@@ -124,6 +152,9 @@ help:
 	@echo
 	@echo "For make to be verbose, add VERBOSE=1"
 
+# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior
+MAKEFLGS:=--warn-undefined-variable --no-builtin-rules
+
 ifdef COQ_CONFIGURED
 define stage-template
 	@echo '*****************************************************'
@@ -196,7 +227,6 @@ indepclean:
 	rm -f $(GENFILES)
 	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE)
 	find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
-	find . -name '*_mod.ml' | xargs rm -f
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -238,7 +268,7 @@ clean-ide:
 	rm -f ide/utf8_convert.ml
 
 ml4clean:
-	rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed)
+	rm -f $(GENML4FILES)
 
 ml4depclean:
 	find . -name '*.ml4.d' | xargs rm -f
@@ -263,7 +293,7 @@ devdocclean:
 ###########################################################################
 
 tags:
-	echo $(MLIFILES) $(MLFILES) $(ML4FILES) | sort -r | xargs \
+	echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -278,7 +308,7 @@ tags:
 
 
 otags: 
-	echo $(MLIFILES) $(MLFILES) | sort -r | xargs otags
+	echo $(MLIFILES) $(MLSTATICFILES) | sort -r | xargs otags
 	echo $(ML4FILES) | sort -r | xargs \
 	etags --append --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
diff --git a/Makefile.build b/Makefile.build
index 85a1512410..130435f779 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -632,7 +632,7 @@ install-latex:
 
 source-doc:
 	if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
-	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLFILES)
+	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)
 
 
 ###########################################################################
@@ -846,7 +846,7 @@ checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'CCDEP     $<'
 	$(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET)
 
-.SECONDARY: $(GENFILES) $(ML4FILESML)
+.SECONDARY: $(GENFILES) $(GENML4FILES)
 
 ###########################################################################
 # this sets up developper supporting stuff
diff --git a/Makefile.stage1 b/Makefile.stage1
index b67118d01a..93d54eef91 100644
--- a/Makefile.stage1
+++ b/Makefile.stage1
@@ -12,19 +12,16 @@ include Makefile.build
 # them if it decided to build them by dependency instead of because of
 # include, and they will then be automatically deleted, leading to an
 # infinite loop.
--include $(ML4FILES:.ml4=.ml4.d)
-.SECONDARY: $(ML4FILES:.ml4=.ml4.d)
--include $(MLFILES:.ml=.ml.d)
-.SECONDARY: $(MLFILES:.ml=.ml.d)
--include $(MLIFILES:.mli=.mli.d)
-.SECONDARY: $(MLIFILES:.mli=.mli.d)
-##Depends upon the fact that all .ml4.d for stage1 files are empty
--include $(STAGE1_ML4:.ml4=.ml.d)
-.SECONDARY: $(STAGE1_ML4:.ml4=.ml.d)
--include  $(CFILES:.c=.c.d)
-.SECONDARY: $(CFILES:.c=.c.d)
--include $(MLLIBFILES:.mllib=.mllib.d)
-.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)
+
+STAGE1_DEPS := $(addsuffix .d, \
+ $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES) $(MLIFILES) $(CFILES) \
+ $(MLLIBFILES) $(STAGE1_ML4:.ml4=.ml))
+
+# NB: this depends upon the fact that .ml4.d for $(STAGE1_ML4) are empty,
+# hence .ml and .ml.d for these .ml4 can be generated initially.
+
+.SECONDARY: $(STAGE1_DEPS)
+-include $(STAGE1_DEPS)
 
 .PHONY: stage1
 stage1: $(STAGE1)
diff --git a/Makefile.stage2 b/Makefile.stage2
index a7ecddc13e..e6a61b8e44 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -9,14 +9,13 @@
 include Makefile.stage1
 include Makefile.doc
 
--include $(MLLIBFILES:.mllib=.mllib.d)
-.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)
--include $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d))
-.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml.d))
--include $(ML4FILES:.ml4=.ml.d)
-.SECONDARY: $(ML4FILES:.ml4=.ml.d)
--include $(VFILES:.v=.v.d)
-.SECONDARY: $(VFILES:.v=.v.d)
+STAGE2_DEPS := $(addsuffix .d, $(GENPLUGINSMOD) $(GENML4FILES) $(VFILES))
+
+.SECONDARY: $(STAGE2_DEPS)
+-include $(STAGE2_DEPS)
+
+# NB: all $(STAGE1_DEPS) are already included thanks to the inclusion of
+# Makefile.stage1
 
 # For emacs: 
 # Local Variables: