diff options
| -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. |