From b71ae795ccd0cb6fa7d9ead9ed693a228b4563b1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 4 Mar 2018 20:55:58 +0100
Subject: [PATCH] update coq-speed export script
---
benchmark/.gitignore | 2 +-
benchmark/export.py | 11 +++++++----
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/benchmark/.gitignore b/benchmark/.gitignore
index 43824c2fe..b0922ce45 100644
--- a/benchmark/.gitignore
+++ b/benchmark/.gitignore
@@ -1,3 +1,3 @@
__pycache__
-build-times.log*
+build-times*
gitlab-extract
diff --git a/benchmark/export.py b/benchmark/export.py
index 9707edff2..308cca16a 100755
--- a/benchmark/export.py
+++ b/benchmark/export.py
@@ -3,8 +3,6 @@ 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",
@@ -19,6 +17,9 @@ parser.add_argument("-p", "--project",
parser.add_argument("-b", "--branch",
dest="branch", required=True,
help="Branch name sent to the server.")
+parser.add_argument("--config",
+ dest="config", required=True,
+ help="The config string.")
parser.add_argument("-s", "--server",
dest="server", required=True,
help="The server (URL) to send the data to.")
@@ -41,8 +42,10 @@ results = list(results)
for datapoint in results:
times = ''.join(datapoint.times)
commit = datapoint.commit
+ print("Sending {}...".format(commit), end='')
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))
+ headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
+ r = requests.post(args.server+"/build_times_8.6", data=times, headers=headers, auth=(args.user, args.password))
r.raise_for_status()
+ print(" done")
--
GitLab