# HG changeset patch # User wenzelm # Date 1476257900 -7200 # Node ID 1eea419fab65117898c360475d744575ec67d47b # Parent fe8f8f88a1d72c95e26fa4cccd446123b96c2230 clarified files; diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Admin/build_history.scala --- /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) + }) + } + } +} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Admin/build_log.scala --- /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_) + } +} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Admin/ci_api.scala --- /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) + } + } +} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Admin/ci_profile.scala --- /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) +} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Tools/build_history.scala --- 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) - }) - } - } -} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Tools/build_log.scala --- 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_) - } -} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Tools/ci_api.scala --- 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) - } - } -} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/Tools/ci_profile.scala --- 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) -} diff -r fe8f8f88a1d7 -r 1eea419fab65 src/Pure/build-jars --- 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