From 49142779c5d4fa85111a573409870e8c5ea9223e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Jan 2017 21:36:02 +0100
Subject: [PATCH] update gitlab-extract to handle the double-CI-build (Coq 8.5
and 8.6)
---
benchmark/gitlab-extract.py | 39 ++++++++++++++++++++++---------------
1 file changed, 23 insertions(+), 16 deletions(-)
diff --git a/benchmark/gitlab-extract.py b/benchmark/gitlab-extract.py
index 5e9db68f8..563a06aad 100755
--- a/benchmark/gitlab-extract.py
+++ b/benchmark/gitlab-extract.py
@@ -51,27 +51,34 @@ if project is None:
sys.stderr.write("Project not found.\n")
sys.exit(1)
+BREAK = False
for commit in parse_log.parse_git_commits(args.commits):
+ if BREAK:
+ break
print("Fetching {}...".format(commit))
commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
if commit_data.status_code != 200:
raise Exception("Commit not found?")
builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
if builds.status_code != 200:
- # no build
- continue
- build = first(sorted(builds.json(), key = lambda b: -int(b['id'])))
- if build is None or build['status'] == 'failed':
- # build failed (or missing...??)
- continue
- if build['status'] == 'running':
- # build still running, don't fetch this or any later commit
+ raise Exception("Build not found?")
+ # iterate over builds by decreasing ID, and look for the artifact
+ for build in builds.json():
+ if build['status'] in ('created', 'pending', 'running'):
+ # build still not yet done, don't fetch this or any later commit
+ BREAK = True
+ break
+ if build['status'] != 'success':
+ # build failed or cancelled, skip to next
+ continue
+ # now fetch the build times
+ build_times = requests.get("{}/builds/{}/artifacts/file/build-time.txt".format(project['web_url'], build['id']))
+ if build_times.status_code != 200:
+ # no artifact at this build, try another one
+ continue
+ # Output in the log file format
+ log_file.write("# {}\n".format(commit))
+ log_file.write(build_times.text)
+ log_file.flush()
+ # don't fetch another one
break
- # now fetch the build times
- build_times = requests.get("{}/builds/{}/artifacts/file/build-time.txt".format(project['web_url'], build['id']))
- if build_times.status_code != 200:
- raise Exception("No artifact at build?")
- # Output in the log file format
- log_file.write("# {}\n".format(commit))
- log_file.write(build_times.text)
- log_file.flush()
--
GitLab