Add tool to combine sharded csv metrics

util/misc/merge-csv.py

@@ -0,0 +1,27 @@
+#!/usr/bin/env python3
+import argparse
+import csv
+import sys
+
+
+def main(infile, outfile):
+    metrics = {}
+    metric_names = []
+
+    for metric, total, bench in csv.reader(infile):
+        assert total == bench
+        if metric not in metrics:
+            metric_names.append(metric)
+
+        metrics.setdefault(metric, []).append(bench)
+
+    writer = csv.writer(outfile)
+    for metric in metric_names:
+        try:
+            writer.writerow([metric, sum(metrics[metric]), *metrics[metric]])
+        except TypeError:
+            writer.writerow([metric, 'Total', *metrics[metric]])
+
+
+if __name__ == '__main__':
+    main(sys.stdin, sys.stdout)