diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e776dd5550e0821777b32500c2685dcdeb379e1c..b17393743747e1e3821974c261c0b6448c34fc7f 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index 45c5a039fa234db6860c6143c1a10311af20ca7c..63a3a176ab5760028a80ea84933dabb59b26e6b0 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -1,5 +1,5 @@
#!/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:
diff --git a/benchmark/parse_log.py b/benchmark/parse_log.py
index e79db09eb93f4da4861c223e6f2bb912c5555414..82da2030ae242802c509b5cbc98150a92756b7fa 100644
--- a/benchmark/parse_log.py
+++ b/benchmark/parse_log.py
@@ -1,13 +1,13 @@
-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'))
diff --git a/benchmark/visualize.py b/benchmark/visualize.py
index d796cdf3e0629ba5bfcd61721d4973f6f6329e5d..3456b4b4b9467ce30fc0e8e84efd25940d5900e2 100755
--- a/benchmark/visualize.py
+++ b/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