isabelle: Admin/jenkins/build/ci_build_stats.scala@4311845b0412 (annotated)

65790 91940684a267 obsolete; wenzelm parents: 65734 diff changeset	1	// FIXME obsolete
91940684a267 obsolete; wenzelm parents: 65734 diff changeset	2
63942 9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	3	object stats extends isabelle.Isabelle_Tool.Body {
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	import isabelle._
63943 fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	6	import java.time._
fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	7	import java.time.format.DateTimeFormatter
fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	8
fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	9
fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	10	val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
63942 9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	11
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	12	val target_dir = Path.explode("stats")
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	13	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	14
63943 fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	15	val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
63942 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	<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	18	<body>
63943 fbc2b562331b include generation time in statistics Lars Hupel <lars.hupel@mytum.de> parents: 63942 diff changeset	19	<p>Generated at $start_time</p>
63942 9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	20	"""
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 html_footer = """
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	23	</body>
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	24	</html>
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	25	"""
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	26
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	27	def generate(job: String): Unit = {
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	28	println(s"=== $job ===")
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	29
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	30	val dir = target_dir + Path.basic(job)
65790 91940684a267 obsolete; wenzelm parents: 65734 diff changeset	31	val sessions: List[String] = Nil
63942 9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	32
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	33	val sections =
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	34	cat_lines(
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	35	sessions.map(session =>
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	36	"<p id=" + quote("session_" + HTML.output(session)) + ">" +
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	37	"<h2>" + HTML.output(session) + "</h2>" +
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	38	"<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	39
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	40	val toc =
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	41	cat_lines(
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	42	sessions.map(session =>
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	43	"<li><a href=" + quote("#session_" + HTML.output(session)) + ">" +
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	44	HTML.output(session) + "</a></li>\n"))
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	45
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	46	val html =
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	47	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	48	sections + html_footer
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	49
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	50	File.write(dir + Path.basic("index.html"), html)
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	51	}
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	52
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	53	override final def apply(args: List[String]): Unit = {
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	54	jobs.foreach(generate)
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	File.write(target_dir + Path.basic("index.html"),
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	57	html_header + "\n<ul>\n" +
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	58	cat_lines(
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	59	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	60	HTML.output(job) + """</a> </li>""")) +
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	61	"\n</ul>\n" + html_footer)
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	62	}
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	63
9195600fcc7c CI script to generate timing statistics Lars Hupel <lars.hupel@mytum.de> parents: diff changeset	64	}

author	wenzelm
	Tue, 16 Jan 2018 09:58:17 +0100
changeset 67445	4311845b0412
parent 65790	91940684a267
permissions	-rw-r--r--