Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts

4 files changed, 40 insertions, 30 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index de113df6a..ca02c983d 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:])