--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_history.scala Wed Oct 12 09:38:20 2016 +0200
@@ -0,0 +1,388 @@
+/* Title: Pure/Admin/build_history.scala
+ Author: Makarius
+
+Build other history versions.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.time.format.DateTimeFormatter
+import java.util.Locale
+
+
+object Build_History
+{
+ /* log files */
+
+ val BUILD_HISTORY = "build_history"
+ val META_INFO_MARKER = "\fmeta_info = "
+
+
+
+ /** other Isabelle environment **/
+
+ private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
+ {
+ other_isabelle =>
+
+
+ /* static system */
+
+ def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+ Isabelle_System.bash(
+ "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
+ env = null, cwd = isabelle_home.file, redirect = redirect,
+ progress_stdout = progress.echo_if(echo, _),
+ progress_stderr = progress.echo_if(echo, _))
+
+ def copy_dir(dir1: Path, dir2: Path): Unit =
+ bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
+
+ def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
+ bash("bin/isabelle " + cmdline, redirect, echo)
+
+ def resolve_components(echo: Boolean): Unit =
+ other_isabelle("components -a", redirect = true, echo = echo).check
+
+ val isabelle_home_user: Path =
+ Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
+
+ val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
+ val log_dir: Path = isabelle_home_user + Path.explode("log")
+
+
+ /* reset settings */
+
+ def reset_settings(components_base: String, nonfree: Boolean)
+ {
+ if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
+ error("Cannot proceed with existing user settings file: " + etc_settings)
+
+ Isabelle_System.mkdirs(etc_settings.dir)
+ File.write(etc_settings,
+ "# generated by Isabelle " + Date.now() + "\n" +
+ "#-*- shell-script -*- :mode=shellscript:\n")
+
+ val component_settings =
+ {
+ val components_base_path =
+ if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
+ else Path.explode(components_base).expand
+
+ val catalogs =
+ if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
+
+ catalogs.map(catalog =>
+ "init_components " + File.bash_path(components_base_path) +
+ " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
+ }
+ File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
+ }
+
+
+ /* augment settings */
+
+ def augment_settings(
+ threads: Int,
+ arch_64: Boolean = false,
+ heap: Int = default_heap,
+ max_heap: Option[Int] = None,
+ more_settings: List[String]): String =
+ {
+ val (ml_platform, ml_settings) =
+ {
+ val windows_32 = "x86-windows"
+ val windows_64 = "x86_64-windows"
+ val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
+ val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
+ val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
+
+ val polyml_home =
+ try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
+ catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
+
+ def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
+
+ def err(platform: String): Nothing =
+ error("Platform " + platform + " unavailable on this machine")
+
+ def check_dir(platform: String): Boolean =
+ platform != "" && ml_home(platform).is_dir
+
+ val ml_platform =
+ if (Platform.is_windows && arch_64) {
+ if (check_dir(windows_64)) windows_64 else err(windows_64)
+ }
+ else if (Platform.is_windows && !arch_64) {
+ if (check_dir(windows_32)) windows_32
+ else platform_32 // x86-cygwin
+ }
+ else {
+ val (platform, platform_name) =
+ if (arch_64) (platform_64, "x86_64-" + platform_family)
+ else (platform_32, "x86-" + platform_family)
+ if (check_dir(platform)) platform else err(platform_name)
+ }
+
+ val ml_options =
+ "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
+ " --gcthreads " + threads +
+ (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
+
+ (ml_platform,
+ List(
+ "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
+ "ML_PLATFORM=" + quote(ml_platform),
+ "ML_OPTIONS=" + quote(ml_options)))
+ }
+
+ val thread_settings =
+ List(
+ "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
+ "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
+
+ val settings =
+ List(ml_settings, thread_settings) :::
+ (if (more_settings.isEmpty) Nil else List(more_settings))
+
+ File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
+
+ ml_platform
+ }
+ }
+
+
+
+ /** build_history **/
+
+ private val default_rev = "tip"
+ private val default_threads = 1
+ private val default_heap = 1000
+ private val default_isabelle_identifier = "build_history"
+
+ def build_history(
+ progress: Progress,
+ hg: Mercurial.Repository,
+ rev: String = default_rev,
+ isabelle_identifier: String = default_isabelle_identifier,
+ components_base: String = "",
+ fresh: Boolean = false,
+ nonfree: Boolean = false,
+ multicore_base: Boolean = false,
+ threads_list: List[Int] = List(default_threads),
+ arch_64: Boolean = false,
+ heap: Int = default_heap,
+ max_heap: Option[Int] = None,
+ more_settings: List[String] = Nil,
+ verbose: Boolean = false,
+ build_args: List[String] = Nil): List[Process_Result] =
+ {
+ /* sanity checks */
+
+ if (File.eq(Path.explode("~~").file, hg.root.file))
+ error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
+
+ for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
+
+ if (heap < 100) error("Bad heap value < 100: " + heap)
+
+ if (max_heap.isDefined && max_heap.get < heap)
+ error("Bad max_heap value < heap: " + max_heap.get)
+
+ System.getenv("ISABELLE_SETTINGS_PRESENT") match {
+ case null | "" =>
+ case _ => error("Cannot run build_history within existing Isabelle settings environment")
+ }
+
+
+ /* init repository */
+
+ hg.update(rev = rev, clean = true)
+ progress.echo_if(verbose, hg.log(rev, options = "-l1"))
+
+ val isabelle_version = hg.identify(rev, options = "-i")
+ val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
+
+
+ /* main */
+
+ val build_history_date = Date.now()
+ val build_host = Isabelle_System.hostname()
+
+ var first_build = true
+ for (threads <- threads_list) yield
+ {
+ /* init settings */
+
+ other_isabelle.reset_settings(components_base, nonfree)
+ other_isabelle.resolve_components(verbose)
+ val ml_platform =
+ other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
+
+ val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
+ val isabelle_output_log = isabelle_output + Path.explode("log")
+ val isabelle_base_log = isabelle_output + Path.explode("../base_log")
+
+ if (first_build) {
+ other_isabelle.resolve_components(verbose)
+ other_isabelle.bash(
+ "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
+ "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
+ redirect = true, echo = verbose).check
+
+ Isabelle_System.rm_tree(isabelle_base_log.file)
+ }
+
+ Isabelle_System.rm_tree(isabelle_output.file)
+ Isabelle_System.mkdirs(isabelle_output)
+
+
+ /* build */
+
+ if (multicore_base && !first_build && isabelle_base_log.is_dir)
+ other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
+
+ val build_start = Date.now()
+ val res =
+ other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
+ val build_end = Date.now()
+
+
+ /* output log */
+
+ val log_path =
+ other_isabelle.log_dir +
+ Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
+
+ val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
+
+ val meta_info =
+ List(Build_Log.Field.build_engine -> BUILD_HISTORY,
+ Build_Log.Field.build_host -> build_host,
+ Build_Log.Field.build_start -> Build_Log.print_date(build_start),
+ Build_Log.Field.build_end -> Build_Log.print_date(build_end),
+ Build_Log.Field.isabelle_version -> isabelle_version)
+
+ val ml_statistics =
+ build_info.finished_sessions.flatMap(session_name =>
+ {
+ val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
+ if (session_log.is_file) {
+ Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
+ ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
+ }
+ else Nil
+ })
+
+ val heap_sizes =
+ build_info.finished_sessions.flatMap(session_name =>
+ {
+ val heap = isabelle_output + Path.explode(session_name)
+ if (heap.is_file)
+ Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
+ else None
+ })
+
+ Isabelle_System.mkdirs(log_path.dir)
+ File.write_gzip(log_path,
+ Library.terminate_lines(
+ Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
+ ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
+ heap_sizes))
+
+ Output.writeln(log_path.implode, stdout = true)
+
+
+ /* next build */
+
+ if (multicore_base && first_build && isabelle_output_log.is_dir)
+ other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
+
+ first_build = false
+
+ res
+ }
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ var multicore_base = false
+ var components_base = ""
+ var heap: Option[Int] = None
+ var max_heap: Option[Int] = None
+ var threads_list = List(default_threads)
+ var isabelle_identifier = default_isabelle_identifier
+ var more_settings: List[String] = Nil
+ var fresh = false
+ var arch_64 = false
+ var nonfree = false
+ var rev = default_rev
+ var verbose = false
+
+ val getopts = Getopts("""
+Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
+
+ Options are:
+ -B first multicore build serves as base for scheduling information
+ -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
+ -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
+ -M THREADS multicore configurations (comma-separated list, default: """ + default_threads + """)
+ -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
+ -U SIZE maximal ML heap in MB (default: unbounded)
+ -e TEXT additional text for generated etc/settings
+ -f fresh build of Isabelle/Scala components (recommended)
+ -m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
+ -n include nonfree components
+ -r REV update to revision (default: """ + default_rev + """)
+ -v verbose
+
+ Build Isabelle sessions from the history of another REPOSITORY clone,
+ passing ARGS directly to its isabelle build tool.
+""",
+ "B" -> (_ => multicore_base = true),
+ "C:" -> (arg => components_base = arg),
+ "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
+ "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
+ "N:" -> (arg => isabelle_identifier = arg),
+ "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
+ "e:" -> (arg => more_settings = more_settings ::: List(arg)),
+ "f" -> (_ => fresh = true),
+ "m:" ->
+ {
+ case "32" | "x86" => arch_64 = false
+ case "64" | "x86_64" => arch_64 = true
+ case bad => error("Bad processor architecture: " + quote(bad))
+ },
+ "n" -> (_ => nonfree = true),
+ "r:" -> (arg => rev = arg),
+ "v" -> (_ => verbose = true))
+
+ val more_args = getopts(args)
+ val (root, build_args) =
+ more_args match {
+ case root :: build_args => (root, build_args)
+ case _ => getopts.usage()
+ }
+
+ using(Mercurial.open_repository(Path.explode(root)))(hg =>
+ {
+ val progress = new Console_Progress(stderr = true)
+ val results =
+ build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
+ components_base = components_base, fresh = fresh, nonfree = nonfree,
+ multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
+ heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
+ max_heap = max_heap, more_settings = more_settings, verbose = verbose,
+ build_args = build_args)
+ val rc = (0 /: results) { case (rc, res) => rc max res.rc }
+ if (rc != 0) sys.exit(rc)
+ })
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_log.scala Wed Oct 12 09:38:20 2016 +0200
@@ -0,0 +1,548 @@
+/* Title: Pure/Admin/build_log.scala
+ Author: Makarius
+
+Build log parsing for current and historic formats.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.time.ZoneId
+import java.time.format.{DateTimeFormatter, DateTimeParseException}
+import java.util.Locale
+
+import scala.collection.mutable
+import scala.util.matching.Regex
+
+
+object Build_Log
+{
+ /** directory content **/
+
+ /* file names */
+
+ def log_date(date: Date): String =
+ String.format(Locale.ROOT, "%s.%05d",
+ DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
+ new java.lang.Long((date.time - date.midnight.time).ms / 1000))
+
+ def log_path(engine: String, date: Date, more: String*): Path =
+ Path.explode(date.rep.getYear.toString) +
+ Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
+
+
+ /* log file collections */
+
+ def is_log(file: JFile): Boolean =
+ List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
+
+ def isatest_files(dir: Path): List[JFile] =
+ File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
+
+ def afp_test_files(dir: Path): List[JFile] =
+ File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
+
+
+
+ /** settings **/
+
+ object Settings
+ {
+ val build_settings = List("ISABELLE_BUILD_OPTIONS")
+ val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
+ val all_settings = build_settings ::: ml_settings
+
+ type Entry = (String, String)
+ type T = List[Entry]
+
+ object Entry
+ {
+ def unapply(s: String): Option[Entry] =
+ s.indexOf('=') match {
+ case -1 => None
+ case i =>
+ val a = s.substring(0, i)
+ val b = Library.perhaps_unquote(s.substring(i + 1))
+ Some((a, b))
+ }
+ def apply(a: String, b: String): String = a + "=" + quote(b)
+ def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
+ }
+
+ def show(): String =
+ cat_lines(
+ build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
+ }
+
+
+
+ /** log file **/
+
+ def print_date(date: Date): String = Log_File.Date_Format(date)
+
+ object Log_File
+ {
+ def apply(name: String, lines: List[String]): Log_File =
+ new Log_File(name, lines)
+
+ def apply(name: String, text: String): Log_File =
+ Log_File(name, Library.trim_split_lines(text))
+
+ def apply(file: JFile): Log_File =
+ {
+ val name = file.getName
+ val (base_name, text) =
+ Library.try_unsuffix(".gz", name) match {
+ case Some(base_name) => (base_name, File.read_gzip(file))
+ case None =>
+ Library.try_unsuffix(".xz", name) match {
+ case Some(base_name) => (base_name, File.read_xz(file))
+ case None => (name, File.read(file))
+ }
+ }
+ apply(base_name, text)
+ }
+
+ def apply(path: Path): Log_File = apply(path.file)
+
+
+ /* date format */
+
+ val Date_Format =
+ {
+ val fmts =
+ Date.Formatter.variants(
+ List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
+ List(Locale.ENGLISH, Locale.GERMAN)) :::
+ List(
+ DateTimeFormatter.RFC_1123_DATE_TIME,
+ Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
+
+ def tune_timezone(s: String): String =
+ s match {
+ case "CET" | "MET" => "GMT+1"
+ case "CEST" | "MEST" => "GMT+2"
+ case "EST" => "Europe/Berlin"
+ case _ => s
+ }
+ def tune_weekday(s: String): String =
+ s match {
+ case "Die" => "Di"
+ case "Mit" => "Mi"
+ case "Don" => "Do"
+ case "Fre" => "Fr"
+ case "Sam" => "Sa"
+ case "Son" => "So"
+ case _ => s
+ }
+
+ def tune(s: String): String =
+ Word.implode(
+ Word.explode(s) match {
+ case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
+ case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
+ case Nil => Nil
+ }
+ )
+
+ Date.Format.make(fmts, tune)
+ }
+
+
+ /* inlined content */
+
+ def print_props(marker: String, props: Properties.T): String =
+ marker + YXML.string_of_body(XML.Encode.properties(props))
+ }
+
+ class Log_File private(val name: String, val lines: List[String])
+ {
+ log_file =>
+
+ override def toString: String = name
+
+ def text: String = cat_lines(lines)
+
+ def err(msg: String): Nothing =
+ error("Error in log file " + quote(name) + ": " + msg)
+
+
+ /* date format */
+
+ object Strict_Date
+ {
+ def unapply(s: String): Some[Date] =
+ try { Some(Log_File.Date_Format.parse(s)) }
+ catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
+ }
+
+
+ /* inlined content */
+
+ def find[A](f: String => Option[A]): Option[A] =
+ lines.iterator.map(f).find(_.isDefined).map(_.get)
+
+ def find_match(regex: Regex): Option[String] =
+ lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
+ map(res => res.get.head)
+
+
+ /* settings */
+
+ def get_setting(a: String): Option[Settings.Entry] =
+ lines.find(_.startsWith(a + "=")) match {
+ case Some(line) => Settings.Entry.unapply(line)
+ case None => None
+ }
+
+ def get_settings(as: List[String]): Settings.T =
+ for { a <- as; entry <- get_setting(a) } yield entry
+
+
+ /* properties (YXML) */
+
+ val xml_cache = new XML.Cache()
+
+ def parse_props(text: String): Properties.T =
+ xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
+
+ def filter_props(marker: String): List[Properties.T] =
+ for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
+
+ def find_line(marker: String): Option[String] =
+ find(Library.try_unprefix(marker, _))
+
+ def find_props(marker: String): Option[Properties.T] =
+ find_line(marker).map(parse_props(_))
+
+
+ /* parse various formats */
+
+ def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
+
+ def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
+
+ def parse_session_info(
+ default_name: String = "",
+ command_timings: Boolean = false,
+ ml_statistics: Boolean = false,
+ task_statistics: Boolean = false): Session_Info =
+ Build_Log.parse_session_info(
+ log_file, default_name, command_timings, ml_statistics, task_statistics)
+ }
+
+
+
+ /** meta info **/
+
+ object Field
+ {
+ val build_engine = "build_engine"
+ val build_host = "build_host"
+ val build_start = "build_start"
+ val build_end = "build_end"
+ val isabelle_version = "isabelle_version"
+ val afp_version = "afp_version"
+ }
+
+ object Meta_Info
+ {
+ val empty: Meta_Info = Meta_Info(Nil, Nil)
+ }
+
+ sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
+ {
+ def is_empty: Boolean = props.isEmpty && settings.isEmpty
+ }
+
+ object Isatest
+ {
+ val engine = "isatest"
+ val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
+ val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
+ val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
+ val No_AFP_Version = new Regex("""$.""")
+ }
+
+ object AFP_Test
+ {
+ val engine = "afp-test"
+ val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
+ val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
+ val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
+ val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
+ val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
+ val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
+ }
+
+ object Jenkins
+ {
+ val engine = "jenkins"
+ val Start = new Regex("""^Started .*$""")
+ val Start_Date = new Regex("""^Build started at (.+)$""")
+ val No_End = new Regex("""$.""")
+ val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
+ val AFP_Version = new Regex("""^AFP id (\S+)$""")
+ val CONFIGURATION = "=== CONFIGURATION ==="
+ val BUILD = "=== BUILD ==="
+ val FINISHED = "Finished: "
+ }
+
+ private def parse_meta_info(log_file: Log_File): Meta_Info =
+ {
+ def parse(engine: String, host: String, start: Date,
+ End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
+ {
+ val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
+ val build_host = if (host == "") Nil else List(Field.build_host -> host)
+
+ val start_date = List(Field.build_start -> start.toString)
+ val end_date =
+ log_file.lines.last match {
+ case End(log_file.Strict_Date(end_date)) =>
+ List(Field.build_end -> end_date.toString)
+ case _ => Nil
+ }
+
+ val isabelle_version =
+ log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
+ val afp_version =
+ log_file.find_match(AFP_Version).map(Field.afp_version -> _)
+
+ Meta_Info(build_engine ::: build_host :::
+ start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
+ log_file.get_settings(Settings.all_settings))
+ }
+
+ log_file.lines match {
+ case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
+ Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
+ log_file.get_settings(Settings.all_settings))
+
+ case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
+ parse(Isatest.engine, host, start, Isatest.End,
+ Isatest.Isabelle_Version, Isatest.No_AFP_Version)
+
+ case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
+ parse(AFP_Test.engine, host, start, AFP_Test.End,
+ AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
+
+ case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
+ parse(AFP_Test.engine, "", start, AFP_Test.End,
+ AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
+
+ case Jenkins.Start() :: _
+ if log_file.lines.contains(Jenkins.CONFIGURATION) ||
+ log_file.lines.last.startsWith(Jenkins.FINISHED) =>
+ log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
+ case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
+ parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
+ Jenkins.Isabelle_Version, Jenkins.AFP_Version)
+ case _ => Meta_Info.empty
+ }
+
+ case line :: _ if line.startsWith("\0") => Meta_Info.empty
+ case List(Isatest.End(_)) => Meta_Info.empty
+ case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
+ case Nil => Meta_Info.empty
+
+ case _ => log_file.err("cannot detect log file format")
+ }
+ }
+
+
+
+ /** build info: produced by isabelle build or build_history **/
+
+ val ML_STATISTICS_MARKER = "\fML_statistics = "
+ val SESSION_NAME = "session_name"
+
+ object Session_Status extends Enumeration
+ {
+ val EXISTING = Value("existing")
+ val FINISHED = Value("finished")
+ val FAILED = Value("failed")
+ val CANCELLED = Value("cancelled")
+ }
+
+ sealed case class Session_Entry(
+ chapter: String,
+ groups: List[String],
+ threads: Option[Int],
+ timing: Timing,
+ ml_timing: Timing,
+ ml_statistics: List[Properties.T],
+ heap_size: Option[Long],
+ status: Session_Status.Value)
+ {
+ def finished: Boolean = status == Session_Status.FINISHED
+ }
+
+ sealed case class Build_Info(sessions: Map[String, Session_Entry])
+ {
+ def session(name: String): Session_Entry = sessions(name)
+ def get_session(name: String): Option[Session_Entry] = sessions.get(name)
+
+ def get_default[A](name: String, f: Session_Entry => A, x: A): A =
+ get_session(name) match {
+ case Some(entry) => f(entry)
+ case None => x
+ }
+
+ def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
+ def finished(name: String): Boolean = get_default(name, _.finished, false)
+ def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
+ def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
+ }
+
+ private def parse_build_info(log_file: Log_File): Build_Info =
+ {
+ object Chapter_Name
+ {
+ def unapply(s: String): Some[(String, String)] =
+ space_explode('/', s) match {
+ case List(chapter, name) => Some((chapter, name))
+ case _ => Some(("", s))
+ }
+ }
+
+ val Session_No_Groups = new Regex("""^Session (\S+)$""")
+ val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
+ val Session_Finished1 =
+ new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
+ val Session_Finished2 =
+ new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
+ val Session_Timing =
+ new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
+ val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
+ val Session_Failed = new Regex("""^(\S+) FAILED""")
+ val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
+ val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
+
+ var chapter = Map.empty[String, String]
+ var groups = Map.empty[String, List[String]]
+ var threads = Map.empty[String, Int]
+ var timing = Map.empty[String, Timing]
+ var ml_timing = Map.empty[String, Timing]
+ var started = Set.empty[String]
+ var failed = Set.empty[String]
+ var cancelled = Set.empty[String]
+ var ml_statistics = Map.empty[String, List[Properties.T]]
+ var heap_sizes = Map.empty[String, Long]
+
+ def all_sessions: Set[String] =
+ chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
+ failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
+
+
+ for (line <- log_file.lines) {
+ line match {
+ case Session_No_Groups(Chapter_Name(chapt, name)) =>
+ chapter += (name -> chapt)
+ groups += (name -> Nil)
+
+ case Session_Groups(Chapter_Name(chapt, name), grps) =>
+ chapter += (name -> chapt)
+ groups += (name -> Word.explode(grps))
+
+ case Session_Started(name) =>
+ started += name
+
+ case Session_Finished1(name,
+ Value.Int(e1), Value.Int(e2), Value.Int(e3),
+ Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
+ val elapsed = Time.hms(e1, e2, e3)
+ val cpu = Time.hms(c1, c2, c3)
+ timing += (name -> Timing(elapsed, cpu, Time.zero))
+
+ case Session_Finished2(name,
+ Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
+ val elapsed = Time.hms(e1, e2, e3)
+ timing += (name -> Timing(elapsed, Time.zero, Time.zero))
+
+ case Session_Timing(name,
+ Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
+ val elapsed = Time.seconds(e)
+ val cpu = Time.seconds(c)
+ val gc = Time.seconds(g)
+ ml_timing += (name -> Timing(elapsed, cpu, gc))
+ threads += (name -> t)
+
+ case Heap(name, Value.Long(size)) =>
+ heap_sizes += (name -> size)
+
+ case _ if line.startsWith(ML_STATISTICS_MARKER) =>
+ val (name, props) =
+ Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
+ case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
+ case _ => log_file.err("malformed ML_statistics " + quote(line))
+ }
+ ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
+
+ case _ =>
+ }
+ }
+
+ val sessions =
+ Map(
+ (for (name <- all_sessions.toList) yield {
+ val status =
+ if (failed(name)) Session_Status.FAILED
+ else if (cancelled(name)) Session_Status.CANCELLED
+ else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
+ Session_Status.FINISHED
+ else if (started(name)) Session_Status.FAILED
+ else Session_Status.EXISTING
+ val entry =
+ Session_Entry(
+ chapter.getOrElse(name, ""),
+ groups.getOrElse(name, Nil),
+ threads.get(name),
+ timing.getOrElse(name, Timing.zero),
+ ml_timing.getOrElse(name, Timing.zero),
+ ml_statistics.getOrElse(name, Nil).reverse,
+ heap_sizes.get(name),
+ status)
+ (name -> entry)
+ }):_*)
+ Build_Info(sessions)
+ }
+
+
+
+ /** session info: produced by "isabelle build" **/
+
+ sealed case class Session_Info(
+ session_name: String,
+ session_timing: Properties.T,
+ command_timings: List[Properties.T],
+ ml_statistics: List[Properties.T],
+ task_statistics: List[Properties.T])
+
+ private def parse_session_info(
+ log_file: Log_File,
+ default_name: String,
+ command_timings: Boolean,
+ ml_statistics: Boolean,
+ task_statistics: Boolean): Session_Info =
+ {
+ val xml_cache = new XML.Cache()
+
+ val session_name =
+ log_file.find_line("\fSession.name = ") match {
+ case None => default_name
+ case Some(name) if default_name == "" || default_name == name => name
+ case Some(name) => log_file.err("log from different session " + quote(name))
+ }
+ val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
+ val command_timings_ =
+ if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
+ val ml_statistics_ =
+ if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
+ val task_statistics_ =
+ if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
+
+ Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/ci_api.scala Wed Oct 12 09:38:20 2016 +0200
@@ -0,0 +1,74 @@
+/* Title: Pure/Admin/ci_api.scala
+ Author: Makarius
+
+API for Isabelle Jenkins continuous integration services.
+*/
+
+package isabelle
+
+
+import java.net.URL
+
+import scala.util.matching.Regex
+
+
+object CI_API
+{
+ /* CI service */
+
+ def root(): String =
+ Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
+
+ def invoke(url: String, args: String*): Any =
+ {
+ val req = url + "/api/json?" + args.mkString("&")
+ val result = Url.read(req)
+ try { JSON.parse(result) }
+ catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
+ }
+
+
+ /* build jobs */
+
+ def build_jobs(): List[String] =
+ for {
+ job <- JSON.array(invoke(root()), "jobs")
+ _class <- JSON.string(job, "_class")
+ if _class == "hudson.model.FreeStyleProject"
+ name <- JSON.string(job, "name")
+ } yield name
+
+ sealed case class Job_Info(
+ job_name: String,
+ timestamp: Long,
+ output: URL,
+ session_logs: List[(String, URL)])
+ {
+ def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
+ def read_session_log(name: String): Build_Log.Log_File =
+ Build_Log.Log_File(name,
+ session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
+ }
+
+ def build_job_builds(job_name: String): List[Job_Info] =
+ {
+ val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
+
+ for {
+ build <- JSON.array(
+ invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
+ number <- JSON.int(build, "number")
+ timestamp <- JSON.long(build, "timestamp")
+ } yield {
+ val job_prefix = root() + "/job/" + job_name + "/" + number
+ val output = Url(job_prefix + "/consoleText")
+ val session_logs =
+ for {
+ artifact <- JSON.array(build, "artifacts")
+ log_path <- JSON.string(artifact, "relativePath")
+ session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
+ } yield (session -> Url(job_prefix + "/artifact/" + log_path))
+ Job_Info(job_name, timestamp, output, session_logs)
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/ci_profile.scala Wed Oct 12 09:38:20 2016 +0200
@@ -0,0 +1,149 @@
+/* Title: Pure/Admin/ci_profile.scala
+ Author: Lars Hupel
+
+Build profile for continuous integration services.
+*/
+
+package isabelle
+
+
+import java.time.{Instant, ZoneId}
+import java.time.format.DateTimeFormatter
+import java.util.{Properties => JProperties}
+
+
+abstract class CI_Profile extends Isabelle_Tool.Body
+{
+ private def build(options: Options): (Build.Results, Time) =
+ {
+ val progress = new Console_Progress(verbose = true)
+ val start_time = Time.now()
+ val results = progress.interrupt_handler {
+ Build.build_selection(
+ options = options,
+ progress = progress,
+ clean_build = true,
+ verbose = true,
+ max_jobs = jobs,
+ dirs = include,
+ select_dirs = select,
+ system_mode = true,
+ selection = select_sessions _)
+ }
+ val end_time = Time.now()
+ (results, end_time - start_time)
+ }
+
+ private def load_properties(): JProperties =
+ {
+ val props = new JProperties()
+ val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
+
+ if (file_name != "")
+ {
+ val file = Path.explode(file_name).file
+ if (file.exists())
+ props.load(new java.io.FileReader(file))
+ props
+ }
+ else
+ props
+ }
+
+ private def compute_timing(results: Build.Results, group: Option[String]): Timing =
+ {
+ val timings = results.sessions.collect {
+ case session if group.forall(results.info(session).groups.contains(_)) =>
+ results(session).timing
+ }
+ (Timing.zero /: timings)(_ + _)
+ }
+
+ private def with_documents(options: Options): Options =
+ {
+ if (documents)
+ options
+ .bool.update("browser_info", true)
+ .string.update("document", "pdf")
+ .string.update("document_variants", "document:outline=/proof,/ML")
+ else
+ options
+ }
+
+
+ final def hg_id(path: Path): String =
+ Isabelle_System.hg("id -i", path.file).out
+
+ final def print_section(title: String): Unit =
+ println(s"\n=== $title ===\n")
+
+
+ final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
+ final val isabelle_id = hg_id(isabelle_home)
+ final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
+
+
+ override final def apply(args: List[String]): Unit =
+ {
+ print_section("CONFIGURATION")
+ println(Build_Log.Settings.show())
+ val props = load_properties()
+ System.getProperties().putAll(props)
+
+ val options =
+ with_documents(Options.init())
+ .int.update("parallel_proofs", 2)
+ .int.update("threads", threads)
+
+ print_section("BUILD")
+ println(s"Build started at $start_time")
+ println(s"Isabelle id $isabelle_id")
+ pre_hook(args)
+
+ print_section("LOG")
+ val (results, elapsed_time) = build(options)
+
+ print_section("TIMING")
+
+ val groups = results.sessions.map(results.info).flatMap(_.groups)
+ for (group <- groups)
+ println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
+
+ val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
+ println("Overall: " + total_timing.message_resources)
+
+ if (!results.ok) {
+ print_section("FAILED SESSIONS")
+
+ for (name <- results.sessions) {
+ if (results.cancelled(name)) {
+ println(s"Session $name: CANCELLED")
+ }
+ else {
+ val result = results(name)
+ if (!result.ok)
+ println(s"Session $name: FAILED ${result.rc}")
+ }
+ }
+ }
+
+ post_hook(results)
+
+ System.exit(results.rc)
+ }
+
+
+ /* profile */
+
+ def documents: Boolean = true
+
+ def threads: Int
+ def jobs: Int
+ def include: List[Path]
+ def select: List[Path]
+
+ def pre_hook(args: List[String]): Unit
+ def post_hook(results: Build.Results): Unit
+
+ def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
+}
--- a/src/Pure/Tools/build_history.scala Wed Oct 12 09:32:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,388 +0,0 @@
-/* Title: Pure/Tools/build_history.scala
- Author: Makarius
-
-Build other history versions.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-import java.time.format.DateTimeFormatter
-import java.util.Locale
-
-
-object Build_History
-{
- /* log files */
-
- val BUILD_HISTORY = "build_history"
- val META_INFO_MARKER = "\fmeta_info = "
-
-
-
- /** other Isabelle environment **/
-
- private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
- {
- other_isabelle =>
-
-
- /* static system */
-
- def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
- Isabelle_System.bash(
- "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
- env = null, cwd = isabelle_home.file, redirect = redirect,
- progress_stdout = progress.echo_if(echo, _),
- progress_stderr = progress.echo_if(echo, _))
-
- def copy_dir(dir1: Path, dir2: Path): Unit =
- bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
-
- def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
- bash("bin/isabelle " + cmdline, redirect, echo)
-
- def resolve_components(echo: Boolean): Unit =
- other_isabelle("components -a", redirect = true, echo = echo).check
-
- val isabelle_home_user: Path =
- Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
-
- val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
- val log_dir: Path = isabelle_home_user + Path.explode("log")
-
-
- /* reset settings */
-
- def reset_settings(components_base: String, nonfree: Boolean)
- {
- if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
- error("Cannot proceed with existing user settings file: " + etc_settings)
-
- Isabelle_System.mkdirs(etc_settings.dir)
- File.write(etc_settings,
- "# generated by Isabelle " + Date.now() + "\n" +
- "#-*- shell-script -*- :mode=shellscript:\n")
-
- val component_settings =
- {
- val components_base_path =
- if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
- else Path.explode(components_base).expand
-
- val catalogs =
- if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
-
- catalogs.map(catalog =>
- "init_components " + File.bash_path(components_base_path) +
- " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
- }
- File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
- }
-
-
- /* augment settings */
-
- def augment_settings(
- threads: Int,
- arch_64: Boolean = false,
- heap: Int = default_heap,
- max_heap: Option[Int] = None,
- more_settings: List[String]): String =
- {
- val (ml_platform, ml_settings) =
- {
- val windows_32 = "x86-windows"
- val windows_64 = "x86_64-windows"
- val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
- val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
- val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
-
- val polyml_home =
- try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
- catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
-
- def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
-
- def err(platform: String): Nothing =
- error("Platform " + platform + " unavailable on this machine")
-
- def check_dir(platform: String): Boolean =
- platform != "" && ml_home(platform).is_dir
-
- val ml_platform =
- if (Platform.is_windows && arch_64) {
- if (check_dir(windows_64)) windows_64 else err(windows_64)
- }
- else if (Platform.is_windows && !arch_64) {
- if (check_dir(windows_32)) windows_32
- else platform_32 // x86-cygwin
- }
- else {
- val (platform, platform_name) =
- if (arch_64) (platform_64, "x86_64-" + platform_family)
- else (platform_32, "x86-" + platform_family)
- if (check_dir(platform)) platform else err(platform_name)
- }
-
- val ml_options =
- "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
- " --gcthreads " + threads +
- (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
-
- (ml_platform,
- List(
- "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
- "ML_PLATFORM=" + quote(ml_platform),
- "ML_OPTIONS=" + quote(ml_options)))
- }
-
- val thread_settings =
- List(
- "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
- "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
-
- val settings =
- List(ml_settings, thread_settings) :::
- (if (more_settings.isEmpty) Nil else List(more_settings))
-
- File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
-
- ml_platform
- }
- }
-
-
-
- /** build_history **/
-
- private val default_rev = "tip"
- private val default_threads = 1
- private val default_heap = 1000
- private val default_isabelle_identifier = "build_history"
-
- def build_history(
- progress: Progress,
- hg: Mercurial.Repository,
- rev: String = default_rev,
- isabelle_identifier: String = default_isabelle_identifier,
- components_base: String = "",
- fresh: Boolean = false,
- nonfree: Boolean = false,
- multicore_base: Boolean = false,
- threads_list: List[Int] = List(default_threads),
- arch_64: Boolean = false,
- heap: Int = default_heap,
- max_heap: Option[Int] = None,
- more_settings: List[String] = Nil,
- verbose: Boolean = false,
- build_args: List[String] = Nil): List[Process_Result] =
- {
- /* sanity checks */
-
- if (File.eq(Path.explode("~~").file, hg.root.file))
- error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
-
- for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
-
- if (heap < 100) error("Bad heap value < 100: " + heap)
-
- if (max_heap.isDefined && max_heap.get < heap)
- error("Bad max_heap value < heap: " + max_heap.get)
-
- System.getenv("ISABELLE_SETTINGS_PRESENT") match {
- case null | "" =>
- case _ => error("Cannot run build_history within existing Isabelle settings environment")
- }
-
-
- /* init repository */
-
- hg.update(rev = rev, clean = true)
- progress.echo_if(verbose, hg.log(rev, options = "-l1"))
-
- val isabelle_version = hg.identify(rev, options = "-i")
- val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
-
-
- /* main */
-
- val build_history_date = Date.now()
- val build_host = Isabelle_System.hostname()
-
- var first_build = true
- for (threads <- threads_list) yield
- {
- /* init settings */
-
- other_isabelle.reset_settings(components_base, nonfree)
- other_isabelle.resolve_components(verbose)
- val ml_platform =
- other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
-
- val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
- val isabelle_output_log = isabelle_output + Path.explode("log")
- val isabelle_base_log = isabelle_output + Path.explode("../base_log")
-
- if (first_build) {
- other_isabelle.resolve_components(verbose)
- other_isabelle.bash(
- "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
- "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
- redirect = true, echo = verbose).check
-
- Isabelle_System.rm_tree(isabelle_base_log.file)
- }
-
- Isabelle_System.rm_tree(isabelle_output.file)
- Isabelle_System.mkdirs(isabelle_output)
-
-
- /* build */
-
- if (multicore_base && !first_build && isabelle_base_log.is_dir)
- other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
-
- val build_start = Date.now()
- val res =
- other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
- val build_end = Date.now()
-
-
- /* output log */
-
- val log_path =
- other_isabelle.log_dir +
- Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
-
- val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
-
- val meta_info =
- List(Build_Log.Field.build_engine -> BUILD_HISTORY,
- Build_Log.Field.build_host -> build_host,
- Build_Log.Field.build_start -> Build_Log.print_date(build_start),
- Build_Log.Field.build_end -> Build_Log.print_date(build_end),
- Build_Log.Field.isabelle_version -> isabelle_version)
-
- val ml_statistics =
- build_info.finished_sessions.flatMap(session_name =>
- {
- val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
- if (session_log.is_file) {
- Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
- ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
- }
- else Nil
- })
-
- val heap_sizes =
- build_info.finished_sessions.flatMap(session_name =>
- {
- val heap = isabelle_output + Path.explode(session_name)
- if (heap.is_file)
- Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
- else None
- })
-
- Isabelle_System.mkdirs(log_path.dir)
- File.write_gzip(log_path,
- Library.terminate_lines(
- Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
- ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
- heap_sizes))
-
- Output.writeln(log_path.implode, stdout = true)
-
-
- /* next build */
-
- if (multicore_base && first_build && isabelle_output_log.is_dir)
- other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
-
- first_build = false
-
- res
- }
- }
-
-
- /* command line entry point */
-
- def main(args: Array[String])
- {
- Command_Line.tool0 {
- var multicore_base = false
- var components_base = ""
- var heap: Option[Int] = None
- var max_heap: Option[Int] = None
- var threads_list = List(default_threads)
- var isabelle_identifier = default_isabelle_identifier
- var more_settings: List[String] = Nil
- var fresh = false
- var arch_64 = false
- var nonfree = false
- var rev = default_rev
- var verbose = false
-
- val getopts = Getopts("""
-Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
-
- Options are:
- -B first multicore build serves as base for scheduling information
- -C DIR base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
- -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
- -M THREADS multicore configurations (comma-separated list, default: """ + default_threads + """)
- -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
- -U SIZE maximal ML heap in MB (default: unbounded)
- -e TEXT additional text for generated etc/settings
- -f fresh build of Isabelle/Scala components (recommended)
- -m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
- -n include nonfree components
- -r REV update to revision (default: """ + default_rev + """)
- -v verbose
-
- Build Isabelle sessions from the history of another REPOSITORY clone,
- passing ARGS directly to its isabelle build tool.
-""",
- "B" -> (_ => multicore_base = true),
- "C:" -> (arg => components_base = arg),
- "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
- "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
- "N:" -> (arg => isabelle_identifier = arg),
- "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
- "e:" -> (arg => more_settings = more_settings ::: List(arg)),
- "f" -> (_ => fresh = true),
- "m:" ->
- {
- case "32" | "x86" => arch_64 = false
- case "64" | "x86_64" => arch_64 = true
- case bad => error("Bad processor architecture: " + quote(bad))
- },
- "n" -> (_ => nonfree = true),
- "r:" -> (arg => rev = arg),
- "v" -> (_ => verbose = true))
-
- val more_args = getopts(args)
- val (root, build_args) =
- more_args match {
- case root :: build_args => (root, build_args)
- case _ => getopts.usage()
- }
-
- using(Mercurial.open_repository(Path.explode(root)))(hg =>
- {
- val progress = new Console_Progress(stderr = true)
- val results =
- build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
- components_base = components_base, fresh = fresh, nonfree = nonfree,
- multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
- heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
- max_heap = max_heap, more_settings = more_settings, verbose = verbose,
- build_args = build_args)
- val rc = (0 /: results) { case (rc, res) => rc max res.rc }
- if (rc != 0) sys.exit(rc)
- })
- }
- }
-}
--- a/src/Pure/Tools/build_log.scala Wed Oct 12 09:32:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,548 +0,0 @@
-/* Title: Pure/Tools/build_log.scala
- Author: Makarius
-
-Build log parsing for current and historic formats.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-import java.time.ZoneId
-import java.time.format.{DateTimeFormatter, DateTimeParseException}
-import java.util.Locale
-
-import scala.collection.mutable
-import scala.util.matching.Regex
-
-
-object Build_Log
-{
- /** directory content **/
-
- /* file names */
-
- def log_date(date: Date): String =
- String.format(Locale.ROOT, "%s.%05d",
- DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
- new java.lang.Long((date.time - date.midnight.time).ms / 1000))
-
- def log_path(engine: String, date: Date, more: String*): Path =
- Path.explode(date.rep.getYear.toString) +
- Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
-
-
- /* log file collections */
-
- def is_log(file: JFile): Boolean =
- List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
-
- def isatest_files(dir: Path): List[JFile] =
- File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
-
- def afp_test_files(dir: Path): List[JFile] =
- File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
-
-
-
- /** settings **/
-
- object Settings
- {
- val build_settings = List("ISABELLE_BUILD_OPTIONS")
- val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
- val all_settings = build_settings ::: ml_settings
-
- type Entry = (String, String)
- type T = List[Entry]
-
- object Entry
- {
- def unapply(s: String): Option[Entry] =
- s.indexOf('=') match {
- case -1 => None
- case i =>
- val a = s.substring(0, i)
- val b = Library.perhaps_unquote(s.substring(i + 1))
- Some((a, b))
- }
- def apply(a: String, b: String): String = a + "=" + quote(b)
- def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
- }
-
- def show(): String =
- cat_lines(
- build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
- }
-
-
-
- /** log file **/
-
- def print_date(date: Date): String = Log_File.Date_Format(date)
-
- object Log_File
- {
- def apply(name: String, lines: List[String]): Log_File =
- new Log_File(name, lines)
-
- def apply(name: String, text: String): Log_File =
- Log_File(name, Library.trim_split_lines(text))
-
- def apply(file: JFile): Log_File =
- {
- val name = file.getName
- val (base_name, text) =
- Library.try_unsuffix(".gz", name) match {
- case Some(base_name) => (base_name, File.read_gzip(file))
- case None =>
- Library.try_unsuffix(".xz", name) match {
- case Some(base_name) => (base_name, File.read_xz(file))
- case None => (name, File.read(file))
- }
- }
- apply(base_name, text)
- }
-
- def apply(path: Path): Log_File = apply(path.file)
-
-
- /* date format */
-
- val Date_Format =
- {
- val fmts =
- Date.Formatter.variants(
- List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
- List(Locale.ENGLISH, Locale.GERMAN)) :::
- List(
- DateTimeFormatter.RFC_1123_DATE_TIME,
- Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
-
- def tune_timezone(s: String): String =
- s match {
- case "CET" | "MET" => "GMT+1"
- case "CEST" | "MEST" => "GMT+2"
- case "EST" => "Europe/Berlin"
- case _ => s
- }
- def tune_weekday(s: String): String =
- s match {
- case "Die" => "Di"
- case "Mit" => "Mi"
- case "Don" => "Do"
- case "Fre" => "Fr"
- case "Sam" => "Sa"
- case "Son" => "So"
- case _ => s
- }
-
- def tune(s: String): String =
- Word.implode(
- Word.explode(s) match {
- case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
- case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
- case Nil => Nil
- }
- )
-
- Date.Format.make(fmts, tune)
- }
-
-
- /* inlined content */
-
- def print_props(marker: String, props: Properties.T): String =
- marker + YXML.string_of_body(XML.Encode.properties(props))
- }
-
- class Log_File private(val name: String, val lines: List[String])
- {
- log_file =>
-
- override def toString: String = name
-
- def text: String = cat_lines(lines)
-
- def err(msg: String): Nothing =
- error("Error in log file " + quote(name) + ": " + msg)
-
-
- /* date format */
-
- object Strict_Date
- {
- def unapply(s: String): Some[Date] =
- try { Some(Log_File.Date_Format.parse(s)) }
- catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
- }
-
-
- /* inlined content */
-
- def find[A](f: String => Option[A]): Option[A] =
- lines.iterator.map(f).find(_.isDefined).map(_.get)
-
- def find_match(regex: Regex): Option[String] =
- lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
- map(res => res.get.head)
-
-
- /* settings */
-
- def get_setting(a: String): Option[Settings.Entry] =
- lines.find(_.startsWith(a + "=")) match {
- case Some(line) => Settings.Entry.unapply(line)
- case None => None
- }
-
- def get_settings(as: List[String]): Settings.T =
- for { a <- as; entry <- get_setting(a) } yield entry
-
-
- /* properties (YXML) */
-
- val xml_cache = new XML.Cache()
-
- def parse_props(text: String): Properties.T =
- xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
-
- def filter_props(marker: String): List[Properties.T] =
- for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
-
- def find_line(marker: String): Option[String] =
- find(Library.try_unprefix(marker, _))
-
- def find_props(marker: String): Option[Properties.T] =
- find_line(marker).map(parse_props(_))
-
-
- /* parse various formats */
-
- def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
-
- def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
-
- def parse_session_info(
- default_name: String = "",
- command_timings: Boolean = false,
- ml_statistics: Boolean = false,
- task_statistics: Boolean = false): Session_Info =
- Build_Log.parse_session_info(
- log_file, default_name, command_timings, ml_statistics, task_statistics)
- }
-
-
-
- /** meta info **/
-
- object Field
- {
- val build_engine = "build_engine"
- val build_host = "build_host"
- val build_start = "build_start"
- val build_end = "build_end"
- val isabelle_version = "isabelle_version"
- val afp_version = "afp_version"
- }
-
- object Meta_Info
- {
- val empty: Meta_Info = Meta_Info(Nil, Nil)
- }
-
- sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
- {
- def is_empty: Boolean = props.isEmpty && settings.isEmpty
- }
-
- object Isatest
- {
- val engine = "isatest"
- val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
- val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
- val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
- val No_AFP_Version = new Regex("""$.""")
- }
-
- object AFP_Test
- {
- val engine = "afp-test"
- val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
- val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
- val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
- val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
- val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
- val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
- }
-
- object Jenkins
- {
- val engine = "jenkins"
- val Start = new Regex("""^Started .*$""")
- val Start_Date = new Regex("""^Build started at (.+)$""")
- val No_End = new Regex("""$.""")
- val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
- val AFP_Version = new Regex("""^AFP id (\S+)$""")
- val CONFIGURATION = "=== CONFIGURATION ==="
- val BUILD = "=== BUILD ==="
- val FINISHED = "Finished: "
- }
-
- private def parse_meta_info(log_file: Log_File): Meta_Info =
- {
- def parse(engine: String, host: String, start: Date,
- End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
- {
- val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
- val build_host = if (host == "") Nil else List(Field.build_host -> host)
-
- val start_date = List(Field.build_start -> start.toString)
- val end_date =
- log_file.lines.last match {
- case End(log_file.Strict_Date(end_date)) =>
- List(Field.build_end -> end_date.toString)
- case _ => Nil
- }
-
- val isabelle_version =
- log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
- val afp_version =
- log_file.find_match(AFP_Version).map(Field.afp_version -> _)
-
- Meta_Info(build_engine ::: build_host :::
- start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
- log_file.get_settings(Settings.all_settings))
- }
-
- log_file.lines match {
- case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
- Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
- log_file.get_settings(Settings.all_settings))
-
- case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
- parse(Isatest.engine, host, start, Isatest.End,
- Isatest.Isabelle_Version, Isatest.No_AFP_Version)
-
- case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
- parse(AFP_Test.engine, host, start, AFP_Test.End,
- AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
-
- case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
- parse(AFP_Test.engine, "", start, AFP_Test.End,
- AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
-
- case Jenkins.Start() :: _
- if log_file.lines.contains(Jenkins.CONFIGURATION) ||
- log_file.lines.last.startsWith(Jenkins.FINISHED) =>
- log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
- case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
- parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
- Jenkins.Isabelle_Version, Jenkins.AFP_Version)
- case _ => Meta_Info.empty
- }
-
- case line :: _ if line.startsWith("\0") => Meta_Info.empty
- case List(Isatest.End(_)) => Meta_Info.empty
- case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
- case Nil => Meta_Info.empty
-
- case _ => log_file.err("cannot detect log file format")
- }
- }
-
-
-
- /** build info: produced by isabelle build or build_history **/
-
- val ML_STATISTICS_MARKER = "\fML_statistics = "
- val SESSION_NAME = "session_name"
-
- object Session_Status extends Enumeration
- {
- val EXISTING = Value("existing")
- val FINISHED = Value("finished")
- val FAILED = Value("failed")
- val CANCELLED = Value("cancelled")
- }
-
- sealed case class Session_Entry(
- chapter: String,
- groups: List[String],
- threads: Option[Int],
- timing: Timing,
- ml_timing: Timing,
- ml_statistics: List[Properties.T],
- heap_size: Option[Long],
- status: Session_Status.Value)
- {
- def finished: Boolean = status == Session_Status.FINISHED
- }
-
- sealed case class Build_Info(sessions: Map[String, Session_Entry])
- {
- def session(name: String): Session_Entry = sessions(name)
- def get_session(name: String): Option[Session_Entry] = sessions.get(name)
-
- def get_default[A](name: String, f: Session_Entry => A, x: A): A =
- get_session(name) match {
- case Some(entry) => f(entry)
- case None => x
- }
-
- def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
- def finished(name: String): Boolean = get_default(name, _.finished, false)
- def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
- def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
- }
-
- private def parse_build_info(log_file: Log_File): Build_Info =
- {
- object Chapter_Name
- {
- def unapply(s: String): Some[(String, String)] =
- space_explode('/', s) match {
- case List(chapter, name) => Some((chapter, name))
- case _ => Some(("", s))
- }
- }
-
- val Session_No_Groups = new Regex("""^Session (\S+)$""")
- val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
- val Session_Finished1 =
- new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
- val Session_Finished2 =
- new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
- val Session_Timing =
- new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
- val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
- val Session_Failed = new Regex("""^(\S+) FAILED""")
- val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
- val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
-
- var chapter = Map.empty[String, String]
- var groups = Map.empty[String, List[String]]
- var threads = Map.empty[String, Int]
- var timing = Map.empty[String, Timing]
- var ml_timing = Map.empty[String, Timing]
- var started = Set.empty[String]
- var failed = Set.empty[String]
- var cancelled = Set.empty[String]
- var ml_statistics = Map.empty[String, List[Properties.T]]
- var heap_sizes = Map.empty[String, Long]
-
- def all_sessions: Set[String] =
- chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
- failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
-
-
- for (line <- log_file.lines) {
- line match {
- case Session_No_Groups(Chapter_Name(chapt, name)) =>
- chapter += (name -> chapt)
- groups += (name -> Nil)
-
- case Session_Groups(Chapter_Name(chapt, name), grps) =>
- chapter += (name -> chapt)
- groups += (name -> Word.explode(grps))
-
- case Session_Started(name) =>
- started += name
-
- case Session_Finished1(name,
- Value.Int(e1), Value.Int(e2), Value.Int(e3),
- Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
- val elapsed = Time.hms(e1, e2, e3)
- val cpu = Time.hms(c1, c2, c3)
- timing += (name -> Timing(elapsed, cpu, Time.zero))
-
- case Session_Finished2(name,
- Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
- val elapsed = Time.hms(e1, e2, e3)
- timing += (name -> Timing(elapsed, Time.zero, Time.zero))
-
- case Session_Timing(name,
- Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
- val elapsed = Time.seconds(e)
- val cpu = Time.seconds(c)
- val gc = Time.seconds(g)
- ml_timing += (name -> Timing(elapsed, cpu, gc))
- threads += (name -> t)
-
- case Heap(name, Value.Long(size)) =>
- heap_sizes += (name -> size)
-
- case _ if line.startsWith(ML_STATISTICS_MARKER) =>
- val (name, props) =
- Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
- case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
- case _ => log_file.err("malformed ML_statistics " + quote(line))
- }
- ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
-
- case _ =>
- }
- }
-
- val sessions =
- Map(
- (for (name <- all_sessions.toList) yield {
- val status =
- if (failed(name)) Session_Status.FAILED
- else if (cancelled(name)) Session_Status.CANCELLED
- else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
- Session_Status.FINISHED
- else if (started(name)) Session_Status.FAILED
- else Session_Status.EXISTING
- val entry =
- Session_Entry(
- chapter.getOrElse(name, ""),
- groups.getOrElse(name, Nil),
- threads.get(name),
- timing.getOrElse(name, Timing.zero),
- ml_timing.getOrElse(name, Timing.zero),
- ml_statistics.getOrElse(name, Nil).reverse,
- heap_sizes.get(name),
- status)
- (name -> entry)
- }):_*)
- Build_Info(sessions)
- }
-
-
-
- /** session info: produced by "isabelle build" **/
-
- sealed case class Session_Info(
- session_name: String,
- session_timing: Properties.T,
- command_timings: List[Properties.T],
- ml_statistics: List[Properties.T],
- task_statistics: List[Properties.T])
-
- private def parse_session_info(
- log_file: Log_File,
- default_name: String,
- command_timings: Boolean,
- ml_statistics: Boolean,
- task_statistics: Boolean): Session_Info =
- {
- val xml_cache = new XML.Cache()
-
- val session_name =
- log_file.find_line("\fSession.name = ") match {
- case None => default_name
- case Some(name) if default_name == "" || default_name == name => name
- case Some(name) => log_file.err("log from different session " + quote(name))
- }
- val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
- val command_timings_ =
- if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
- val ml_statistics_ =
- if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
- val task_statistics_ =
- if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
-
- Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
- }
-}
--- a/src/Pure/Tools/ci_api.scala Wed Oct 12 09:32:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-/* Title: Pure/Tools/ci_api.scala
- Author: Makarius
-
-API for Isabelle Jenkins continuous integration services.
-*/
-
-package isabelle
-
-
-import java.net.URL
-
-import scala.util.matching.Regex
-
-
-object CI_API
-{
- /* CI service */
-
- def root(): String =
- Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
-
- def invoke(url: String, args: String*): Any =
- {
- val req = url + "/api/json?" + args.mkString("&")
- val result = Url.read(req)
- try { JSON.parse(result) }
- catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
- }
-
-
- /* build jobs */
-
- def build_jobs(): List[String] =
- for {
- job <- JSON.array(invoke(root()), "jobs")
- _class <- JSON.string(job, "_class")
- if _class == "hudson.model.FreeStyleProject"
- name <- JSON.string(job, "name")
- } yield name
-
- sealed case class Job_Info(
- job_name: String,
- timestamp: Long,
- output: URL,
- session_logs: List[(String, URL)])
- {
- def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
- def read_session_log(name: String): Build_Log.Log_File =
- Build_Log.Log_File(name,
- session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
- }
-
- def build_job_builds(job_name: String): List[Job_Info] =
- {
- val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
-
- for {
- build <- JSON.array(
- invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
- number <- JSON.int(build, "number")
- timestamp <- JSON.long(build, "timestamp")
- } yield {
- val job_prefix = root() + "/job/" + job_name + "/" + number
- val output = Url(job_prefix + "/consoleText")
- val session_logs =
- for {
- artifact <- JSON.array(build, "artifacts")
- log_path <- JSON.string(artifact, "relativePath")
- session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
- } yield (session -> Url(job_prefix + "/artifact/" + log_path))
- Job_Info(job_name, timestamp, output, session_logs)
- }
- }
-}
--- a/src/Pure/Tools/ci_profile.scala Wed Oct 12 09:32:48 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-/* Title: Pure/Tools/ci_profile.scala
- Author: Lars Hupel
-
-Build profile for continuous integration services.
-*/
-
-package isabelle
-
-
-import java.time.{Instant, ZoneId}
-import java.time.format.DateTimeFormatter
-import java.util.{Properties => JProperties}
-
-
-abstract class CI_Profile extends Isabelle_Tool.Body
-{
- private def build(options: Options): (Build.Results, Time) =
- {
- val progress = new Console_Progress(verbose = true)
- val start_time = Time.now()
- val results = progress.interrupt_handler {
- Build.build_selection(
- options = options,
- progress = progress,
- clean_build = true,
- verbose = true,
- max_jobs = jobs,
- dirs = include,
- select_dirs = select,
- system_mode = true,
- selection = select_sessions _)
- }
- val end_time = Time.now()
- (results, end_time - start_time)
- }
-
- private def load_properties(): JProperties =
- {
- val props = new JProperties()
- val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
-
- if (file_name != "")
- {
- val file = Path.explode(file_name).file
- if (file.exists())
- props.load(new java.io.FileReader(file))
- props
- }
- else
- props
- }
-
- private def compute_timing(results: Build.Results, group: Option[String]): Timing =
- {
- val timings = results.sessions.collect {
- case session if group.forall(results.info(session).groups.contains(_)) =>
- results(session).timing
- }
- (Timing.zero /: timings)(_ + _)
- }
-
- private def with_documents(options: Options): Options =
- {
- if (documents)
- options
- .bool.update("browser_info", true)
- .string.update("document", "pdf")
- .string.update("document_variants", "document:outline=/proof,/ML")
- else
- options
- }
-
-
- final def hg_id(path: Path): String =
- Isabelle_System.hg("id -i", path.file).out
-
- final def print_section(title: String): Unit =
- println(s"\n=== $title ===\n")
-
-
- final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
- final val isabelle_id = hg_id(isabelle_home)
- final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
-
-
- override final def apply(args: List[String]): Unit =
- {
- print_section("CONFIGURATION")
- println(Build_Log.Settings.show())
- val props = load_properties()
- System.getProperties().putAll(props)
-
- val options =
- with_documents(Options.init())
- .int.update("parallel_proofs", 2)
- .int.update("threads", threads)
-
- print_section("BUILD")
- println(s"Build started at $start_time")
- println(s"Isabelle id $isabelle_id")
- pre_hook(args)
-
- print_section("LOG")
- val (results, elapsed_time) = build(options)
-
- print_section("TIMING")
-
- val groups = results.sessions.map(results.info).flatMap(_.groups)
- for (group <- groups)
- println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
-
- val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
- println("Overall: " + total_timing.message_resources)
-
- if (!results.ok) {
- print_section("FAILED SESSIONS")
-
- for (name <- results.sessions) {
- if (results.cancelled(name)) {
- println(s"Session $name: CANCELLED")
- }
- else {
- val result = results(name)
- if (!result.ok)
- println(s"Session $name: FAILED ${result.rc}")
- }
- }
- }
-
- post_hook(results)
-
- System.exit(results.rc)
- }
-
-
- /* profile */
-
- def documents: Boolean = true
-
- def threads: Int
- def jobs: Int
- def include: List[Path]
- def select: List[Path]
-
- def pre_hook(args: List[String]): Unit
- def post_hook(results: Build.Results): Unit
-
- def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
-}
--- a/src/Pure/build-jars Wed Oct 12 09:32:48 2016 +0200
+++ b/src/Pure/build-jars Wed Oct 12 09:38:20 2016 +0200
@@ -9,6 +9,10 @@
## sources
declare -a SOURCES=(
+ Admin/build_history.scala
+ Admin/build_log.scala
+ Admin/ci_api.scala
+ Admin/ci_profile.scala
Admin/isabelle_cronjob.scala
Concurrent/consumer_thread.scala
Concurrent/counter.scala
@@ -110,13 +114,9 @@
Tools/bibtex.scala
Tools/build.scala
Tools/build_doc.scala
- Tools/build_history.scala
- Tools/build_log.scala
Tools/build_stats.scala
Tools/check_keywords.scala
Tools/check_sources.scala
- Tools/ci_api.scala
- Tools/ci_profile.scala
Tools/debugger.scala
Tools/doc.scala
Tools/main.scala