--- 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
--- /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 "$@"
--- 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
--- /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)
--- 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)
}
}
--- /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()
+}
--- 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
--- 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)
}
--- 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
}
--- 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
}
--- 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"
--- 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)
}
--- /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)
+ })
+ }
+ }
+}
--- /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)
+ }
+}
--- 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</ul>\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(", ", ", ")")
-}
--- 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)
}
}
}
--- 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}
--- 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
}
--- 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
}
--- 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
--- 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 */