equal
deleted
inserted
replaced
1 object stats extends isabelle.Isabelle_Tool.Body { |
1 object stats extends isabelle.Isabelle_Tool.Body { |
2 |
2 |
3 import isabelle._ |
3 import isabelle._ |
|
4 import java.time._ |
|
5 import java.time.format.DateTimeFormatter |
|
6 |
|
7 |
|
8 val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) |
4 |
9 |
5 val target_dir = Path.explode("stats") |
10 val target_dir = Path.explode("stats") |
6 val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") |
11 val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") |
7 |
12 |
8 val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> |
13 val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN"> |
9 <html> |
14 <html> |
10 <head><title>Performance statistics from session build output</title></head> |
15 <head><title>Performance statistics from session build output</title></head> |
11 <body> |
16 <body> |
|
17 <p>Generated at $start_time</p> |
12 """ |
18 """ |
13 |
19 |
14 val html_footer = """ |
20 val html_footer = """ |
15 </body> |
21 </body> |
16 </html> |
22 </html> |