Skip to content
Snippets Groups Projects
Commit b71ae795 authored by Ralf Jung's avatar Ralf Jung
Browse files

update coq-speed export script

parent db735a45
No related branches found
No related tags found
No related merge requests found
__pycache__ __pycache__
build-times.log* build-times*
gitlab-extract gitlab-extract
...@@ -3,8 +3,6 @@ import argparse, sys, pprint, itertools, subprocess ...@@ -3,8 +3,6 @@ import argparse, sys, pprint, itertools, subprocess
import requests import requests
import parse_log import parse_log
markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
# read command-line arguments # read command-line arguments
parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana') parser = argparse.ArgumentParser(description='Export iris-coq build times to grafana')
parser.add_argument("-f", "--file", parser.add_argument("-f", "--file",
...@@ -19,6 +17,9 @@ parser.add_argument("-p", "--project", ...@@ -19,6 +17,9 @@ parser.add_argument("-p", "--project",
parser.add_argument("-b", "--branch", parser.add_argument("-b", "--branch",
dest="branch", required=True, dest="branch", required=True,
help="Branch name sent to the server.") help="Branch name sent to the server.")
parser.add_argument("--config",
dest="config", required=True,
help="The config string.")
parser.add_argument("-s", "--server", parser.add_argument("-s", "--server",
dest="server", required=True, dest="server", required=True,
help="The server (URL) to send the data to.") help="The server (URL) to send the data to.")
...@@ -41,8 +42,10 @@ results = list(results) ...@@ -41,8 +42,10 @@ results = list(results)
for datapoint in results: for datapoint in results:
times = ''.join(datapoint.times) times = ''.join(datapoint.times)
commit = datapoint.commit commit = datapoint.commit
print("Sending {}...".format(commit), end='')
date = subprocess.check_output(['git', 'show', commit, '-s', '--pretty=%cI']).strip().decode('UTF-8') 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} headers = {'X-Project': args.project, 'X-Branch': args.branch, 'X-Commit': commit, 'X-Config': args.config, 'X-Date': date}
r = requests.post(args.server, data=times, headers=headers, auth=(args.user, args.password)) r = requests.post(args.server+"/build_times_8.6", data=times, headers=headers, auth=(args.user, args.password))
r.raise_for_status() r.raise_for_status()
print(" done")
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment