From 41451e5ec3136b153fcc5af00c8bb4af870a498c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 4 Oct 2012 18:16:27 +0000
Subject: Makefile.build: easier compilation with timings info

 On a reasonable platform equipped with a /usr/bin/time, a simple
 "make TIMED=1" should provide you with timings of the .v compilations.

 If you don't have /usr/bin/time, or prefer a different output format,
 you can still do a "make TIMECMD='...'".

 For storing the timings in a spreadsheet, simply do:
 "make TIMED=1 2> timings.csv"
 and then import this csv in your favorite office program,
 with whitespace as separator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/Makefile.build b/Makefile.build
index 7a1058f10a..cb5672cae5 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -72,15 +72,26 @@ READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
-TIMECMD=	# is "'time -p'" to get compilation time of .v
 
-# NB: variable TIME, if set, is the formatting string for unix command 'time'.
-# For instance:
-# TIME="%C (%U user, %S sys, %e total, %M maxres)"
+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'"
+
+# 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
+
+# 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) $(VM)
-BOOTCOQTOP:=$(TIMECMD) $(COQTOPEXE) -boot $(COQOPTS)
-BOOTCOQC:=$(BOOTCOQTOP) -compile
+BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
 # or only abbreviated versions. 
-- 
cgit v1.2.3