diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 48 |
1 files changed, 33 insertions, 15 deletions
diff --git a/Makefile.build b/Makefile.build index 3c32e5bcc2..6590f5f308 100644 --- a/Makefile.build +++ b/Makefile.build @@ -50,6 +50,12 @@ VALIDATE ?= # When non-empty, passed as extra arguments to coqtop/coqc: COQUSERFLAGS ?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -104,6 +110,19 @@ include Makefile.dev ## provides the 'printers' and 'revision' rules ########################################################################### # Timing targets ########################################################################### +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + 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:: @@ -111,21 +130,21 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(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) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_REAL_ARG) $(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) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_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' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-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' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-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) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -809,21 +828,20 @@ $(USERCONTRIBMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter user-contrib/%, $(ML # NB: for make world, no need to mention explicitly the .cmxs of the plugins, # since they are all mentioned in at least one Declare ML Module in some .v -coqlib: theories plugins +coqlib: stdlib-vo contrib-vo ifdef QUICK - $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' - $(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(PLUGINSVO) + $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio' + $(HIDE)$(BOOTCOQC) -schedule-vio2vo $(NJOBS) $(THEORIESVO) $(CONTRIBVO) endif -coqlib.timing.diff: theories.timing.diff plugins.timing.diff +coqlib.timing.diff: stdlib.timing.diff -theories: $(THEORIESVO) -plugins: $(PLUGINSVO) +stdlib-vo: $(THEORIESVO) +contrib-vo: $(CONTRIBVO) -theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff) -plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff) +stdlib.timing.diff: $(ALLVO:.$(VO)=.v.timing.diff) -.PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff +.PHONY: coqlib stdlib-vo contrib-vo coqlib.timing.diff stdlib.timing.diff # The .vo files in Init are built with the -noinit option @@ -859,7 +877,7 @@ endif $(HIDE)$(BOOTCOQC) $< -vio -noglob %.v.timing.diff: %.v.before-timing %.v.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)'PYTHON TIMING-DIFF $*.v.{before,after}-timing' $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" |