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

.gitlab-ci.yml

@@ -6,6 +6,8 @@ buildjob:
   script:
   - 'make -j8 TIMED=y 2>&1 | tee build-log.txt'
   - 'cat build-log.txt  | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" > build-time.txt'
+  only:
+  - master
   artifacts:
     paths:
     - build-time.txt

benchmark/gitlab-extract.py

 #!/usr/bin/env python3
-import argparse, pprint, subprocess, sys
+import argparse, pprint, sys
 import requests
 import parse_log
 
@@ -42,19 +42,13 @@ log_file = sys.stdout if args.file == "-" else open(args.file, "a")
 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"), []))
+    last_result = last(parse_log.parse(open(args.file, "r"), parse_times = False))
     args.commits = "{}..origin/master".format(last_result.commit)
 
 projects = req("projects")
 project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
 
-if args.commits.find('..') >= 0:
-    # a range of commits
-    commits = subprocess.check_output(["git", "rev-list", args.commits]).decode("utf-8")
-else:
-    # a single commit
-    commits = subprocess.check_output(["git", "rev-parse", args.commits]).decode("utf-8")
-for commit in reversed(commits.strip().split('\n')):
+for commit in parse_log.parse_git_commits(args.commits):
     print("Fetching {}...".format(commit))
     builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
     if builds.status_code != 200:

benchmark/parse_log.py

-import re
+import re, subprocess
 
 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.'''
+def parse(file, parse_times = True):
+    '''[file] should be a file-like object, an iterator over the lines.
+       yields a list of Result objects.'''
     commit_re = re.compile("^# ([a-z0-9]+)$")
     time_re = re.compile("^([a-zA-Z0-9_/-]+) \(user: ([0-9.]+) mem: ([0-9]+) ko\)$")
     commit = None
@@ -17,18 +17,19 @@ def parse(file, filter):
         m = commit_re.match(line)
         if m is not None:
             # previous commit, if any, is done now
-            if times is not None:
+            if commit is not None:
                 yield Result(commit, times)
             # start recording next commit
             commit = m.group(1)
-            times = {} # reset the recorded times
+            if parse_times:
+                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:
+            if times is not None:
+                name = m.group(1)
+                time = float(m.group(2))
                 times[name] = time
             continue
         # nothing else we know about
@@ -36,3 +37,13 @@ def parse(file, filter):
     # end of file. previous commit, if any, is done now.
     if times is not None:
         yield Result(commit, times)
+
+def parse_git_commits(commits):
+    '''Returns an iterable of SHA1s'''
+    if commits.find('..') >= 0:
+        # a range of commits
+        commits = subprocess.check_output(["git", "rev-list", commits])
+    else:
+        # a single commit
+        commits = subprocess.check_output(["git", "rev-parse", commits])
+    return reversed(commits.decode("utf-8").strip().split('\n'))

benchmark/visualize.py

@@ -3,6 +3,8 @@ import argparse, sys, pprint, itertools
 import matplotlib.pyplot as plt
 import parse_log
 
+markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
+
 # read command-line arguments
 parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
 parser.add_argument("-f", "--file",
@@ -11,18 +13,23 @@ parser.add_argument("-f", "--file",
 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")
+parser.add_argument("-c", "--commits",
+                    dest="commits",
+                    help="Restrict the graph to the given commits.")
 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))
+results = parse_log.parse(log_file, parse_times = True)
+if args.commits:
+    commits = set(parse_log.parse_git_commits(args.commits))
+    results = filter(lambda r: r.commit in commits, results)
+results = list(results)
 
-markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
+timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
 for timing in timings:
     plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-
-plt.legend(timings, loc='lower left')
+plt.legend(timings, loc='upper left')
 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