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