From 2074187fff574d29f5b43ed6fa85dedcb0ec608f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 11:25:01 +0100
Subject: [PATCH] make plots with many lines more readable

---
 benchmark/visualize.py | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/benchmark/visualize.py b/benchmark/visualize.py
index ab8008e15..5a2990cfb 100755
--- a/benchmark/visualize.py
+++ b/benchmark/visualize.py
@@ -1,5 +1,5 @@
 #!/usr/bin/env python3
-import argparse, sys, pprint
+import argparse, sys, pprint, itertools
 import matplotlib.pyplot as plt
 import parse_log
 
@@ -10,17 +10,19 @@ parser.add_argument("-f", "--file",
                     help="Filename to get the data from.")
 parser.add_argument("-t", "--timings", nargs='+',
                     dest="timings",
-                    help="The names of the Coq files (without the extension) whose timings should be extracted")
+                    help="The names of the Coq files (with or without the extension) whose timings should be extracted")
 args = parser.parse_args()
 pp = pprint.PrettyPrinter()
 log_file = sys.stdin if args.file == "-" else open(args.file, "r")
 
-results = list(parse_log.parse(log_file, args.timings))
+timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
+results = list(parse_log.parse(log_file, timings))
 
-for timing in args.timings:
-    plt.plot(list(map(lambda r: r.times[timing], results)))
+markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
+for timing in timings:
+    plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
 
-plt.legend(args.timings)
+plt.legend(timings)
 plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
 plt.subplots_adjust(bottom=0.2) # more space for the commit labels
 
-- 
GitLab