diff options
| author | letouzey | 2012-10-04 18:16:27 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-04 18:16:27 +0000 |
| commit | 41451e5ec3136b153fcc5af00c8bb4af870a498c (patch) | |
| tree | 8e9f2207ddee7afb78c9fb794f7f082fd3049a76 | |
| parent | 88e15b0bd942b4a316afa660da04b6639bccd2dd (diff) | |
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
| -rw-r--r-- | Makefile.build | 23 |
1 files 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. |