# HG changeset patch # User traytel # Date 1475753640 -7200 # Node ID 3a506cb576d3b45804af211ece8858cc18801ce6 # Parent 6855c2f7aa6a435eb60c8d0b41efe19327e556a5# Parent f3ac9153bc0d97fcd42df0da7888f66ed70710b9 merged diff -r 6855c2f7aa6a -r 3a506cb576d3 .hgtags --- a/.hgtags Thu Oct 06 13:33:26 2016 +0200 +++ b/.hgtags Thu Oct 06 13:34:00 2016 +0200 @@ -25,6 +25,7 @@ 6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011 76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1 21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012 +20126dd9772c973118879a6878acfd9e6c66f1e7 build_history_base d90218288d517942cfbc80a6b2654ecb22735e5c Isabelle2013 9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1 4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2 diff -r 6855c2f7aa6a -r 3a506cb576d3 Admin/build_history --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/build_history Thu Oct 06 13:34:00 2016 +0200 @@ -0,0 +1,10 @@ +#!/usr/bin/env bash +# +# DESCRIPTION: build history versions from another repository clone + + +THIS="$(cd "$(dirname "$0")"; pwd)" + +"$THIS/build" jars || exit $? + +exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@" diff -r 6855c2f7aa6a -r 3a506cb576d3 bin/isabelle_java --- a/bin/isabelle_java Thu Oct 06 13:33:26 2016 +0200 +++ b/bin/isabelle_java Thu Oct 06 13:34:00 2016 +0200 @@ -14,7 +14,16 @@ ( source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 - declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)" + case "$ISABELLE_JAVA_PLATFORM" in + x86-*) + ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS32" + ;; + x86_64-*) + ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS64" + ;; + esac + + declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $ISABELLE_TOOL_JAVA_OPTIONS)" if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" @@ -64,6 +73,7 @@ echo "Unknown JAVA_HOME -- Java unavailable" >&2 exit 127 else + unset ISABELLE_HOME unset CLASSPATH exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" -classpath "$ISABELLE_CLASSPATH" "$@" fi diff -r 6855c2f7aa6a -r 3a506cb576d3 lib/dummy_stty/stty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/dummy_stty/stty Thu Oct 06 13:34:00 2016 +0200 @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# +# dummy stty for old versions of scalac (e.g. 2.10.0) diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Concurrent/event_timer.scala --- a/src/Pure/Concurrent/event_timer.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Concurrent/event_timer.scala Thu Oct 06 13:34:00 2016 +0200 @@ -11,7 +11,7 @@ package isabelle -import java.util.{Timer, TimerTask, Date} +import java.util.{Timer, TimerTask, Date => JDate} object Event_Timer @@ -26,7 +26,7 @@ def request(time: Time)(event: => Unit): Request = { val task = new TimerTask { def run { event } } - event_timer.schedule(task, new Date(time.ms)) + event_timer.schedule(task, new JDate(time.ms)) new Request(time, task) } } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/General/date.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/date.scala Thu Oct 06 13:34:00 2016 +0200 @@ -0,0 +1,82 @@ +/* Title: Pure/General/date.scala + Author: Makarius + +Date and time, with time zone. +*/ + +package isabelle + + +import java.time.{Instant, ZonedDateTime, ZoneId} +import java.time.format.{DateTimeFormatter, DateTimeParseException} +import java.time.temporal.TemporalAccessor + +import scala.annotation.tailrec + + +object Date +{ + /* format */ + + object Format + { + def make(fmts: List[DateTimeFormatter], filter: String => String = s => s): Format = + { + require(fmts.nonEmpty) + + @tailrec def parse_first( + last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor = + { + fs match { + case Nil => throw last_exn.get + case f :: rest => + try { ZonedDateTime.from(f.parse(str)) } + catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) } + } + } + new Format { + def apply(date: Date): String = fmts.head.format(date.rep) + def parse(str: String): Date = + new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str)))) + } + } + + def make_patterns(patterns: List[String], filter: String => String = s => s): Format = + make(patterns.toList.map(DateTimeFormatter.ofPattern(_)), filter) + + def apply(patterns: String*): Format = + make(patterns.toList.map(DateTimeFormatter.ofPattern(_))) + + val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx") + val date: Format = apply("dd-MMM-uuuu") + val time: Format = apply("HH:mm:ss") + } + + abstract class Format private + { + def apply(date: Date): String + def parse(str: String): Date + def unapply(str: String): Option[Date] = + try { Some(parse(str)) } + catch { case _: DateTimeParseException => None } + } + + + /* date operations */ + + def timezone(): ZoneId = ZoneId.systemDefault + + def now(zone: ZoneId = timezone()): Date = new Date(ZonedDateTime.now(zone)) + + def apply(t: Time, zone: ZoneId = timezone()): Date = + new Date(ZonedDateTime.ofInstant(t.instant, zone)) +} + +sealed case class Date(rep: ZonedDateTime) +{ + def time: Time = Time.instant(Instant.from(rep)) + def timezone: ZoneId = rep.getZone + + def format(fmt: Date.Format = Date.Format.default): String = fmt(this) + override def toString: String = format() +} diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/General/mercurial.scala Thu Oct 06 13:34:00 2016 +0200 @@ -33,18 +33,22 @@ def close() { } def command(cmd: String, cwd: JFile = null): Process_Result = - Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd) + Isabelle_System.hg("--repository " + File.bash_path(root) + " --noninteractive " + cmd, + cwd = cwd) def heads(template: String = "{node|short}\n", options: String = ""): List[String] = command("heads " + options + opt_template(template)).check.out_lines def identify(rev: String = "", options: String = ""): String = - command("id -i " + options + opt_rev(rev)).check.out_lines.headOption getOrElse "" + command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse "" def manifest(rev: String = "", options: String = ""): List[String] = command("manifest " + options + opt_rev(rev)).check.out_lines + def log(rev: String = "", template: String = "", options: String = ""): String = + Library.trim_line(command("log " + options + opt_rev(rev) + opt_template(template)).check.out) + def pull(remote: String = "", rev: String = "", options: String = ""): Unit = command("pull " + options + opt_rev(rev) + optional(remote)).check diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/General/time.scala --- a/src/Pure/General/time.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/General/time.scala Thu Oct 06 13:34:00 2016 +0200 @@ -9,6 +9,7 @@ import java.util.Locale +import java.time.Instant object Time @@ -25,6 +26,8 @@ def print_seconds(s: Double): String = String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef]) + + def instant(t: Instant): Time = ms(t.getEpochSecond * 1000L + t.getNano / 1000000L) } final class Time private(val ms: Long) extends AnyVal @@ -57,4 +60,6 @@ String.format(Locale.ROOT, "%d:%02d:%02d", new java.lang.Long(s / 3600), new java.lang.Long((s / 60) % 60), new java.lang.Long(s % 60)) } + + def instant: Instant = Instant.ofEpochMilli(ms) } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/System/isabelle_system.scala Thu Oct 06 13:34:00 2016 +0200 @@ -260,7 +260,10 @@ val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) - proc.environment.clear; for ((x, y) <- env) proc.environment.put(x, y) + if (env != null) { + proc.environment.clear + for ((x, y) <- env) proc.environment.put(x, y) + } proc.redirectErrorStream(redirect) proc.start } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/System/process_result.scala Thu Oct 06 13:34:00 2016 +0200 @@ -40,4 +40,7 @@ Output.writeln(Library.trim_line(out), stdout = true) copy(out_lines = Nil, err_lines = Nil) } + + def print_if(b: Boolean): Process_Result = if (b) print else this + def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/System/progress.scala Thu Oct 06 13:34:00 2016 +0200 @@ -10,6 +10,7 @@ class Progress { def echo(msg: String) {} + def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } def theory(session: String, theory: String) {} def stopped: Boolean = false override def toString: String = if (stopped) "Progress(stopped)" else "Progress" diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/build.scala Thu Oct 06 13:34:00 2016 +0200 @@ -334,48 +334,6 @@ } - /* inlined properties (YXML) */ - - object Props - { - def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text)) - - def parse_lines(prefix: String, lines: List[String]): List[Properties.T] = - for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s) - - def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] = - lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length))) - } - - - /* log files */ - - private val SESSION_NAME = "\fSession.name = " - - sealed case class Log_Info( - name: String, - stats: List[Properties.T], - tasks: List[Properties.T], - command_timings: List[Properties.T], - session_timing: Properties.T) - - def parse_log(full_stats: Boolean, text: String): Log_Info = - { - val lines = split_lines(text) - val xml_cache = new XML.Cache() - def parse_lines(prfx: String): List[Properties.T] = - Props.parse_lines(prfx, lines).map(xml_cache.props(_)) - - val name = - lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse "" - val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil - val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil - val command_timings = parse_lines("\fcommand_timing = ") - val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil - Log_Info(name, stats, tasks, command_timings, session_timing) - } - - /* sources and heaps */ private val SOURCES = "sources: " @@ -519,7 +477,7 @@ } try { - val info = parse_log(false, text) + val info = Build_Log.Log_File(name, text).parse_session_info(name, false) val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0 (info.command_timings, session_timing) } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/build_history.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/build_history.scala Thu Oct 06 13:34:00 2016 +0200 @@ -0,0 +1,320 @@ +/* Title: Pure/Tools/build_history.scala + Author: Makarius + +Build other history versions. +*/ + +package isabelle + + +import java.io.{File => JFile} +import java.util.Calendar + + +object Build_History +{ + /** 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") + + + /* 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 " + Calendar.getInstance.getTime + "\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]) + { + val 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 "") + + 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(_)))) + } + } + + + + /** 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 other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier) + + + /* main */ + + var first_build = true + for (threads <- threads_list) yield + { + /* init settings */ + + other_isabelle.reset_settings(components_base, nonfree) + other_isabelle.resolve_components(verbose) + 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 res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = true) + + 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(false) + 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 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/build_log.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/build_log.scala Thu Oct 06 13:34:00 2016 +0200 @@ -0,0 +1,258 @@ +/* Title: Pure/Tools/build_log.scala + Author: Makarius + +Build log parsing for historic versions, back to "build_history_base". +*/ + +package isabelle + + +import java.time.ZonedDateTime +import java.time.format.{DateTimeFormatter, DateTimeParseException} + +import scala.collection.mutable +import scala.util.matching.Regex + + +object Build_Log +{ + /** log file **/ + + 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)) + } + + 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) + + + /* 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(setting: String): String = + lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting) + + def get_settings(settings: List[String]): List[String] = + settings.map(get_setting(_)) + + + /* 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(prefix: String): List[Properties.T] = + for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s) + + def find_line(prefix: String): Option[String] = + find(Library.try_unprefix(prefix, _)) + + def find_props(prefix: String): Option[Properties.T] = + find_line(prefix).map(parse_props(_)) + + + /* parse various formats */ + + def parse_session_info(session_name: String, full: Boolean): Session_Info = + Build_Log.parse_session_info(log_file, session_name, full) + + def parse_header: Header = Build_Log.parse_header(log_file) + + def parse_info: Info = Build_Log.parse_info(log_file) + } + + + /* session log: 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, name0: String, full: Boolean): Session_Info = + { + val xml_cache = new XML.Cache() + + val session_name = + log_file.find_line("\fSession.name = ") match { + case None => name0 + case Some(name) if name0 == "" || name0 == 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 = log_file.filter_props("\fcommand_timing = ") + val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil + val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil + + Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics) + } + + + /* header and meta data */ + + object Header_Kind extends Enumeration + { + val ISATEST = Value("isatest") + val AFP_TEST = Value("afp-test") + val JENKINS = Value("jenkins") + } + + sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String]) + + object Field + { + 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" + } + + val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") + + object AFP + { + val Date_Format = + Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), + // workaround for jdk-8u102 + s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a }))) + + val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""") + val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""") + val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""") + val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""") + val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings + } + + private def parse_header(log_file: Log_File): Header = + { + log_file.lines match { + case AFP.Test_Start(start, hostname) :: _ => + (start, log_file.lines.last) match { + case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) => + val isabelle_version = + log_file.find_match(AFP.Isabelle_Version) getOrElse + log_file.err("missing Isabelle version") + val afp_version = + log_file.find_match(AFP.AFP_Version) getOrElse + log_file.err("missing AFP version") + + Header(Header_Kind.AFP_TEST, + List( + Field.build_host -> hostname, + Field.build_start -> start_date.toString, + Field.build_end -> end_date.toString, + Field.isabelle_version -> isabelle_version, + Field.afp_version -> afp_version), + log_file.get_settings(AFP.settings)) + + case _ => log_file.err("cannot detect start/end date in afp-test log") + } + case _ => log_file.err("cannot detect log header format") + } + } + + object Session_Status extends Enumeration + { + val UNKNOWN = Value("unknown") + val FINISHED = Value("finished") + val FAILED = Value("failed") + val CANCELLED = Value("cancelled") + } + + + /* main log: produced by isatest, afp-test, jenkins etc. */ + + sealed case class Info( + ml_options: List[(String, String)], + finished: Map[String, Timing], + timing: Map[String, Timing], + threads: Map[String, Int]) + { + val sessions: Set[String] = finished.keySet ++ timing.keySet + + override def toString: String = + sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")") + } + + private val Session_Finished1 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") + private val Session_Finished2 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") + private val Session_Timing = + new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") + + private object ML_Option + { + def unapply(s: String): Option[(String, String)] = + s.indexOf('=') match { + case -1 => None + case i => + val a = s.substring(0, i) + Library.try_unquote(s.substring(i + 1)) match { + case Some(b) if Build.ml_options.contains(a) => Some((a, b)) + case _ => None + } + } + } + + private def parse_info(log_file: Log_File): Info = + { + val ml_options = new mutable.ListBuffer[(String, String)] + var finished = Map.empty[String, Timing] + var timing = Map.empty[String, Timing] + var threads = Map.empty[String, Int] + + for (line <- log_file.lines) { + line match { + 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) + finished += (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) + finished += (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) + timing += (name -> Timing(elapsed, cpu, gc)) + threads += (name -> t) + case ML_Option(a, b) => ml_options += (a -> b) + case _ => + } + } + + Info(ml_options.toList, finished, timing, threads) + } +} diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Thu Oct 06 13:34:00 2016 +0200 @@ -7,70 +7,8 @@ package isabelle -import scala.collection.mutable -import scala.util.matching.Regex - - object Build_Stats { - /* parse build output */ - - private val Session_Finished1 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") - private val Session_Finished2 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") - private val Session_Timing = - new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") - - private object ML_Option - { - def unapply(s: String): Option[(String, String)] = - s.indexOf('=') match { - case -1 => None - case i => - val a = s.substring(0, i) - Library.try_unquote(s.substring(i + 1)) match { - case Some(b) if Build.ml_options.contains(a) => Some((a, b)) - case _ => None - } - } - } - - def parse(text: String): Build_Stats = - { - val ml_options = new mutable.ListBuffer[(String, String)] - var finished = Map.empty[String, Timing] - var timing = Map.empty[String, Timing] - var threads = Map.empty[String, Int] - - for (line <- split_lines(text)) { - line match { - 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) - finished += (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) - finished += (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) - timing += (name -> Timing(elapsed, cpu, gc)) - threads += (name -> t) - case ML_Option(a, b) => ml_options += (a -> b) - case _ => - } - } - - Build_Stats(ml_options.toList, finished, timing, threads) - } - - /* presentation */ private val default_history_length = 100 @@ -86,18 +24,18 @@ elapsed_threshold: Time = default_elapsed_threshold, ml_timing: Option[Boolean] = default_ml_timing): List[String] = { - val build_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) - if (build_infos.isEmpty) error("No build infos for job " + quote(job)) + val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) + if (job_infos.isEmpty) error("No build infos for job " + quote(job)) - val all_build_stats = - Par_List.map((info: CI_API.Build_Info) => - (info.timestamp / 1000, parse(Url.read(info.output))), build_infos) + val all_infos = + Par_List.map((job_info: CI_API.Job_Info) => + (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos) val all_sessions = - (Set.empty[String] /: all_build_stats)( - { case (s, (_, stats)) => s ++ stats.sessions }) + (Set.empty[String] /: all_infos)( + { case (s, (_, info)) => s ++ info.sessions }) - def check_threshold(stats: Build_Stats, session: String): Boolean = - stats.finished.get(session) match { + def check_threshold(info: Build_Log.Info, session: String): Boolean = + info.finished.get(session) match { case Some(t) => t.elapsed >= elapsed_threshold case None => false } @@ -105,7 +43,7 @@ val sessions = for { session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions) - if all_build_stats.filter({ case (_, stats) => check_threshold(stats, session) }).length >= 3 + if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3 } yield session Isabelle_System.mkdirs(dir) @@ -113,10 +51,10 @@ Isabelle_System.with_tmp_file(session, "png") { data_file => Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => val data = - for { (t, stats) <- all_build_stats if stats.finished.isDefinedAt(session) } + for { (t, info) <- all_infos if info.finished.isDefinedAt(session) } yield { - val finished = stats.finished.getOrElse(session, Timing.zero) - val timing = stats.timing.getOrElse(session, Timing.zero) + val finished = info.finished.getOrElse(session, Timing.zero) + val timing = info.timing.getOrElse(session, Timing.zero) List(t.toString, finished.elapsed.minutes, finished.cpu.minutes, timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ") } @@ -247,15 +185,3 @@ "\n\n" + html_footer) }) } - -sealed case class Build_Stats( - ml_options: List[(String, String)], - finished: Map[String, Timing], - timing: Map[String, Timing], - threads: Map[String, Int]) -{ - val sessions: Set[String] = finished.keySet ++ timing.keySet - - override def toString: String = - sessions.toList.sorted.mkString("Build_Stats(", ", ", ")") -} diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Thu Oct 06 13:34:00 2016 +0200 @@ -38,19 +38,22 @@ name <- JSON.string(job, "name") } yield name - sealed case class Build_Info( + sealed case class Job_Info( job_name: String, timestamp: Long, output: URL, session_logs: List[(String, URL)]) { - def read_output(): String = Url.read(output) - def read_log(full_stats: Boolean, name: String): Build.Log_Info = - Build.parse_log(full_stats, - session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") + def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) + def read_log(name: String, full: Boolean): Build_Log.Session_Info = + { + val text = + session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" + Build_Log.Log_File(name, text).parse_session_info(name, full) + } } - def build_job_builds(job_name: String): List[Build_Info] = + def build_job_builds(job_name: String): List[Job_Info] = { val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") @@ -68,7 +71,7 @@ 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)) - Build_Info(job_name, timestamp, output, session_logs) + Job_Info(job_name, timestamp, output, session_logs) } } } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Thu Oct 06 13:34:00 2016 +0200 @@ -7,7 +7,7 @@ package isabelle -import java.time._ +import java.time.{Instant, ZoneId} import java.time.format.DateTimeFormatter import java.util.{Properties => JProperties} diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/ml_statistics.scala --- a/src/Pure/Tools/ml_statistics.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/ml_statistics.scala Thu Oct 06 13:34:00 2016 +0200 @@ -22,11 +22,11 @@ final case class Entry(time: Double, data: Map[String, Double]) - def apply(name: String, stats: List[Properties.T]): ML_Statistics = - new ML_Statistics(name, stats) + def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics = + new ML_Statistics(session_name, ml_statistics) - def apply(info: Build.Log_Info): ML_Statistics = - apply(info.name, info.stats) + def apply(info: Build_Log.Session_Info): ML_Statistics = + apply(info.session_name, info.ml_statistics) val empty = apply("", Nil) @@ -59,26 +59,26 @@ time_fields, speed_fields) } -final class ML_Statistics private(val name: String, val stats: List[Properties.T]) +final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T]) { val Now = new Properties.Double("now") def now(props: Properties.T): Double = Now.unapply(props).get - require(stats.forall(props => Now.unapply(props).isDefined)) + require(ml_statistics.forall(props => Now.unapply(props).isDefined)) - val time_start = if (stats.isEmpty) 0.0 else now(stats.head) - val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start + val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) + val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start val fields: Set[String] = SortedSet.empty[String] ++ - (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name) + (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name) yield x) val content: List[ML_Statistics.Entry] = { var last_edge = Map.empty[String, (Double, Double, Double)] val result = new mutable.ListBuffer[ML_Statistics.Entry] - for (props <- stats) { + for (props <- ml_statistics) { val time = now(props) - time_start require(time >= 0.0) @@ -135,7 +135,7 @@ GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() - title = name + title = session_name contents = Component.wrap(new ChartPanel(c)) visible = true } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/Tools/task_statistics.scala --- a/src/Pure/Tools/task_statistics.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/Tools/task_statistics.scala Thu Oct 06 13:34:00 2016 +0200 @@ -17,22 +17,23 @@ object Task_Statistics { - def apply(name: String, tasks: List[Properties.T]): Task_Statistics = - new Task_Statistics(name, tasks) + def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics = + new Task_Statistics(session_name, task_statistics) - def apply(info: Build.Log_Info): Task_Statistics = - apply(info.name, info.tasks) + def apply(info: Build_Log.Session_Info): Task_Statistics = + apply(info.session_name, info.task_statistics) } -final class Task_Statistics private(val name: String, val tasks: List[Properties.T]) +final class Task_Statistics private( + val session_name: String, val task_statistics: List[Properties.T]) { private val Task_Name = new Properties.String("task_name") private val Run = new Properties.Int("run") def chart(bins: Int = 100): JFreeChart = { - val values = new Array[Double](tasks.length) - for ((Run(x), i) <- tasks.iterator.zipWithIndex) + val values = new Array[Double](task_statistics.length) + for ((Run(x), i) <- task_statistics.iterator.zipWithIndex) values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000) val data = new HistogramDataset @@ -54,7 +55,7 @@ GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() - title = name + title = session_name contents = Component.wrap(new ChartPanel(chart(bins))) visible = true } diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/build-jars --- a/src/Pure/build-jars Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/build-jars Thu Oct 06 13:34:00 2016 +0200 @@ -27,6 +27,7 @@ General/antiquote.scala General/bytes.scala General/completion.scala + General/date.scala General/exn.scala General/file.scala General/graph.scala @@ -107,6 +108,8 @@ 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 diff -r 6855c2f7aa6a -r 3a506cb576d3 src/Pure/library.scala --- a/src/Pure/library.scala Thu Oct 06 13:33:26 2016 +0200 +++ b/src/Pure/library.scala Thu Oct 06 13:34:00 2016 +0200 @@ -130,6 +130,9 @@ else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s + def trim_split_lines(s: String): List[String] = + split_lines(trim_line(s)).map(trim_line(_)) + /* quote */