Merge branch 'v8.7'

1 files changed, 100 insertions, 5 deletions

diff --git a/Makefile.build b/Makefile.build
index c00e96ea1..7703df08f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -34,6 +34,12 @@ TIMED ?=
 # it could be set to "'/usr/bin/time -p'".
 TIMECMD ?=
 
+# When non-empty, -time is passed to coqc and the output is recorded
+# in a timing file for each .v file.  If set to "before" or "after",
+# the file name for foo.v is foo.v.$(TIMING)-timing; otherwise, it is
+# foo.v.timing
+TIMING ?=
+
 # Non-empty skips the update of all dependency .d files:
 NO_RECALC_DEPS ?=
 
@@ -43,6 +49,16 @@ VALIDATE ?=
 # Is "-xml" when building XML library:
 COQ_XML ?=
 
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
+BEFORE ?=
+AFTER ?=
+
 ###########################################################################
 # Default starting rule
 ###########################################################################
@@ -53,6 +69,9 @@ world: coq coqide documentation revision
 
 coq: coqlib coqbinaries tools
 
+world.timing.diff: coq.timing.diff
+coq.timing.diff: coqlib.timing.diff
+
 # Note: 'world' does not build the bytecode binaries anymore.
 # For that, you can use the 'byte' rule. Native and byte compilations
 # shouldn't be done in a same make -j... run, otherwise both ocamlc and
@@ -60,7 +79,7 @@ coq: coqlib coqbinaries tools
 
 byte: coqbyte coqide-byte pluginsbyte printers
 
-.PHONY: world coq byte
+.PHONY: world coq byte world.timing.diff coq.timing.diff
 
 ###########################################################################
 # Includes
@@ -78,6 +97,53 @@ include Makefile.install
 include Makefile.dev      ## provides the 'printers' and 'revision' rules
 
 ###########################################################################
+# Timing targets
+###########################################################################
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff
+
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
+###########################################################################
 
 # This include below will lauch the build of all .d.
 # The - at front is for disabling warnings about currently missing ones.
@@ -101,7 +167,21 @@ DEPENDENCIES := \
 ###########################################################################
 
 # Default timing command
-STDTIME=/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+# Use /usr/bin/time on linux, gtime on Mac OS
+TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+ifneq (,$(TIMED))
+ifeq (0,$(shell /usr/bin/time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=/usr/bin/time -f $(TIMEFMT)
+else
+ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+STDTIME?=gtime -f $(TIMEFMT)
+else
+STDTIME?=time
+endif
+endif
+else
+STDTIME?=/usr/bin/time -f $(TIMEFMT)
+endif
 
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
@@ -602,18 +682,28 @@ OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 # since they are all mentioned in at least one Declare ML Module in some .v
 
 coqlib: theories plugins
+coqlib.timing.diff: theories.timing.diff plugins.timing.diff
 
 theories: $(THEORIESVO)
 plugins: $(PLUGINSVO)
 
-.PHONY: coqlib theories plugins
+theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff)
+plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff)
+
+.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff
 
 # The .vo files in Init are built with the -noinit option
 
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(SHOW)'COQC $(COQ_XML) -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< $(COQ_XML) -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA)
 
 # MExtraction.v generates the ml core file of the micromega tactic.
 # We check that this generated code is still in sync with the version
@@ -640,13 +730,18 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP)
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob
-	$(HIDE)$(BOOTCOQC) $<
+	$(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA)
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
 	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 endif
 
+%.v.timing.diff: %.v.before-timing %.v.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
+
 # Dependencies of .v files
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)