diff --git a/benchmark/export.py b/benchmark/export.py new file mode 100755 index 0000000000000000000000000000000000000000..9707edff28968fad8a42c3554645cfb09325f39b --- /dev/null +++ b/benchmark/export.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python3 +import argparse, sys, pprint, itertools, subprocess +import requests +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='Export iris-coq build times to grafana') +parser.add_argument("-f", "--file", + dest="file", required=True, + help="Filename to get the data from.") +parser.add_argument("-c", "--commits", + dest="commits", + help="Restrict the graph to the given commits.") +parser.add_argument("-p", "--project", + dest="project", required=True, + help="Project name sent to the server.") +parser.add_argument("-b", "--branch", + dest="branch", required=True, + help="Branch name sent to the server.") +parser.add_argument("-s", "--server", + dest="server", required=True, + help="The server (URL) to send the data to.") +parser.add_argument("-u", "--user", + dest="user", required=True, + help="Username for HTTP auth.") +parser.add_argument("--password", + dest="password", required=True, + help="Password for HTTP auth.") +args = parser.parse_args() +pp = pprint.PrettyPrinter() +log_file = sys.stdin if args.file == "-" else open(args.file, "r") + +results = parse_log.parse(log_file, parse_times = parse_log.PARSE_RAW) +if args.commits: + commits = set(parse_log.parse_git_commits(args.commits)) + results = filter(lambda r: r.commit in commits, results) +results = list(results) + +for datapoint in results: + times = ''.join(datapoint.times) + commit = datapoint.commit + date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8') + headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Date': date} + r = requests.post(args.server, data=times, headers=headers, auth=(args.user, args.password)) + r.raise_for_status() + diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py index 07f4727c22e343e6256a5325011c9aec5571d866..0c83d51df40987b37fee68b2191b6c1a62baa413 100755 --- a/benchmark/gitlab-extract.py +++ b/benchmark/gitlab-extract.py @@ -16,7 +16,9 @@ def first(it): def req(path): url = '%s/api/v3/%s' % (args.server, path) - return requests.get(url, headers={'PRIVATE-TOKEN': args.private_token}) + r = requests.get(url, headers={'PRIVATE-TOKEN': args.private_token}) + r.raise_for_status() + return r # read command-line arguments parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab') @@ -45,7 +47,7 @@ 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"), parse_times = False)) + last_result = last(parse_log.parse(open(args.file, "r"), parse_times = parse_log.PARSE_NOT)) args.commits = "{}..origin/master".format(last_result.commit) projects = req("projects?per_page=512") diff --git a/benchmark/parse_log.py b/benchmark/parse_log.py index 1649fe42e83cdc8a862796f5e4c5dbaa681bb8d5..568f83d9c3134142df9e26a59f7b8bc93043dd52 100644 --- a/benchmark/parse_log.py +++ b/benchmark/parse_log.py @@ -5,7 +5,11 @@ class Result: self.commit = commit self.times = times -def parse(file, parse_times = True): +PARSE_NOT = 0 +PARSE_RAW = 1 +PARSE_FULL = 2 + +def parse(file, parse_times = PARSE_FULL): '''[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]+)$") @@ -21,16 +25,19 @@ def parse(file, parse_times = True): yield Result(commit, times) # start recording next commit commit = m.group(1) - if parse_times: - times = {} # reset the recorded times + if parse_times != PARSE_NOT: + times = [] if parse_times == PARSE_RAW else {} # reset the recorded times continue # next file time? m = time_re.match(line) if m is not None: if times is not None: - name = m.group(1) - time = float(m.group(2)) - times[name] = time + if parse_times == PARSE_RAW: + times.append(line) + else: + name = m.group(1) + time = float(m.group(2)) + times[name] = time continue # nothing else we know about, ignore # end of file. previous commit, if any, is done now. diff --git a/benchmark/visualize.py b/benchmark/visualize.py index fcb59991afad2f5edae41d6b9405fda2cad0df72..06eba983d5396bb02b8f783f350b22f6bb80f237 100755 --- a/benchmark/visualize.py +++ b/benchmark/visualize.py @@ -20,7 +20,7 @@ args = parser.parse_args() pp = pprint.PrettyPrinter() log_file = sys.stdin if args.file == "-" else open(args.file, "r") -results = parse_log.parse(log_file, parse_times = True) +results = parse_log.parse(log_file, parse_times = parse_log.PARSE_FULL) if args.commits: commits = set(parse_log.parse_git_commits(args.commits)) results = filter(lambda r: r.commit in commits, results)