merged
authorwenzelm
Thu, 06 Oct 2016 11:27:28 +0200
changeset 64066 f3ac9153bc0d
parent 64061 b8f8fe506585 (current diff)
parent 64065 2c5039363ea3 (diff)
child 64067 3a506cb576d3
child 64068 666c7475f4f7
merged
--- a/.hgtags	Wed Oct 05 21:27:21 2016 +0200
+++ b/.hgtags	Thu Oct 06 11:27:28 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 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/bin/isabelle_java	Thu Oct 06 11:27:28 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 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.scala	Thu Oct 06 11:27:28 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 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/General/mercurial.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/General/time.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/System/process_result.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/System/progress.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/build.scala	Thu Oct 06 11:27:28 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 11:27:28 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 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/ci_api.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/ml_statistics.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/Tools/task_statistics.scala	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/build-jars	Thu Oct 06 11:27:28 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	Wed Oct 05 21:27:21 2016 +0200
+++ b/src/Pure/library.scala	Thu Oct 06 11:27:28 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 */