# HG changeset patch # User Lars Hupel # Date 1529939939 -7200 # Node ID 71483c0e0023089728572c8a3a99d956b253c884 # Parent ebdd5508f3865bd11a0644c8ef4a2355af5f4c33 obsolete diff -r ebdd5508f386 -r 71483c0e0023 Admin/jenkins/build/ci_build_stats.scala --- a/Admin/jenkins/build/ci_build_stats.scala Mon Jun 25 14:06:50 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -// FIXME obsolete - -object stats extends isabelle.Isabelle_Tool.Body { - - import isabelle._ - import java.time._ - import java.time.format.DateTimeFormatter - - - val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) - - val target_dir = Path.explode("stats") - val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") - - val html_header = s""" - -Performance statistics from session build output - -

Generated at $start_time

-""" - - val html_footer = """ - - -""" - - def generate(job: String): Unit = { - println(s"=== $job ===") - - val dir = target_dir + Path.basic(job) - val sessions: List[String] = Nil - - 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) - } - -}