Makefile: no more separate stages

 - Instead of the separate stage mechanism, we let make handle the
   build and inclusion of all .d. Some initial calls to camlp4o
   will fail, but make tries again later, and this finally works
   great. These initial error message are made nice to avoid bad
   interaction with M-x next-error

 - The only recursive call to a sub-make is Makefile calling Makefile.build
   in which the includes of .d take place. This allows to avoid compiling
   anything for a make clean or make tags

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

5 files changed, 54 insertions, 179 deletions

diff --git a/Makefile b/Makefile
index 7fc5e331b5..6501ccd50a 100644
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,6 @@
 
 # Specific command-line options to this Makefile
 #
-# make GOTO_STAGE=N        # perform only stage N (with N=1,2)
 # make VERBOSE=1           # restore the raw echoing of commands
 # make NO_RECALC_DEPS=1    # avoid recomputing dependencies
 # make NO_RECOMPILE_LIB=1  # a coqtop rebuild does not trigger a stdlib rebuild
@@ -58,7 +57,7 @@
 #
 # * Useful builtin functions
 #
-# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...)
+# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...)
 #
 # * Behavior of -include
 #
@@ -138,9 +137,7 @@ include Makefile.common
 
 NOARG: world
 
-.PHONY: NOARG help always tags otags
-
-always: ;
+.PHONY: NOARG help always
 
 help:
 	@echo "Please use either"
@@ -152,60 +149,33 @@ 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 '*****************************************************'
-	@echo '*****************************************************'
-	@echo '****************** Entering stage$(1) ******************'
-	@echo '*****************************************************'
-	@echo '*****************************************************'
-	+$(MAKE) $(MAKEFLGS) -f Makefile.stage$(1) "$@"
-endef
-else
-define stage-template
-	@echo "Please run ./configure first" >&2; exit 1
-endef
-endif
-
-UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.mli' -o -name '.\#*.ml4')
+UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
 ifdef UNSAVED_FILES
-$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; cancel them or save before proceeding. \
-Or your editor crashed. Then, you may want to consider whether you want to restore the autosaves)
+$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \
+cancel them or save before proceeding. Or your editor crashed. \
+Then, you may want to consider whether you want to restore the autosaves)
 #If you try to simply remove this explicit test, the compilation may
 #fail later. In particular, if a .#*.v file exists, coqdep fails to
 #run.
 endif
 
-ifdef GOTO_STAGE
-config/Makefile Makefile.common Makefile.build Makefile: ;
+# Apart from clean and tags, everything will be done in a sub-call to make
+# on Makefile.build. This way, we avoid doing here the -include of .d :
+# since they trigger some compilations, we do not want them for a mere clean
 
-%: always
-	$(call stage-template,$(GOTO_STAGE))
+ifdef COQ_CONFIGURED
+%:: always
+	$(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@"
 else
+%:: always
+	@echo "Please run ./configure first" >&2; exit 1
+endif
 
-.PHONY: stage1 stage2 world revision
-
-stage1 $(STAGE1_TARGETS) : always
-	$(call stage-template,1)
-
-stage2 $(STAGE2_TARGETS) : stage1
-	$(call stage-template,2)
-
-# Nota:
-# - world is one of the targets in $(STAGE2_TARGETS), hence launching
-# "make" or "make world" leads to recursion into stage1 then stage2
-# - the aim of stage1 is to build grammar.cma and q_constr.cmo
-# More details in dev/doc/build-system*.txt
-
+always : ;
 
-# This is to remove the built-in rule "%: %.o" :
-%: %.o
-# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
+# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
 
-endif #GOTO_STAGE
+Makefile Makefile.build Makefile.common config/Makefile : ;
 
 ###########################################################################
 # Cleaning
@@ -292,6 +262,8 @@ devdocclean:
 # Emacs tags
 ###########################################################################
 
+.PHONY: tags otags
+
 tags:
 	echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
 	etags --language=none\
diff --git a/Makefile.build b/Makefile.build
index eb1ab45bed..e06c80596b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -24,25 +24,45 @@
 # by Emacs' next-error.
 ###########################################################################
 
-include Makefile.common
-ifndef COQ_CONFIGURED
- $(error Please run ./configure first)
-endif
-
-.PHONY: NOARG
-
-NOARG: world
+###########################################################################
+# Starting rule
+###########################################################################
 
 # build and install the three subsystems: coq, coqide
 world: revision coq coqide
 install: install-coq install-coqide
 
+.PHONY: world install
+
+###########################################################################
+# Includes
+###########################################################################
+
+include Makefile.common
+include Makefile.doc
+
 ifeq ($(WITHDOC),all)
 world: doc
 install: install-doc
 endif
 
-#install-manpages: install-coq-manpages
+# All dependency includes must be declared secondary, otherwise make will
+# delete 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.
+
+ALLDEPS=$(addsuffix .d, \
+  $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES))
+
+.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES)
+
+# NOTA: the -include below will lauch the build of all .d. Some of them
+# will _fail_ at first, this is to be expected (no grammar.cma initially).
+# These errors (see below "not ready yet, will try again later") do not
+# discourage make to try again and finally succeed.
+
+-include $(ALLDEPS)
+
 
 ###########################################################################
 # Compilation options
@@ -662,7 +682,7 @@ parsing/grammar.cma: | parsing/grammar.mllib.d
 ## of the ml4
 
 toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
-	$(SHOW)'OCAMLOPT    $<'
+	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
 
 toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
@@ -764,7 +784,7 @@ $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo
 %.cmx: %.ml | %.ml.d
 	$(SHOW)'OCAMLOPT  $<'
 	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c -o $*.tmp.cmx $< && \
-	  rm -f $*.tmp.cmi && mv -f $*.tmp.o $*.o && mv -f $*.tmp.cmx $*.cmx
+          rm -f $*.tmp.cmi && mv -f $*.tmp.o $*.o && mv -f $*.tmp.cmx $*.cmx
 
 %.cmxs: %.cmxa
 	$(SHOW)'OCAMLOPT -shared -o $@'
@@ -791,11 +811,11 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
 	$(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@
 
-.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
-
 %.ml: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET)
+	$(HIDE)if ls `$(CAMLP4DEPS) $<` > /dev/null 2>&1; then \
+	       $(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET); \
+	       else echo Dependencies `$(CAMLP4DEPS) $<` not ready yet, will try again later; false; fi
 
 %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
@@ -860,8 +880,6 @@ 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) $(GENML4FILES)
-
 ###########################################################################
 # this sets up developper supporting stuff
 ###########################################################################
diff --git a/Makefile.common b/Makefile.common
index 8a29988d52..62a22d8b9b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -261,20 +261,6 @@ COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo output.cmo cpretty.cmo main.cmo )
 COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
 
-# grammar modules with camlp4
-
-GRAMMARCMA:=parsing/grammar.cma
-
-GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \
-  parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \
-  parsing/g_prim.ml4 parsing/g_tactic.ml4 \
-  parsing/g_ltac.ml4 parsing/g_constr.ml4 \
-  parsing/lexer.ml4 parsing/q_coqast.ml4
-
-STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4
-STAGE1:=parsing/grammar.cma parsing/q_constr.cmo
-
-
 ###########################################################################
 # vo files
 ###########################################################################
@@ -364,52 +350,6 @@ DATE=$(shell LANG=C date +"%B %Y")
 
 SOURCEDOCDIR=dev/source-doc
 
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
-
-### Targets forwarded by Makefile to a specific stage:
-
-## Enumeration of targets that require being done at stage1
-
-STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
-  $(GENFILES) \
-  source-doc revision toplevel/mltop.ml toplevel/mltop.optml \
-  $(STAGE1_ML4:.ml4=.ml) %.o
-
-ifdef CM_STAGE1
- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
-endif
-
-## Enumeration of targets that require being done at stage2
-
-VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
-  fsets relations wellfounded ints reals \
-  setoids sorting natural integer rational numbers noreal \
-  omega micromega ring setoid_ring dp xml extraction field fourier \
-  funind cc subtac rtauto
-
-DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \
-  rectutorial refman-quick refman-nodep stdlib-nodep \
-  install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url \
-  ide/index_urls.txt
-
-DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva
-
-STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
-  interp parsing pretyping highparsing toplevel hightactics \
-  coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
-  $(CSDPCERT) coqbinaries $(TOOLS) tools \
-  printers debug initplugins plugins \
-  world install coqide coqide-files coq coqlib \
-  coqlight states check init theories theories-light \
-  $(DOC_TARGETS) $(VO_TARGETS) validate \
-  %.vo %.glob states/% install-% \
-  $(DOC_TARGET_PATTERNS)
-
-ifndef CM_STAGE1
- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
-endif
-
-
 # For emacs: 
 # Local Variables: 
 # mode: makefile 
diff --git a/Makefile.stage1 b/Makefile.stage1
deleted file mode 100644
index 93d54eef91..0000000000
--- a/Makefile.stage1
+++ /dev/null
@@ -1,32 +0,0 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
-
-include Makefile.build
-
-# All includes must be declared secondary, otherwise make will delete
-# 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.
-
-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)
-
-# For emacs: 
-# Local Variables: 
-# mode: makefile 
-# End:
diff --git a/Makefile.stage2 b/Makefile.stage2
deleted file mode 100644
index e6a61b8e44..0000000000
--- a/Makefile.stage2
+++ /dev/null
@@ -1,23 +0,0 @@
-#######################################################################
-#  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
-# <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
-#   \VV/  #############################################################
-#    //   #      This file is distributed under the terms of the      #
-#         #       GNU Lesser General Public License Version 2.1       #
-#######################################################################
-
-include Makefile.stage1
-include Makefile.doc
-
-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: 
-# mode: makefile 
-# End: