From 7731b8878d6a8c78874f6657745fa61d2703ee53 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 21 May 2020 17:48:02 -0400 Subject: Fix an uncaught python exception in timing Previously, when either the 'before' or 'after' had no files, we'd get an uncaught exception: ``` Traceback (most recent call last): File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem) File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) ValueError: max() arg is an empty sequence ``` Fixes #12387 --- tools/TimeFileMaker.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tools/TimeFileMaker.py') diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a3078af4a1..12462726e5 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -387,8 +387,8 @@ def make_diff_table_string(left_dict, right_dict, total_string = 'Total' if not include_mem else 'Total Time / Peak Mem' middle_width = max(map(len, names + [tag, total_string])) - left_peak = max(v.get(MEM_KEY, 0) for v in left_dict.values()) - right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values()) + left_peak = max([0] + [v.get(MEM_KEY, 0) for v in left_dict.values()]) + right_peak = max([0] + [v.get(MEM_KEY, 0) for v in right_dict.values()]) diff_peak = left_peak - right_peak percent_diff_peak = (format_percentage((left_peak - right_peak) / float(right_peak)) if right_peak != 0 else (INFINITY if left_peak > 0 else 'N/A')) -- cgit v1.2.3