Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

benchmark/.gitignore

+__pycache__
+build-times.log

benchmark/gitlab-extract.py

 #!/usr/bin/env python3
 import argparse, pprint, subprocess, sys
 import requests
+import parse_log
+
+def last(it):
+    r = first(it) # errors out if it is empty
+    for i in it:
+        r = i
+    return r
 
 def first(it):
     for i in it:
@@ -12,7 +19,7 @@ def req(path):
     return requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
 
 # read command-line arguments
-parser = argparse.ArgumentParser(description='Update and build a bunch of stuff')
+parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab')
 parser.add_argument("-t", "--private-token",
                     dest="private_token", required=True,
                     help="The private token used to authenticate access.")
@@ -31,6 +38,13 @@ parser.add_argument("-c", "--commits",
 args = parser.parse_args()
 log_file = sys.stdout if args.file == "-" else open(args.file, "a")
 
+# determine commit, if missing
+if args.commits is None:
+    if args.file == "-":
+        raise Exception("If you do not give explicit commits, you have to give a logfile so that we can determine the missing commits.")
+    last_result = last(parse_log.parse(open(args.file, "r"), []))
+    args.commits = "{}..origin/master".format(last_result.commit)
+
 projects = req("projects")
 project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
 

benchmark/parse_log.py

+import re
+
+class Result:
+    def __init__(self, commit, times):
+        self.commit = commit
+        self.times = times
+
+def parse(file, filter):
+    '''[file] should be a file-like object, an iterator over the lines. filter should support "in" queries.
+       yields a list of Result objects giving the times of those Coq files that are "in" filter.'''
+    commit_re = re.compile("^# ([a-z0-9]+)$")
+    time_re = re.compile("^([a-zA-Z0-9_/-]+) \(user: ([0-9.]+) mem: ([0-9]+) ko\)$")
+    commit = None
+    times = None
+    for line in file:
+        # next commit?
+        m = commit_re.match(line)
+        if m is not None:
+            # previous commit, if any, is done now
+            if times is not None:
+                yield Result(commit, times)
+            # start recording next commit
+            commit = m.group(1)
+            times = {} # reset the recorded times
+            continue
+        # next file time?
+        m = time_re.match(line)
+        if m is not None:
+            name = m.group(1)
+            time = float(m.group(2))
+            if name in filter:
+                times[name] = time
+            continue
+        # nothing else we know about
+        raise Exception("Unexpected line: {}".format(line))
+    # end of file. previous commit, if any, is done now.
+    if times is not None:
+        yield Result(commit, times)

benchmark/visualize.py

+#!/usr/bin/env python3
+import argparse, sys, pprint, itertools
+import matplotlib.pyplot as plt
+import parse_log
+
+# read command-line arguments
+parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
+parser.add_argument("-f", "--file",
+                    dest="file", required=True,
+                    help="Filename to get the data from.")
+parser.add_argument("-t", "--timings", nargs='+',
+                    dest="timings",
+                    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")
+
+timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
+results = list(parse_log.parse(log_file, timings))
+
+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(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
+
+plt.xlabel('Commit')
+plt.ylabel('Time (s)')
+plt.title('Time to compile files')
+plt.grid(True)
+plt.show()