From 1b4bc997554894d4a317eae965f4634e04c11d20 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 27 Dec 2017 22:32:11 -0500 Subject: Add TIMING_SORT_BY and --sort-by to timing scripts This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 --- test-suite/coq-makefile/timing/run.sh | 4 ++-- tools/CoqMakefile.in | 6 ++++-- tools/TimeFileMaker.py | 28 ++++++++++++++++++++++++---- tools/make-both-single-timing-files.py | 18 ++++++------------ tools/make-both-time-files.py | 18 ++++++------------ 5 files changed, 42 insertions(+), 32 deletions(-) diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 898af5590..4cff224c7 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -31,9 +31,9 @@ coq_makefile -f _CoqProject -o Makefile make cleanall make make-pretty-timed-after TGTS="all" -j1 || exit $? rm -f time-of-build-before.log -make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +make print-pretty-timed-diff TIMING_SORT_BY=diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log cp ../before/time-of-build-before.log ./ -make print-pretty-timed-diff || exit $? +make print-pretty-timed-diff TIMING_SORT_BY=diff || exit $? INFINITY="∞" INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected the time to increase diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 33a2f8593..904cd8532 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -119,6 +119,8 @@ CAMLPKGS ?= # Option for making timing files TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -334,7 +336,7 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: 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) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(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' @@ -346,7 +348,7 @@ print-pretty-single-time-diff:: $(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) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a5a5fa8fe..0d24332f1 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -10,6 +10,20 @@ STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' INFINITY = '\xe2\x88\x9e' +def parse_args(argv, USAGE, HELP_STRING): + sort_by = 'auto' + if any(arg.startswith('--sort-by=') for arg in argv[1:]): + sort_by = [arg for arg in argv[1:] if arg.startswith('--sort-by=')][-1][len('--sort-by='):] + args = [arg for arg in argv if not arg.startswith('--sort-by=')] + if len(args) < 3 or '--help' in args[1:] or '-h' in args[1:] or sort_by not in ('auto', 'absolute', 'diff'): + print(USAGE) + if '--help' in args[1:] or '-h' in args[1:]: + print(HELP_STRING) + if len(args) == 2: sys.exit(0) + sys.exit(1) + return sort_by, args + + def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) @@ -108,6 +122,7 @@ def format_percentage(num, signed=True): return sign + '%d.%02d%%' % (whole_part, frac_part) def make_diff_table_string(left_times_dict, right_times_dict, + sort_by='auto', descending=True, left_tag="After", tag="File Name", right_tag="Before", with_percent=True, change_tag="Change", percent_change_tag="% Change"): @@ -125,10 +140,15 @@ def make_diff_table_string(left_times_dict, right_times_dict, if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A'))) for name, lseconds, rseconds in prediff_times) # update to sort by approximate difference, first - get_key = make_sorting_key(all_names_dict, descending=descending) - all_names_dict = dict((name, (fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending), get_key(name))) - for name in all_names_dict.keys()) - names = sorted(all_names_dict.keys(), key=all_names_dict.get) + get_key_abs = make_sorting_key(all_names_dict, descending=descending) + get_key_diff = (lambda name: fix_sign_for_sorting(int(abs(to_seconds(diff_times_dict[name]))), descending=descending)) + if sort_by == 'absolute': + get_key = get_key_abs + elif sort_by == 'diff': + get_key = get_key_diff + else: # sort_by == 'auto' + get_key = (lambda name: (get_key_diff(name), get_key_abs(name))) + names = sorted(all_names_dict.keys(), key=get_key) #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending) # set the widths of each of the columns by the longest thing to go in that column left_sum = sum_times(left_times_dict.values()) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index 2d33503c3..32c52c7a1 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -3,16 +3,10 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_single_file_times(sys.argv[1]) - right_dict = get_single_file_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code") - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_single_file_times(args[1]) + right_dict = get_single_file_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) + print_or_write_table(table, args[3:]) diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 69ec5a663..f730a8d6b 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -3,20 +3,14 @@ import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] + USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0] HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table. The input is expected to contain lines in the format: FILE_NAME (...user: NUMBER_IN_SECONDS...) ''' - if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(USAGE) - if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]: - print(HELP_STRING) - if len(sys.argv) == 2: sys.exit(0) - sys.exit(1) - else: - left_dict = get_times(sys.argv[1]) - right_dict = get_times(sys.argv[2]) - table = make_diff_table_string(left_dict, right_dict) - print_or_write_table(table, sys.argv[3:]) + sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) + left_dict = get_times(args[1]) + right_dict = get_times(args[2]) + table = make_diff_table_string(left_dict, right_dict, sort_by=sort_by) + print_or_write_table(table, args[3:]) -- cgit v1.2.3