Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4

 - With the ?= construction, we avoid warnings about undefined variables,
   while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make'

 - Some extra documentation and cleanup

2 files changed, 48 insertions, 57 deletions

diff --git a/Makefile b/Makefile
index 34ce67b7d..6649542c8 100644
--- a/Makefile
+++ b/Makefile
@@ -118,7 +118,7 @@ help:
 	@echo
 	@echo "For make to be verbose, add VERBOSE=1"
 	@echo
-	@echo "If you want camlp{4,5} to generate human-readable files, add NO_RECOMPILE_ML4=1"
+	@echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
 
 UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
 ifdef UNSAVED_FILES
diff --git a/Makefile.build b/Makefile.build
index f9f64071c..95df69c2d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -10,6 +10,40 @@
 # some variables.
 
 ###########################################################################
+# User-customizable variables
+###########################################################################
+
+# The following variables could be modified via the command-line of make,
+# either with the syntax 'make XYZ=1' or 'XYZ=1 make'
+
+# To see the actual commands launched by make instead of shortened versions,
+# set this variable to 1 (or any non-empty value):
+VERBOSE ?=
+
+# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files
+# will be generated in a human-readable format rather than in a binary format.
+READABLE_ML4 ?=
+
+# When non-empty, a time command is performed at each .v compilation.
+# To collect compilation timings of .v and import them in a spreadsheet,
+# you could hence consider: make TIMED=1 2> timings.csv
+TIMED ?=
+
+# When $(TIMED) is set, the time command used by default is $(STDTIME)
+# (see below), unless the following variable is non-empty. For instance,
+# it could be set to "'/usr/bin/time -p'".
+TIMECMD ?=
+
+# Non-empty skips the update of all dependency .d files:
+NO_RECALC_DEPS ?=
+
+# Non-empty runs the checker on all produced .vo files:
+VALIDATE ?=
+
+# Is "-xml" when building XML library:
+COQ_XML ?=
+
+###########################################################################
 # Default starting rule
 ###########################################################################
 
@@ -57,59 +91,18 @@ DEPENDENCIES := \
 # Compilation options
 ###########################################################################
 
-# Variables meant to be modifiable via the command-line of make
-
-# If you do:
-#
-#   VERBOSE=1 make
-#
-# then instead of shortened version of the commands run by make
-# you will see the actual commands.
-
-# If you do:
-#
-#   READABLE_ML4=1 make
-#
-# then *.ml files corresponding to *.ml4 files will be generated
-# in a human-readable format rather than in the binary format.
-
-NO_RECOMPILE_ML4=
-NO_RECALC_DEPS=
-VALIDATE=
-COQ_XML=	# is "-xml" when building XML library
-
-TIMED=          # non-empty will activate a default time command
-                # when compiling .v (see $(STDTIME) below)
-
-TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
-                # e.g. "'time -p'"
+# Default timing command
+STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 
-# NB: if you want to collect compilation timings of .v and import them
-# in a spreadsheet, I suggest something like:
-#   make TIMED=1 2> timings.csv
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
 # NB: do not use a variable named TIME, since this variable controls
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
-TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
-
 COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
-# The SHOW and HIDE variables control whether make will echo complete commands 
-# or only abbreviated versions. 
-# Quiet mode is ON by default except if VERBOSE=1 option is given to make
-
-ifdef VERBOSE
-SHOW := @true ""
-HIDE :=
-else
-SHOW := @echo ""
-HIDE := @
-endif
-
 LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) )
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -162,11 +155,7 @@ else
 CAMLP4USE=-D$(CAMLVERSION)
 endif
 
-ifdef READABLE_ML4
-PR_O=pr_o.cmo
-else
-PR_O=pr_dump.cmo
-endif
+PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
 
 SYSMOD:=str unix dynlink threads
 SYSCMA:=$(addsuffix .cma,$(SYSMOD))
@@ -183,6 +172,13 @@ endif
 # Infrastructure for the rest of the Makefile
 ###########################################################################
 
+# The SHOW and HIDE variables control whether make will echo complete commands
+# or only abbreviated versions.
+# Quiet mode is ON by default except if VERBOSE=1 option is given to make
+
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
 define order-only-template
  ifeq "order-only" "$(1)"
    ORDER_ONLY_SEP:=|
@@ -203,13 +199,8 @@ ifdef VALIDATE
  VO_TOOLS_DEP += $(CHICKEN)
 endif
 
-ifdef NO_RECALC_DEPS
-  D_DEPEND_BEFORE_SRC:=|
-  D_DEPEND_AFTER_SRC:=
-else
-  D_DEPEND_BEFORE_SRC:=
-  D_DEPEND_AFTER_SRC:=|
-endif
+D_DEPEND_BEFORE_SRC := $(if $(NO_RECALC_DEPS),|,)
+D_DEPEND_AFTER_SRC := $(if $(NO_RECALC_DEPS),,|)
 
 ## When a rule redirects stdout of a command to the target file : cmd > $@
 ## then the target file will be created even if cmd has failed.