# HG changeset patch # User Lars Hupel # Date 1474724035 -7200 # Node ID 9195600fcc7ceb0784e82cb9411680b16aabdef6 # Parent f353674c2528a121ccbcc6f6ecd2404375bf71d2 CI script to generate timing statistics diff -r f353674c2528 -r 9195600fcc7c Admin/jenkins/build/ci_build_stats.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/jenkins/build/ci_build_stats.scala Sat Sep 24 15:33:55 2016 +0200 @@ -0,0 +1,56 @@ +object stats extends isabelle.Isabelle_Tool.Body { + + import isabelle._ + + val target_dir = Path.explode("stats") + val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") + + val html_header = """ + +Performance statistics from session build output + +""" + + val html_footer = """ + + +""" + + def generate(job: String): Unit = { + println(s"=== $job ===") + + val dir = target_dir + Path.basic(job) + val sessions = Build_Stats.present_job(job, dir) + + val sections = + cat_lines( + sessions.map(session => + "

" + + "

" + HTML.output(session) + "

" + + "

\n")) + + val toc = + cat_lines( + sessions.map(session => + "

" + + HTML.output(session) + "

\n")) + + val html = + html_header + "\n

" + HTML.output(job) + "

\n" + "

" + toc + "

\n" + + sections + html_footer + + File.write(dir + Path.basic("index.html"), html) + } + + override final def apply(args: List[String]): Unit = { + jobs.foreach(generate) + + File.write(target_dir + Path.basic("index.html"), + html_header + "\n

""" + + HTML.output(job) + """

\n" + html_footer) + } + +}