Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
66bb3579
Commit
66bb3579
authored
Feb 24, 2016
by
Ralf Jung
Browse files
start work on a build-times visualizer
parent
bc2298c3
Changes
4
Hide whitespace changes
Inline
Side-by-side
benchmark/.gitignore
0 → 100644
View file @
66bb3579
__pycache__
build-times.log
benchmark/gitlab-extract.py
View file @
66bb3579
#!/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."
)
...
...
benchmark/parse_log.py
0 → 100644
View file @
66bb3579
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
)
benchmark/visualize.py
0 → 100755
View file @
66bb3579
#!/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
()
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment