Allow a few build system optimisations/corner-cutting

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

4 files changed, 103 insertions, 31 deletions

diff --git a/Makefile b/Makefile
index f97a2b98e1..536dfc3bc6 100644
--- a/Makefile
+++ b/Makefile
@@ -24,13 +24,34 @@
 # by Emacs' next-error.
 ###########################################################################
 
+FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or
+FIND_PRINTF_P:=-print | sed 's|^\./||'
+
+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 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
+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 ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
+export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P))
+export CFILES   := $(shell find kernel/byterun -name '*.c')
+
+export ML4FILESML:= $(ML4FILES:.ml4=.ml)
+
 include Makefile.common
 
 NOARG: world
 
-.PHONY: stage1 stage2 stage3 NOARG help world revision always tags otags
+.PHONY: NOARG help always tags otags
 
-always:
+always: ;
 
 help:
 	@echo "Please use either"
@@ -66,6 +87,19 @@ Or your editor crashed. Then, you may want to consider whether you want to resto
 #run.
 endif
 
+ifdef GOTO_STAGE
+config/Makefile Makefile.common Makefile.build Makefile: ;
+
+.DEFAULT:
+	$(call stage-template,$(GOTO_STAGE))
+else
+
+.PHONY: stage1 stage2 stage3 world revision
+
+# This is to remove the built-in rule "%: %.o"
+# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
+%: %.o
+
 %.o: always
 	$(call stage-template,1)
 
@@ -73,8 +107,17 @@ endif
 stage1 $(STAGE1_TARGETS): always
 	$(call stage-template,1)
 
-%.cmo %.cmx %.cmi %.cma %.cmxa %.ml4.preprocessed: stage1
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa
+ifdef CM_STAGE1
+$(CAML_OBJECT_PATTERNS): always
+	$(call stage-template,1)
+
+%.ml4.preprocessed: stage1
+	$(call stage-template,2)
+else
+$(CAML_OBJECT_PATTERNS) %.ml4.preprocessed: stage1
 	$(call stage-template,2)
+endif
 
 stage2 $(STAGE2_TARGETS): stage1
 	$(call stage-template,2)
@@ -85,11 +128,13 @@ stage2 $(STAGE2_TARGETS): stage1
 stage3 $(STAGE3_TARGETS): stage2
 	$(call stage-template,3)
 
+endif #GOTO_STAGE
+
 ###########################################################################
 # Cleaning
 ###########################################################################
 
-.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide depclean distclean cleanconfig cleantheories docclean
+.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean
 
 clean: objclean cruftclean depclean docclean
 
@@ -134,8 +179,11 @@ clean-ide:
 ml4clean:
 	rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4.preprocessed)
 
+ml4depclean:
+	find . -name '*.ml4.d' | xargs rm -f
+
 depclean:
-	find . -name '*.d' | xargs  rm -f
+	find . -name '*.d' | xargs rm -f
 
 cleanconfig:
 	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
@@ -190,7 +238,3 @@ ifdef COQ_CONFIGURED
 else
 	@echo "Please run ./configure first" >&2; exit 1
 endif
-
-# This is to remove the built-in rule "%: %.o"
-# Otherwise, "make foo" recurses into stage1, trying to build foo.o .
-%: %.o
diff --git a/Makefile.build b/Makefile.build
index 4a57994bc2..35b7d429ec 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -811,9 +811,14 @@ endif
 
 # .ml4.d contains the dependencies to generate the .ml from the .ml4
 # NOT to generate object code.
+ifdef NO_RECOMPILE_ML4
+  SEP:=$(ORDER_ONLY_SEP)
+else
+  SEP:=
+endif
 %.ml4.d: %.ml4
 	$(SHOW)'CAMLP4DEPS $<'
-	$(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: ' && $(CAMLP4DEPS) "$<" ) > "$@" \
+	$(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: $(SEP)' && $(CAMLP4DEPS) "$<" ) > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.ml4.ml.d: %.ml4 | $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d
diff --git a/Makefile.common b/Makefile.common
index ba911adb07..99742b4360 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -433,27 +433,6 @@ PRINTERSCMO:=\
   toplevel/cerrors.cmo toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \
   dev/top_printers.cmo
 
-FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or
-FIND_PRINTF_P:=-print | sed 's|^\./||'
-
-YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P))
-LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P))
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
-  scripts/tolink.ml kernel/copcodes.ml
-GENMLIFILES:=$(YACCFILES:.mly=.mli)
-GENHFILES:=kernel/byterun/coq_jumptbl.h
-GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
-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)
-MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
-  $(GENMLIFILES)
-ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P))
-CFILES   := $(shell find kernel/byterun -name '*.c')
-
-ML4FILESML:= $(ML4FILES:.ml4=.ml)
-
 ###########################################################################
 # vo files
 ###########################################################################
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 516664720c..5b71dc9c92 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -40,6 +40,50 @@ files. In particular, .glob files are now always created.
 
 See also section "cleaning targets"
 
+Reducing build system overhead
+------------------------------
+
+When you are actively working on a file in a "make a change, make to
+test, make a change, make to test", etc mode, here are a few tips to
+save precious time:
+
+ - Always ask for what you want directly (e.g. bin/coqtop,
+   foo/bar.cmo, ...), don't do "make world" and interrupt
+   it when it has done what you want. This will try to minimise the
+   stage at which what you ask for is done (instead of maximising it
+   in order to maximise parallelism of the build process).
+
+   For example, if you only want to test whether bin/coqtop still
+   builds (and eventually start it to test your bugfix or new
+   feature), don't do "make world" and interrupt it when bin/coqtop is
+   built. Use "make bin/coqtop" or "make coqbinaries" or something
+   like that. This will avoid entering the stage 3, and cut build
+   system overhead by 50% (1.2s instead of 2.4 on writer's machine).
+
+ - You can turn off rebuilding of the standard library each time
+   bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1.
+
+ - If you want to avoid all .ml4 files being recompiled only because
+   grammar.cma was rebuilt, do "make ml4depclean" once and then use
+   NO_RECOMPILE_ML4=1.
+
+ - The CM_STAGE1=1 option to make will build all .cm* files mentioned
+   as targets on the command line in stage1. Whether this will work is
+   your responsibility. It should work for .ml files that don't depend
+   (nor directly nor indirectly through transitive closure of the
+   dependencies) on any .ml4 file, or where those dependencies can be
+   safely ignored in the current situation (e.g. all these .ml4 files
+   don't need to be recompiled).
+
+   This will avoid entering the stage2 (a reduction of 33% in
+   overhead, 0.4s on the writer's machine).
+
+ - To jump directly into a stage (e.g. because you know nothing is to
+   be done in stage 1 or (1 and 2) or because you know that the target
+   you give can be, in this situation, done in a lower stage than the
+   build system dares to), use GOTO_STAGE=n. This will jump into stage
+   n and try to do the targets you gave in that stage.
+
 Dependencies
 ------------