From 66bb3579c9a3532e5d2829a71e56fc8f240dce5a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 24 Feb 2016 10:29:27 +0100
Subject: [PATCH] start work on a build-times visualizer
---
benchmark/.gitignore | 2 ++
benchmark/gitlab-extract.py | 3 ++-
benchmark/parse_log.py | 38 +++++++++++++++++++++++++++++++++++++
benchmark/visualize.py | 20 +++++++++++++++++++
4 files changed, 62 insertions(+), 1 deletion(-)
create mode 100644 benchmark/.gitignore
create mode 100644 benchmark/parse_log.py
create mode 100755 benchmark/visualize.py
diff --git a/benchmark/.gitignore b/benchmark/.gitignore
new file mode 100644
index 000000000..9c7d8939c
--- /dev/null
+++ b/benchmark/.gitignore
@@ -0,0 +1,2 @@
+__pycache__
+build-times.log
diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index a819f19c9..6a8f28c2b 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -1,6 +1,7 @@
#!/usr/bin/env python3
import argparse, pprint, subprocess, sys
import requests
+import parse_log
def first(it):
for i in it:
@@ -12,7 +13,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.")
diff --git a/benchmark/parse_log.py b/benchmark/parse_log.py
new file mode 100644
index 000000000..e79db09eb
--- /dev/null
+++ b/benchmark/parse_log.py
@@ -0,0 +1,38 @@
+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)
diff --git a/benchmark/visualize.py b/benchmark/visualize.py
new file mode 100755
index 000000000..0b778a678
--- /dev/null
+++ b/benchmark/visualize.py
@@ -0,0 +1,20 @@
+#!/usr/bin/env python3
+import argparse, sys, pprint
+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 (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")
+
+for result in parse_log.parse(log_file, args.timings):
+ pp.pprint(result.commit)
+ pp.pprint(result.times)
+ print()
--
GitLab