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 --- tools/make-both-time-files.py | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'tools/make-both-time-files.py') 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