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 <module>
    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

7 files changed, 121 insertions, 2 deletions

diff --git a/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst
new file mode 100644
index 0000000000..4e5406ad4d
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  ``make pretty-timed-diff`` no longer raises Python exceptions in the rare
+  corner case where the log of times contains no files (`#12388
+  <https://github.com/coq/coq/pull/12388>`_, fixes `#12387
+  <https://github.com/coq/coq/pull/12387>`_, by Jason Gross).
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh
new file mode 100755
index 0000000000..4a50759bdb
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/run.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+set -x
+set -e
+
+cd "$(dirname "${BASH_SOURCE[0]}")"
+
+"$COQLIB"/tools/make-both-time-files.py time-of-build-after.log.in time-of-build-before.log.in time-of-build-both.log
+
+diff -u time-of-build-both.log.expected time-of-build-both.log || exit $?
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in
new file mode 100644
index 0000000000..1031cb85c5
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-after.log.in
@@ -0,0 +1,58 @@
+./src/Rewriter/PerfTesting/Specific/make.py primes.txt
+make --no-print-directory -C rewriter
+make[2]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/deps/coqutil
+Generating Makefile.coq.all
+make -f Makefile.coq.all
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/bedrock2 noex
+Generating Makefile.coq.noex
+rm -f .coqdeps.d
+make -f Makefile.coq.noex
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
+make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
+coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq
+COQ_MAKEFILE -f _CoqProject > Makefile.coq
+make --no-print-directory -C rewriter
+make[2]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/deps/coqutil
+Generating Makefile.coq.all
+make -f Makefile.coq.all
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/bedrock2 noex
+Generating Makefile.coq.noex
+rm -f .coqdeps.d
+make -f Makefile.coq.noex
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
+make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
+COQDEP VFILES
+make --no-print-directory -C rewriter
+make[2]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/deps/coqutil
+Generating Makefile.coq.all
+make -f Makefile.coq.all
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/bedrock2 noex
+Generating Makefile.coq.noex
+rm -f .coqdeps.d
+make -f Makefile.coq.noex
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
+make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
+COQC src/UnsaturatedSolinasHeuristics/Tests.v
+Finished transaction in 25.269 secs (24.869u,0.051s) (successful)
+src/UnsaturatedSolinasHeuristics/Tests.vo (real: 26.27, user: 25.97, sys: 0.27, mem: 566428 ko)
+DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256
+DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct
+DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions
+DIFF Crypto.Fancy.Montgomery256.montred256
+DIFF Crypto.Fancy.Barrett256.Prod.MulMod
+DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct
+DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions
+DIFF Crypto.Fancy.Barrett256.barrett_red256
+DIFF Crypto.UnsaturatedSolinasHeuristics.Tests.get_possible_limbs
+cp -f AUTHORS fiat-rust/AUTHORS
+cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS
+cp -f LICENSE fiat-rust/LICENSE
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in
new file mode 100644
index 0000000000..b78039b589
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-before.log.in
@@ -0,0 +1,40 @@
+./src/Rewriter/PerfTesting/Specific/make.py primes.txt
+make --no-print-directory -C rewriter
+make[2]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/deps/coqutil
+Generating Makefile.coq.all
+make -f Makefile.coq.all
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/bedrock2 noex
+Generating Makefile.coq.noex
+rm -f .coqdeps.d
+make -f Makefile.coq.noex
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
+make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
+coq_makefile -f _CoqProject INSTALLDEFAULTROOT = Crypto -o Makefile-coq
+COQ_MAKEFILE -f _CoqProject > Makefile.coq
+make --no-print-directory -C rewriter
+make[2]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/deps/coqutil
+Generating Makefile.coq.all
+make -f Makefile.coq.all
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C bedrock2/bedrock2 noex
+Generating Makefile.coq.noex
+rm -f .coqdeps.d
+make -f Makefile.coq.noex
+make[3]: Nothing to be done for 'real-all'.
+make --no-print-directory -C coqprime src/Coqprime/PrimalityTest/Zp.vo
+make[1]: 'src/Coqprime/PrimalityTest/Zp.vo' is up to date.
+DIFF Crypto.Fancy.Montgomery256.Prod.MontRed256
+DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct
+DIFF Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions
+DIFF Crypto.Fancy.Montgomery256.montred256
+DIFF Crypto.Fancy.Barrett256.Prod.MulMod
+DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct
+DIFF Crypto.Fancy.Barrett256.prod_barrett_red256_correct.Assumptions
+DIFF Crypto.Fancy.Barrett256.barrett_red256
+cp -f AUTHORS fiat-rust/AUTHORS
+cp -f CONTRIBUTORS fiat-rust/CONTRIBUTORS
+cp -f LICENSE fiat-rust/LICENSE
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected
new file mode 100644
index 0000000000..6a232623bf
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/006-zero-before/time-of-build-both.log.expected
@@ -0,0 +1,5 @@
+   After |  Peak Mem | File Name                             |   Before | Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
+-------------------------------------------------------------------------------------------------------------------------------------------
+0m25.96s | 566428 ko | Total Time / Peak Mem                 | 0m00.00s |     0 ko || +0m25.96s ||    566428 ko |   N/A    |              ∞
+-------------------------------------------------------------------------------------------------------------------------------------------
+0m25.97s | 566428 ko | UnsaturatedSolinasHeuristics/Tests.vo |   N/A    |   N/A    || +0m25.96s ||    566428 ko |        ∞ |              ∞
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
index 8935759705..123b272a69 100755
--- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh
@@ -12,3 +12,4 @@ export COQLIB
 ./003-non-utf8/run.sh
 ./004-per-file-fuzz/run.sh
 ./005-correct-diff-sorting-order-mem/run.sh
+./006-zero-before/run.sh
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'))