| author | Lars Hupel <lars.hupel@mytum.de> |
| Sat, 24 Sep 2016 15:33:55 +0200 | |
| changeset 63942 | 9195600fcc7c |
| child 63943 | fbc2b562331b |
| permissions | -rw-r--r-- |
|
63942
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
1 |
object stats extends isabelle.Isabelle_Tool.Body {
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
import isabelle._ |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
val target_dir = Path.explode("stats")
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
<html> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
10 |
<head><title>Performance statistics from session build output</title></head> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
<body> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
12 |
""" |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
13 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
14 |
val html_footer = """ |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
15 |
</body> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
16 |
</html> |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
17 |
""" |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
18 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
19 |
def generate(job: String): Unit = {
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
20 |
println(s"=== $job ===") |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
21 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
22 |
val dir = target_dir + Path.basic(job) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
23 |
val sessions = Build_Stats.present_job(job, dir) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
24 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
25 |
val sections = |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
cat_lines( |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
27 |
sessions.map(session => |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
"<p id=" + quote("session_" + HTML.output(session)) + ">" +
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
"<h2>" + HTML.output(session) + "</h2>" + |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
30 |
"<img src=" + quote(HTML.output(session + ".png")) + "></p>\n")) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
31 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
val toc = |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
cat_lines( |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
34 |
sessions.map(session => |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
35 |
"<li><a href=" + quote("#session_" + HTML.output(session)) + ">" +
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
HTML.output(session) + "</a></li>\n")) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
38 |
val html = |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
39 |
html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" + "<div><ul>" + toc + "</ul></div>\n" + |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
40 |
sections + html_footer |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
41 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
42 |
File.write(dir + Path.basic("index.html"), html)
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
43 |
} |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
44 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
45 |
override final def apply(args: List[String]): Unit = {
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
46 |
jobs.foreach(generate) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
47 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
48 |
File.write(target_dir + Path.basic("index.html"),
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
49 |
html_header + "\n<ul>\n" + |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
50 |
cat_lines( |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
51 |
jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" + |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
52 |
HTML.output(job) + """</a> </li>""")) + |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
53 |
"\n</ul>\n" + html_footer) |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
54 |
} |
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
55 |
|
|
9195600fcc7c
CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
56 |
} |