clarified files;
authorwenzelm
Wed Oct 12 09:38:20 2016 +0200 (2016-10-12)
changeset 641601eea419fab65
parent 64159 fe8f8f88a1d7
child 64161 2b1128e95dfb
clarified files;
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/ci_api.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_api.scala
src/Pure/Tools/ci_profile.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Admin/build_history.scala	Wed Oct 12 09:38:20 2016 +0200
     1.3 @@ -0,0 +1,388 @@
     1.4 +/*  Title:      Pure/Admin/build_history.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Build other history versions.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile}
    1.14 +import java.time.format.DateTimeFormatter
    1.15 +import java.util.Locale
    1.16 +
    1.17 +
    1.18 +object Build_History
    1.19 +{
    1.20 +  /* log files */
    1.21 +
    1.22 +  val BUILD_HISTORY = "build_history"
    1.23 +  val META_INFO_MARKER = "\fmeta_info = "
    1.24 +
    1.25 +
    1.26 +
    1.27 +  /** other Isabelle environment **/
    1.28 +
    1.29 +  private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    1.30 +  {
    1.31 +    other_isabelle =>
    1.32 +
    1.33 +
    1.34 +    /* static system */
    1.35 +
    1.36 +    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    1.37 +      Isabelle_System.bash(
    1.38 +        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    1.39 +        env = null, cwd = isabelle_home.file, redirect = redirect,
    1.40 +        progress_stdout = progress.echo_if(echo, _),
    1.41 +        progress_stderr = progress.echo_if(echo, _))
    1.42 +
    1.43 +    def copy_dir(dir1: Path, dir2: Path): Unit =
    1.44 +      bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
    1.45 +
    1.46 +    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    1.47 +      bash("bin/isabelle " + cmdline, redirect, echo)
    1.48 +
    1.49 +    def resolve_components(echo: Boolean): Unit =
    1.50 +      other_isabelle("components -a", redirect = true, echo = echo).check
    1.51 +
    1.52 +    val isabelle_home_user: Path =
    1.53 +      Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    1.54 +
    1.55 +    val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    1.56 +    val log_dir: Path = isabelle_home_user + Path.explode("log")
    1.57 +
    1.58 +
    1.59 +    /* reset settings */
    1.60 +
    1.61 +    def reset_settings(components_base: String, nonfree: Boolean)
    1.62 +    {
    1.63 +      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    1.64 +        error("Cannot proceed with existing user settings file: " + etc_settings)
    1.65 +
    1.66 +      Isabelle_System.mkdirs(etc_settings.dir)
    1.67 +      File.write(etc_settings,
    1.68 +        "# generated by Isabelle " + Date.now() + "\n" +
    1.69 +        "#-*- shell-script -*- :mode=shellscript:\n")
    1.70 +
    1.71 +      val component_settings =
    1.72 +      {
    1.73 +        val components_base_path =
    1.74 +          if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    1.75 +          else Path.explode(components_base).expand
    1.76 +
    1.77 +        val catalogs =
    1.78 +          if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
    1.79 +
    1.80 +        catalogs.map(catalog =>
    1.81 +          "init_components " + File.bash_path(components_base_path) +
    1.82 +            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
    1.83 +      }
    1.84 +      File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
    1.85 +    }
    1.86 +
    1.87 +
    1.88 +    /* augment settings */
    1.89 +
    1.90 +    def augment_settings(
    1.91 +      threads: Int,
    1.92 +      arch_64: Boolean = false,
    1.93 +      heap: Int = default_heap,
    1.94 +      max_heap: Option[Int] = None,
    1.95 +      more_settings: List[String]): String =
    1.96 +    {
    1.97 +      val (ml_platform, ml_settings) =
    1.98 +      {
    1.99 +        val windows_32 = "x86-windows"
   1.100 +        val windows_64 = "x86_64-windows"
   1.101 +        val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
   1.102 +        val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
   1.103 +        val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
   1.104 +
   1.105 +        val polyml_home =
   1.106 +          try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
   1.107 +          catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
   1.108 +
   1.109 +        def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
   1.110 +
   1.111 +        def err(platform: String): Nothing =
   1.112 +          error("Platform " + platform + " unavailable on this machine")
   1.113 +
   1.114 +        def check_dir(platform: String): Boolean =
   1.115 +          platform != "" && ml_home(platform).is_dir
   1.116 +
   1.117 +        val ml_platform =
   1.118 +          if (Platform.is_windows && arch_64) {
   1.119 +            if (check_dir(windows_64)) windows_64 else err(windows_64)
   1.120 +          }
   1.121 +          else if (Platform.is_windows && !arch_64) {
   1.122 +            if (check_dir(windows_32)) windows_32
   1.123 +            else platform_32  // x86-cygwin
   1.124 +          }
   1.125 +          else {
   1.126 +            val (platform, platform_name) =
   1.127 +              if (arch_64) (platform_64, "x86_64-" + platform_family)
   1.128 +              else (platform_32, "x86-" + platform_family)
   1.129 +            if (check_dir(platform)) platform else err(platform_name)
   1.130 +          }
   1.131 +
   1.132 +        val ml_options =
   1.133 +          "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
   1.134 +          " --gcthreads " + threads +
   1.135 +          (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
   1.136 +
   1.137 +        (ml_platform,
   1.138 +          List(
   1.139 +            "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
   1.140 +            "ML_PLATFORM=" + quote(ml_platform),
   1.141 +            "ML_OPTIONS=" + quote(ml_options)))
   1.142 +      }
   1.143 +
   1.144 +      val thread_settings =
   1.145 +        List(
   1.146 +          "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
   1.147 +          "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
   1.148 +
   1.149 +      val settings =
   1.150 +        List(ml_settings, thread_settings) :::
   1.151 +          (if (more_settings.isEmpty) Nil else List(more_settings))
   1.152 +
   1.153 +      File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
   1.154 +
   1.155 +      ml_platform
   1.156 +    }
   1.157 +  }
   1.158 +
   1.159 +
   1.160 +
   1.161 +  /** build_history **/
   1.162 +
   1.163 +  private val default_rev = "tip"
   1.164 +  private val default_threads = 1
   1.165 +  private val default_heap = 1000
   1.166 +  private val default_isabelle_identifier = "build_history"
   1.167 +
   1.168 +  def build_history(
   1.169 +    progress: Progress,
   1.170 +    hg: Mercurial.Repository,
   1.171 +    rev: String = default_rev,
   1.172 +    isabelle_identifier: String = default_isabelle_identifier,
   1.173 +    components_base: String = "",
   1.174 +    fresh: Boolean = false,
   1.175 +    nonfree: Boolean = false,
   1.176 +    multicore_base: Boolean = false,
   1.177 +    threads_list: List[Int] = List(default_threads),
   1.178 +    arch_64: Boolean = false,
   1.179 +    heap: Int = default_heap,
   1.180 +    max_heap: Option[Int] = None,
   1.181 +    more_settings: List[String] = Nil,
   1.182 +    verbose: Boolean = false,
   1.183 +    build_args: List[String] = Nil): List[Process_Result] =
   1.184 +  {
   1.185 +    /* sanity checks */
   1.186 +
   1.187 +    if (File.eq(Path.explode("~~").file, hg.root.file))
   1.188 +      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
   1.189 +
   1.190 +    for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
   1.191 +
   1.192 +    if (heap < 100) error("Bad heap value < 100: " + heap)
   1.193 +
   1.194 +    if (max_heap.isDefined && max_heap.get < heap)
   1.195 +      error("Bad max_heap value < heap: " + max_heap.get)
   1.196 +
   1.197 +    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
   1.198 +      case null | "" =>
   1.199 +      case _ => error("Cannot run build_history within existing Isabelle settings environment")
   1.200 +    }
   1.201 +
   1.202 +
   1.203 +    /* init repository */
   1.204 +
   1.205 +    hg.update(rev = rev, clean = true)
   1.206 +    progress.echo_if(verbose, hg.log(rev, options = "-l1"))
   1.207 +
   1.208 +    val isabelle_version = hg.identify(rev, options = "-i")
   1.209 +    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
   1.210 +
   1.211 +
   1.212 +    /* main */
   1.213 +
   1.214 +    val build_history_date = Date.now()
   1.215 +    val build_host = Isabelle_System.hostname()
   1.216 +
   1.217 +    var first_build = true
   1.218 +    for (threads <- threads_list) yield
   1.219 +    {
   1.220 +      /* init settings */
   1.221 +
   1.222 +      other_isabelle.reset_settings(components_base, nonfree)
   1.223 +      other_isabelle.resolve_components(verbose)
   1.224 +      val ml_platform =
   1.225 +        other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
   1.226 +
   1.227 +      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   1.228 +      val isabelle_output_log = isabelle_output + Path.explode("log")
   1.229 +      val isabelle_base_log = isabelle_output + Path.explode("../base_log")
   1.230 +
   1.231 +      if (first_build) {
   1.232 +        other_isabelle.resolve_components(verbose)
   1.233 +        other_isabelle.bash(
   1.234 +          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
   1.235 +            "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
   1.236 +          redirect = true, echo = verbose).check
   1.237 +
   1.238 +        Isabelle_System.rm_tree(isabelle_base_log.file)
   1.239 +      }
   1.240 +
   1.241 +      Isabelle_System.rm_tree(isabelle_output.file)
   1.242 +      Isabelle_System.mkdirs(isabelle_output)
   1.243 +
   1.244 +
   1.245 +      /* build */
   1.246 +
   1.247 +      if (multicore_base && !first_build && isabelle_base_log.is_dir)
   1.248 +        other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
   1.249 +
   1.250 +      val build_start = Date.now()
   1.251 +      val res =
   1.252 +        other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
   1.253 +      val build_end = Date.now()
   1.254 +
   1.255 +
   1.256 +      /* output log */
   1.257 +
   1.258 +      val log_path =
   1.259 +        other_isabelle.log_dir +
   1.260 +          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
   1.261 +
   1.262 +      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
   1.263 +
   1.264 +      val meta_info =
   1.265 +        List(Build_Log.Field.build_engine -> BUILD_HISTORY,
   1.266 +          Build_Log.Field.build_host -> build_host,
   1.267 +          Build_Log.Field.build_start -> Build_Log.print_date(build_start),
   1.268 +          Build_Log.Field.build_end -> Build_Log.print_date(build_end),
   1.269 +          Build_Log.Field.isabelle_version -> isabelle_version)
   1.270 +
   1.271 +      val ml_statistics =
   1.272 +        build_info.finished_sessions.flatMap(session_name =>
   1.273 +          {
   1.274 +            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
   1.275 +            if (session_log.is_file) {
   1.276 +              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
   1.277 +                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
   1.278 +            }
   1.279 +            else Nil
   1.280 +          })
   1.281 +
   1.282 +      val heap_sizes =
   1.283 +        build_info.finished_sessions.flatMap(session_name =>
   1.284 +          {
   1.285 +            val heap = isabelle_output + Path.explode(session_name)
   1.286 +            if (heap.is_file)
   1.287 +              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
   1.288 +            else None
   1.289 +          })
   1.290 +
   1.291 +      Isabelle_System.mkdirs(log_path.dir)
   1.292 +      File.write_gzip(log_path,
   1.293 +        Library.terminate_lines(
   1.294 +          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
   1.295 +          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
   1.296 +          heap_sizes))
   1.297 +
   1.298 +      Output.writeln(log_path.implode, stdout = true)
   1.299 +
   1.300 +
   1.301 +      /* next build */
   1.302 +
   1.303 +      if (multicore_base && first_build && isabelle_output_log.is_dir)
   1.304 +        other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
   1.305 +
   1.306 +      first_build = false
   1.307 +
   1.308 +      res
   1.309 +    }
   1.310 +  }
   1.311 +
   1.312 +
   1.313 +  /* command line entry point */
   1.314 +
   1.315 +  def main(args: Array[String])
   1.316 +  {
   1.317 +    Command_Line.tool0 {
   1.318 +      var multicore_base = false
   1.319 +      var components_base = ""
   1.320 +      var heap: Option[Int] = None
   1.321 +      var max_heap: Option[Int] = None
   1.322 +      var threads_list = List(default_threads)
   1.323 +      var isabelle_identifier = default_isabelle_identifier
   1.324 +      var more_settings: List[String] = Nil
   1.325 +      var fresh = false
   1.326 +      var arch_64 = false
   1.327 +      var nonfree = false
   1.328 +      var rev = default_rev
   1.329 +      var verbose = false
   1.330 +
   1.331 +      val getopts = Getopts("""
   1.332 +Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
   1.333 +
   1.334 +  Options are:
   1.335 +    -B           first multicore build serves as base for scheduling information
   1.336 +    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
   1.337 +    -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
   1.338 +    -M THREADS   multicore configurations (comma-separated list, default: """ + default_threads + """)
   1.339 +    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
   1.340 +    -U SIZE      maximal ML heap in MB (default: unbounded)
   1.341 +    -e TEXT      additional text for generated etc/settings
   1.342 +    -f           fresh build of Isabelle/Scala components (recommended)
   1.343 +    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   1.344 +    -n           include nonfree components
   1.345 +    -r REV       update to revision (default: """ + default_rev + """)
   1.346 +    -v           verbose
   1.347 +
   1.348 +  Build Isabelle sessions from the history of another REPOSITORY clone,
   1.349 +  passing ARGS directly to its isabelle build tool.
   1.350 +""",
   1.351 +        "B" -> (_ => multicore_base = true),
   1.352 +        "C:" -> (arg => components_base = arg),
   1.353 +        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
   1.354 +        "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
   1.355 +        "N:" -> (arg => isabelle_identifier = arg),
   1.356 +        "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
   1.357 +        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
   1.358 +        "f" -> (_ => fresh = true),
   1.359 +        "m:" ->
   1.360 +          {
   1.361 +            case "32" | "x86" => arch_64 = false
   1.362 +            case "64" | "x86_64" => arch_64 = true
   1.363 +            case bad => error("Bad processor architecture: " + quote(bad))
   1.364 +          },
   1.365 +        "n" -> (_ => nonfree = true),
   1.366 +        "r:" -> (arg => rev = arg),
   1.367 +        "v" -> (_ => verbose = true))
   1.368 +
   1.369 +      val more_args = getopts(args)
   1.370 +      val (root, build_args) =
   1.371 +        more_args match {
   1.372 +          case root :: build_args => (root, build_args)
   1.373 +          case _ => getopts.usage()
   1.374 +        }
   1.375 +
   1.376 +      using(Mercurial.open_repository(Path.explode(root)))(hg =>
   1.377 +        {
   1.378 +          val progress = new Console_Progress(stderr = true)
   1.379 +          val results =
   1.380 +            build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
   1.381 +              components_base = components_base, fresh = fresh, nonfree = nonfree,
   1.382 +              multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
   1.383 +              heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   1.384 +              max_heap = max_heap, more_settings = more_settings, verbose = verbose,
   1.385 +              build_args = build_args)
   1.386 +          val rc = (0 /: results) { case (rc, res) => rc max res.rc }
   1.387 +          if (rc != 0) sys.exit(rc)
   1.388 +        })
   1.389 +    }
   1.390 +  }
   1.391 +}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Admin/build_log.scala	Wed Oct 12 09:38:20 2016 +0200
     2.3 @@ -0,0 +1,548 @@
     2.4 +/*  Title:      Pure/Admin/build_log.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Build log parsing for current and historic formats.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.io.{File => JFile}
    2.14 +import java.time.ZoneId
    2.15 +import java.time.format.{DateTimeFormatter, DateTimeParseException}
    2.16 +import java.util.Locale
    2.17 +
    2.18 +import scala.collection.mutable
    2.19 +import scala.util.matching.Regex
    2.20 +
    2.21 +
    2.22 +object Build_Log
    2.23 +{
    2.24 +  /** directory content **/
    2.25 +
    2.26 +  /* file names */
    2.27 +
    2.28 +  def log_date(date: Date): String =
    2.29 +    String.format(Locale.ROOT, "%s.%05d",
    2.30 +      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
    2.31 +      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
    2.32 +
    2.33 +  def log_path(engine: String, date: Date, more: String*): Path =
    2.34 +    Path.explode(date.rep.getYear.toString) +
    2.35 +      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
    2.36 +
    2.37 +
    2.38 +  /* log file collections */
    2.39 +
    2.40 +  def is_log(file: JFile): Boolean =
    2.41 +    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
    2.42 +
    2.43 +  def isatest_files(dir: Path): List[JFile] =
    2.44 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
    2.45 +
    2.46 +  def afp_test_files(dir: Path): List[JFile] =
    2.47 +    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
    2.48 +
    2.49 +
    2.50 +
    2.51 +  /** settings **/
    2.52 +
    2.53 +  object Settings
    2.54 +  {
    2.55 +    val build_settings = List("ISABELLE_BUILD_OPTIONS")
    2.56 +    val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    2.57 +    val all_settings = build_settings ::: ml_settings
    2.58 +
    2.59 +    type Entry = (String, String)
    2.60 +    type T = List[Entry]
    2.61 +
    2.62 +    object Entry
    2.63 +    {
    2.64 +      def unapply(s: String): Option[Entry] =
    2.65 +        s.indexOf('=') match {
    2.66 +          case -1 => None
    2.67 +          case i =>
    2.68 +            val a = s.substring(0, i)
    2.69 +            val b = Library.perhaps_unquote(s.substring(i + 1))
    2.70 +            Some((a, b))
    2.71 +        }
    2.72 +      def apply(a: String, b: String): String = a + "=" + quote(b)
    2.73 +      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    2.74 +    }
    2.75 +
    2.76 +    def show(): String =
    2.77 +      cat_lines(
    2.78 +        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    2.79 +  }
    2.80 +
    2.81 +
    2.82 +
    2.83 +  /** log file **/
    2.84 +
    2.85 +  def print_date(date: Date): String = Log_File.Date_Format(date)
    2.86 +
    2.87 +  object Log_File
    2.88 +  {
    2.89 +    def apply(name: String, lines: List[String]): Log_File =
    2.90 +      new Log_File(name, lines)
    2.91 +
    2.92 +    def apply(name: String, text: String): Log_File =
    2.93 +      Log_File(name, Library.trim_split_lines(text))
    2.94 +
    2.95 +    def apply(file: JFile): Log_File =
    2.96 +    {
    2.97 +      val name = file.getName
    2.98 +      val (base_name, text) =
    2.99 +        Library.try_unsuffix(".gz", name) match {
   2.100 +          case Some(base_name) => (base_name, File.read_gzip(file))
   2.101 +          case None =>
   2.102 +            Library.try_unsuffix(".xz", name) match {
   2.103 +              case Some(base_name) => (base_name, File.read_xz(file))
   2.104 +              case None => (name, File.read(file))
   2.105 +            }
   2.106 +          }
   2.107 +      apply(base_name, text)
   2.108 +    }
   2.109 +
   2.110 +    def apply(path: Path): Log_File = apply(path.file)
   2.111 +
   2.112 +
   2.113 +    /* date format */
   2.114 +
   2.115 +    val Date_Format =
   2.116 +    {
   2.117 +      val fmts =
   2.118 +        Date.Formatter.variants(
   2.119 +          List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
   2.120 +          List(Locale.ENGLISH, Locale.GERMAN)) :::
   2.121 +        List(
   2.122 +          DateTimeFormatter.RFC_1123_DATE_TIME,
   2.123 +          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
   2.124 +
   2.125 +      def tune_timezone(s: String): String =
   2.126 +        s match {
   2.127 +          case "CET" | "MET" => "GMT+1"
   2.128 +          case "CEST" | "MEST" => "GMT+2"
   2.129 +          case "EST" => "Europe/Berlin"
   2.130 +          case _ => s
   2.131 +        }
   2.132 +      def tune_weekday(s: String): String =
   2.133 +        s match {
   2.134 +          case "Die" => "Di"
   2.135 +          case "Mit" => "Mi"
   2.136 +          case "Don" => "Do"
   2.137 +          case "Fre" => "Fr"
   2.138 +          case "Sam" => "Sa"
   2.139 +          case "Son" => "So"
   2.140 +          case _ => s
   2.141 +        }
   2.142 +
   2.143 +      def tune(s: String): String =
   2.144 +        Word.implode(
   2.145 +          Word.explode(s) match {
   2.146 +            case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
   2.147 +            case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
   2.148 +            case Nil => Nil
   2.149 +          }
   2.150 +        )
   2.151 +
   2.152 +      Date.Format.make(fmts, tune)
   2.153 +    }
   2.154 +
   2.155 +
   2.156 +    /* inlined content */
   2.157 +
   2.158 +    def print_props(marker: String, props: Properties.T): String =
   2.159 +      marker + YXML.string_of_body(XML.Encode.properties(props))
   2.160 +  }
   2.161 +
   2.162 +  class Log_File private(val name: String, val lines: List[String])
   2.163 +  {
   2.164 +    log_file =>
   2.165 +
   2.166 +    override def toString: String = name
   2.167 +
   2.168 +    def text: String = cat_lines(lines)
   2.169 +
   2.170 +    def err(msg: String): Nothing =
   2.171 +      error("Error in log file " + quote(name) + ": " + msg)
   2.172 +
   2.173 +
   2.174 +    /* date format */
   2.175 +
   2.176 +    object Strict_Date
   2.177 +    {
   2.178 +      def unapply(s: String): Some[Date] =
   2.179 +        try { Some(Log_File.Date_Format.parse(s)) }
   2.180 +        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
   2.181 +    }
   2.182 +
   2.183 +
   2.184 +    /* inlined content */
   2.185 +
   2.186 +    def find[A](f: String => Option[A]): Option[A] =
   2.187 +      lines.iterator.map(f).find(_.isDefined).map(_.get)
   2.188 +
   2.189 +    def find_match(regex: Regex): Option[String] =
   2.190 +      lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
   2.191 +        map(res => res.get.head)
   2.192 +
   2.193 +
   2.194 +    /* settings */
   2.195 +
   2.196 +    def get_setting(a: String): Option[Settings.Entry] =
   2.197 +      lines.find(_.startsWith(a + "=")) match {
   2.198 +        case Some(line) => Settings.Entry.unapply(line)
   2.199 +        case None => None
   2.200 +      }
   2.201 +
   2.202 +    def get_settings(as: List[String]): Settings.T =
   2.203 +      for { a <- as; entry <- get_setting(a) } yield entry
   2.204 +
   2.205 +
   2.206 +    /* properties (YXML) */
   2.207 +
   2.208 +    val xml_cache = new XML.Cache()
   2.209 +
   2.210 +    def parse_props(text: String): Properties.T =
   2.211 +      xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
   2.212 +
   2.213 +    def filter_props(marker: String): List[Properties.T] =
   2.214 +      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
   2.215 +
   2.216 +    def find_line(marker: String): Option[String] =
   2.217 +      find(Library.try_unprefix(marker, _))
   2.218 +
   2.219 +    def find_props(marker: String): Option[Properties.T] =
   2.220 +      find_line(marker).map(parse_props(_))
   2.221 +
   2.222 +
   2.223 +    /* parse various formats */
   2.224 +
   2.225 +    def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
   2.226 +
   2.227 +    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   2.228 +
   2.229 +    def parse_session_info(
   2.230 +        default_name: String = "",
   2.231 +        command_timings: Boolean = false,
   2.232 +        ml_statistics: Boolean = false,
   2.233 +        task_statistics: Boolean = false): Session_Info =
   2.234 +      Build_Log.parse_session_info(
   2.235 +        log_file, default_name, command_timings, ml_statistics, task_statistics)
   2.236 +  }
   2.237 +
   2.238 +
   2.239 +
   2.240 +  /** meta info **/
   2.241 +
   2.242 +  object Field
   2.243 +  {
   2.244 +    val build_engine = "build_engine"
   2.245 +    val build_host = "build_host"
   2.246 +    val build_start = "build_start"
   2.247 +    val build_end = "build_end"
   2.248 +    val isabelle_version = "isabelle_version"
   2.249 +    val afp_version = "afp_version"
   2.250 +  }
   2.251 +
   2.252 +  object Meta_Info
   2.253 +  {
   2.254 +    val empty: Meta_Info = Meta_Info(Nil, Nil)
   2.255 +  }
   2.256 +
   2.257 +  sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
   2.258 +  {
   2.259 +    def is_empty: Boolean = props.isEmpty && settings.isEmpty
   2.260 +  }
   2.261 +
   2.262 +  object Isatest
   2.263 +  {
   2.264 +    val engine = "isatest"
   2.265 +    val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
   2.266 +    val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
   2.267 +    val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
   2.268 +    val No_AFP_Version = new Regex("""$.""")
   2.269 +  }
   2.270 +
   2.271 +  object AFP_Test
   2.272 +  {
   2.273 +    val engine = "afp-test"
   2.274 +    val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   2.275 +    val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   2.276 +    val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   2.277 +    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   2.278 +    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   2.279 +    val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
   2.280 +  }
   2.281 +
   2.282 +  object Jenkins
   2.283 +  {
   2.284 +    val engine = "jenkins"
   2.285 +    val Start = new Regex("""^Started .*$""")
   2.286 +    val Start_Date = new Regex("""^Build started at (.+)$""")
   2.287 +    val No_End = new Regex("""$.""")
   2.288 +    val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
   2.289 +    val AFP_Version = new Regex("""^AFP id (\S+)$""")
   2.290 +    val CONFIGURATION = "=== CONFIGURATION ==="
   2.291 +    val BUILD = "=== BUILD ==="
   2.292 +    val FINISHED = "Finished: "
   2.293 +  }
   2.294 +
   2.295 +  private def parse_meta_info(log_file: Log_File): Meta_Info =
   2.296 +  {
   2.297 +    def parse(engine: String, host: String, start: Date,
   2.298 +      End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
   2.299 +    {
   2.300 +      val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
   2.301 +      val build_host = if (host == "") Nil else List(Field.build_host -> host)
   2.302 +
   2.303 +      val start_date = List(Field.build_start -> start.toString)
   2.304 +      val end_date =
   2.305 +        log_file.lines.last match {
   2.306 +          case End(log_file.Strict_Date(end_date)) =>
   2.307 +            List(Field.build_end -> end_date.toString)
   2.308 +          case _ => Nil
   2.309 +        }
   2.310 +
   2.311 +      val isabelle_version =
   2.312 +        log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
   2.313 +      val afp_version =
   2.314 +        log_file.find_match(AFP_Version).map(Field.afp_version -> _)
   2.315 +
   2.316 +      Meta_Info(build_engine ::: build_host :::
   2.317 +          start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
   2.318 +        log_file.get_settings(Settings.all_settings))
   2.319 +    }
   2.320 +
   2.321 +    log_file.lines match {
   2.322 +      case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
   2.323 +        Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
   2.324 +          log_file.get_settings(Settings.all_settings))
   2.325 +
   2.326 +      case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
   2.327 +        parse(Isatest.engine, host, start, Isatest.End,
   2.328 +          Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   2.329 +
   2.330 +      case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
   2.331 +        parse(AFP_Test.engine, host, start, AFP_Test.End,
   2.332 +          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   2.333 +
   2.334 +      case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
   2.335 +        parse(AFP_Test.engine, "", start, AFP_Test.End,
   2.336 +          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   2.337 +
   2.338 +      case Jenkins.Start() :: _
   2.339 +      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
   2.340 +         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
   2.341 +        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
   2.342 +          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
   2.343 +            parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
   2.344 +              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
   2.345 +          case _ => Meta_Info.empty
   2.346 +        }
   2.347 +
   2.348 +      case line :: _ if line.startsWith("\0") => Meta_Info.empty
   2.349 +      case List(Isatest.End(_)) => Meta_Info.empty
   2.350 +      case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
   2.351 +      case Nil => Meta_Info.empty
   2.352 +
   2.353 +      case _ => log_file.err("cannot detect log file format")
   2.354 +    }
   2.355 +  }
   2.356 +
   2.357 +
   2.358 +
   2.359 +  /** build info: produced by isabelle build or build_history **/
   2.360 +
   2.361 +  val ML_STATISTICS_MARKER = "\fML_statistics = "
   2.362 +  val SESSION_NAME = "session_name"
   2.363 +
   2.364 +  object Session_Status extends Enumeration
   2.365 +  {
   2.366 +    val EXISTING = Value("existing")
   2.367 +    val FINISHED = Value("finished")
   2.368 +    val FAILED = Value("failed")
   2.369 +    val CANCELLED = Value("cancelled")
   2.370 +  }
   2.371 +
   2.372 +  sealed case class Session_Entry(
   2.373 +    chapter: String,
   2.374 +    groups: List[String],
   2.375 +    threads: Option[Int],
   2.376 +    timing: Timing,
   2.377 +    ml_timing: Timing,
   2.378 +    ml_statistics: List[Properties.T],
   2.379 +    heap_size: Option[Long],
   2.380 +    status: Session_Status.Value)
   2.381 +  {
   2.382 +    def finished: Boolean = status == Session_Status.FINISHED
   2.383 +  }
   2.384 +
   2.385 +  sealed case class Build_Info(sessions: Map[String, Session_Entry])
   2.386 +  {
   2.387 +    def session(name: String): Session_Entry = sessions(name)
   2.388 +    def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   2.389 +
   2.390 +    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   2.391 +      get_session(name) match {
   2.392 +        case Some(entry) => f(entry)
   2.393 +        case None => x
   2.394 +      }
   2.395 +
   2.396 +    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
   2.397 +    def finished(name: String): Boolean = get_default(name, _.finished, false)
   2.398 +    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   2.399 +    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   2.400 +  }
   2.401 +
   2.402 +  private def parse_build_info(log_file: Log_File): Build_Info =
   2.403 +  {
   2.404 +    object Chapter_Name
   2.405 +    {
   2.406 +      def unapply(s: String): Some[(String, String)] =
   2.407 +        space_explode('/', s) match {
   2.408 +          case List(chapter, name) => Some((chapter, name))
   2.409 +          case _ => Some(("", s))
   2.410 +        }
   2.411 +    }
   2.412 +
   2.413 +    val Session_No_Groups = new Regex("""^Session (\S+)$""")
   2.414 +    val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   2.415 +    val Session_Finished1 =
   2.416 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   2.417 +    val Session_Finished2 =
   2.418 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   2.419 +    val Session_Timing =
   2.420 +      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   2.421 +    val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   2.422 +    val Session_Failed = new Regex("""^(\S+) FAILED""")
   2.423 +    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   2.424 +    val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
   2.425 +
   2.426 +    var chapter = Map.empty[String, String]
   2.427 +    var groups = Map.empty[String, List[String]]
   2.428 +    var threads = Map.empty[String, Int]
   2.429 +    var timing = Map.empty[String, Timing]
   2.430 +    var ml_timing = Map.empty[String, Timing]
   2.431 +    var started = Set.empty[String]
   2.432 +    var failed = Set.empty[String]
   2.433 +    var cancelled = Set.empty[String]
   2.434 +    var ml_statistics = Map.empty[String, List[Properties.T]]
   2.435 +    var heap_sizes = Map.empty[String, Long]
   2.436 +
   2.437 +    def all_sessions: Set[String] =
   2.438 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
   2.439 +      failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
   2.440 +
   2.441 +
   2.442 +    for (line <- log_file.lines) {
   2.443 +      line match {
   2.444 +        case Session_No_Groups(Chapter_Name(chapt, name)) =>
   2.445 +          chapter += (name -> chapt)
   2.446 +          groups += (name -> Nil)
   2.447 +
   2.448 +        case Session_Groups(Chapter_Name(chapt, name), grps) =>
   2.449 +          chapter += (name -> chapt)
   2.450 +          groups += (name -> Word.explode(grps))
   2.451 +
   2.452 +        case Session_Started(name) =>
   2.453 +          started += name
   2.454 +
   2.455 +        case Session_Finished1(name,
   2.456 +            Value.Int(e1), Value.Int(e2), Value.Int(e3),
   2.457 +            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   2.458 +          val elapsed = Time.hms(e1, e2, e3)
   2.459 +          val cpu = Time.hms(c1, c2, c3)
   2.460 +          timing += (name -> Timing(elapsed, cpu, Time.zero))
   2.461 +
   2.462 +        case Session_Finished2(name,
   2.463 +            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   2.464 +          val elapsed = Time.hms(e1, e2, e3)
   2.465 +          timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   2.466 +
   2.467 +        case Session_Timing(name,
   2.468 +            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   2.469 +          val elapsed = Time.seconds(e)
   2.470 +          val cpu = Time.seconds(c)
   2.471 +          val gc = Time.seconds(g)
   2.472 +          ml_timing += (name -> Timing(elapsed, cpu, gc))
   2.473 +          threads += (name -> t)
   2.474 +
   2.475 +        case Heap(name, Value.Long(size)) =>
   2.476 +          heap_sizes += (name -> size)
   2.477 +
   2.478 +        case _ if line.startsWith(ML_STATISTICS_MARKER) =>
   2.479 +          val (name, props) =
   2.480 +            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
   2.481 +              case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
   2.482 +              case _ => log_file.err("malformed ML_statistics " + quote(line))
   2.483 +            }
   2.484 +          ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
   2.485 +
   2.486 +        case _ =>
   2.487 +      }
   2.488 +    }
   2.489 +
   2.490 +    val sessions =
   2.491 +      Map(
   2.492 +        (for (name <- all_sessions.toList) yield {
   2.493 +          val status =
   2.494 +            if (failed(name)) Session_Status.FAILED
   2.495 +            else if (cancelled(name)) Session_Status.CANCELLED
   2.496 +            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   2.497 +              Session_Status.FINISHED
   2.498 +            else if (started(name)) Session_Status.FAILED
   2.499 +            else Session_Status.EXISTING
   2.500 +          val entry =
   2.501 +            Session_Entry(
   2.502 +              chapter.getOrElse(name, ""),
   2.503 +              groups.getOrElse(name, Nil),
   2.504 +              threads.get(name),
   2.505 +              timing.getOrElse(name, Timing.zero),
   2.506 +              ml_timing.getOrElse(name, Timing.zero),
   2.507 +              ml_statistics.getOrElse(name, Nil).reverse,
   2.508 +              heap_sizes.get(name),
   2.509 +              status)
   2.510 +          (name -> entry)
   2.511 +        }):_*)
   2.512 +    Build_Info(sessions)
   2.513 +  }
   2.514 +
   2.515 +
   2.516 +
   2.517 +  /** session info: produced by "isabelle build" **/
   2.518 +
   2.519 +  sealed case class Session_Info(
   2.520 +    session_name: String,
   2.521 +    session_timing: Properties.T,
   2.522 +    command_timings: List[Properties.T],
   2.523 +    ml_statistics: List[Properties.T],
   2.524 +    task_statistics: List[Properties.T])
   2.525 +
   2.526 +  private def parse_session_info(
   2.527 +    log_file: Log_File,
   2.528 +    default_name: String,
   2.529 +    command_timings: Boolean,
   2.530 +    ml_statistics: Boolean,
   2.531 +    task_statistics: Boolean): Session_Info =
   2.532 +  {
   2.533 +    val xml_cache = new XML.Cache()
   2.534 +
   2.535 +    val session_name =
   2.536 +      log_file.find_line("\fSession.name = ") match {
   2.537 +        case None => default_name
   2.538 +        case Some(name) if default_name == "" || default_name == name => name
   2.539 +        case Some(name) => log_file.err("log from different session " + quote(name))
   2.540 +      }
   2.541 +    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   2.542 +    val command_timings_ =
   2.543 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   2.544 +    val ml_statistics_ =
   2.545 +      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
   2.546 +    val task_statistics_ =
   2.547 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   2.548 +
   2.549 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   2.550 +  }
   2.551 +}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Admin/ci_api.scala	Wed Oct 12 09:38:20 2016 +0200
     3.3 @@ -0,0 +1,74 @@
     3.4 +/*  Title:      Pure/Admin/ci_api.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +API for Isabelle Jenkins continuous integration services.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +import java.net.URL
    3.14 +
    3.15 +import scala.util.matching.Regex
    3.16 +
    3.17 +
    3.18 +object CI_API
    3.19 +{
    3.20 +  /* CI service */
    3.21 +
    3.22 +  def root(): String =
    3.23 +    Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
    3.24 +
    3.25 +  def invoke(url: String, args: String*): Any =
    3.26 +  {
    3.27 +    val req = url + "/api/json?" + args.mkString("&")
    3.28 +    val result = Url.read(req)
    3.29 +    try { JSON.parse(result) }
    3.30 +    catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
    3.31 +  }
    3.32 +
    3.33 +
    3.34 +  /* build jobs */
    3.35 +
    3.36 +  def build_jobs(): List[String] =
    3.37 +    for {
    3.38 +      job <- JSON.array(invoke(root()), "jobs")
    3.39 +      _class <- JSON.string(job, "_class")
    3.40 +      if _class == "hudson.model.FreeStyleProject"
    3.41 +      name <- JSON.string(job, "name")
    3.42 +    } yield name
    3.43 +
    3.44 +  sealed case class Job_Info(
    3.45 +    job_name: String,
    3.46 +    timestamp: Long,
    3.47 +    output: URL,
    3.48 +    session_logs: List[(String, URL)])
    3.49 +  {
    3.50 +    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    3.51 +    def read_session_log(name: String): Build_Log.Log_File =
    3.52 +      Build_Log.Log_File(name,
    3.53 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    3.54 +  }
    3.55 +
    3.56 +  def build_job_builds(job_name: String): List[Job_Info] =
    3.57 +  {
    3.58 +    val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
    3.59 +
    3.60 +    for {
    3.61 +      build <- JSON.array(
    3.62 +        invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    3.63 +      number <- JSON.int(build, "number")
    3.64 +      timestamp <- JSON.long(build, "timestamp")
    3.65 +    } yield {
    3.66 +      val job_prefix = root() + "/job/" + job_name + "/" + number
    3.67 +      val output = Url(job_prefix + "/consoleText")
    3.68 +      val session_logs =
    3.69 +        for {
    3.70 +          artifact <- JSON.array(build, "artifacts")
    3.71 +          log_path <- JSON.string(artifact, "relativePath")
    3.72 +          session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
    3.73 +        } yield (session -> Url(job_prefix + "/artifact/" + log_path))
    3.74 +      Job_Info(job_name, timestamp, output, session_logs)
    3.75 +    }
    3.76 +  }
    3.77 +}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Admin/ci_profile.scala	Wed Oct 12 09:38:20 2016 +0200
     4.3 @@ -0,0 +1,149 @@
     4.4 +/*  Title:      Pure/Admin/ci_profile.scala
     4.5 +    Author:     Lars Hupel
     4.6 +
     4.7 +Build profile for continuous integration services.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +import java.time.{Instant, ZoneId}
    4.14 +import java.time.format.DateTimeFormatter
    4.15 +import java.util.{Properties => JProperties}
    4.16 +
    4.17 +
    4.18 +abstract class CI_Profile extends Isabelle_Tool.Body
    4.19 +{
    4.20 +  private def build(options: Options): (Build.Results, Time) =
    4.21 +  {
    4.22 +    val progress = new Console_Progress(verbose = true)
    4.23 +    val start_time = Time.now()
    4.24 +    val results = progress.interrupt_handler {
    4.25 +      Build.build_selection(
    4.26 +        options = options,
    4.27 +        progress = progress,
    4.28 +        clean_build = true,
    4.29 +        verbose = true,
    4.30 +        max_jobs = jobs,
    4.31 +        dirs = include,
    4.32 +        select_dirs = select,
    4.33 +        system_mode = true,
    4.34 +        selection = select_sessions _)
    4.35 +    }
    4.36 +    val end_time = Time.now()
    4.37 +    (results, end_time - start_time)
    4.38 +  }
    4.39 +
    4.40 +  private def load_properties(): JProperties =
    4.41 +  {
    4.42 +    val props = new JProperties()
    4.43 +    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
    4.44 +
    4.45 +    if (file_name != "")
    4.46 +    {
    4.47 +      val file = Path.explode(file_name).file
    4.48 +      if (file.exists())
    4.49 +        props.load(new java.io.FileReader(file))
    4.50 +      props
    4.51 +    }
    4.52 +    else
    4.53 +      props
    4.54 +  }
    4.55 +
    4.56 +  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
    4.57 +  {
    4.58 +    val timings = results.sessions.collect {
    4.59 +      case session if group.forall(results.info(session).groups.contains(_)) =>
    4.60 +        results(session).timing
    4.61 +    }
    4.62 +    (Timing.zero /: timings)(_ + _)
    4.63 +  }
    4.64 +
    4.65 +  private def with_documents(options: Options): Options =
    4.66 +  {
    4.67 +    if (documents)
    4.68 +      options
    4.69 +        .bool.update("browser_info", true)
    4.70 +        .string.update("document", "pdf")
    4.71 +        .string.update("document_variants", "document:outline=/proof,/ML")
    4.72 +    else
    4.73 +      options
    4.74 +  }
    4.75 +
    4.76 +
    4.77 +  final def hg_id(path: Path): String =
    4.78 +    Isabelle_System.hg("id -i", path.file).out
    4.79 +
    4.80 +  final def print_section(title: String): Unit =
    4.81 +    println(s"\n=== $title ===\n")
    4.82 +
    4.83 +
    4.84 +  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
    4.85 +  final val isabelle_id = hg_id(isabelle_home)
    4.86 +  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
    4.87 +
    4.88 +
    4.89 +  override final def apply(args: List[String]): Unit =
    4.90 +  {
    4.91 +    print_section("CONFIGURATION")
    4.92 +    println(Build_Log.Settings.show())
    4.93 +    val props = load_properties()
    4.94 +    System.getProperties().putAll(props)
    4.95 +
    4.96 +    val options =
    4.97 +      with_documents(Options.init())
    4.98 +        .int.update("parallel_proofs", 2)
    4.99 +        .int.update("threads", threads)
   4.100 +
   4.101 +    print_section("BUILD")
   4.102 +    println(s"Build started at $start_time")
   4.103 +    println(s"Isabelle id $isabelle_id")
   4.104 +    pre_hook(args)
   4.105 +
   4.106 +    print_section("LOG")
   4.107 +    val (results, elapsed_time) = build(options)
   4.108 +
   4.109 +    print_section("TIMING")
   4.110 +
   4.111 +    val groups = results.sessions.map(results.info).flatMap(_.groups)
   4.112 +    for (group <- groups)
   4.113 +      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
   4.114 +
   4.115 +    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
   4.116 +    println("Overall: " + total_timing.message_resources)
   4.117 +
   4.118 +    if (!results.ok) {
   4.119 +      print_section("FAILED SESSIONS")
   4.120 +
   4.121 +      for (name <- results.sessions) {
   4.122 +        if (results.cancelled(name)) {
   4.123 +          println(s"Session $name: CANCELLED")
   4.124 +        }
   4.125 +        else {
   4.126 +          val result = results(name)
   4.127 +          if (!result.ok)
   4.128 +            println(s"Session $name: FAILED ${result.rc}")
   4.129 +        }
   4.130 +      }
   4.131 +    }
   4.132 +
   4.133 +    post_hook(results)
   4.134 +
   4.135 +    System.exit(results.rc)
   4.136 +  }
   4.137 +
   4.138 +
   4.139 +  /* profile */
   4.140 +
   4.141 +  def documents: Boolean = true
   4.142 +
   4.143 +  def threads: Int
   4.144 +  def jobs: Int
   4.145 +  def include: List[Path]
   4.146 +  def select: List[Path]
   4.147 +
   4.148 +  def pre_hook(args: List[String]): Unit
   4.149 +  def post_hook(results: Build.Results): Unit
   4.150 +
   4.151 +  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
   4.152 +}
     5.1 --- a/src/Pure/Tools/build_history.scala	Wed Oct 12 09:32:48 2016 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,388 +0,0 @@
     5.4 -/*  Title:      Pure/Tools/build_history.scala
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Build other history versions.
     5.8 -*/
     5.9 -
    5.10 -package isabelle
    5.11 -
    5.12 -
    5.13 -import java.io.{File => JFile}
    5.14 -import java.time.format.DateTimeFormatter
    5.15 -import java.util.Locale
    5.16 -
    5.17 -
    5.18 -object Build_History
    5.19 -{
    5.20 -  /* log files */
    5.21 -
    5.22 -  val BUILD_HISTORY = "build_history"
    5.23 -  val META_INFO_MARKER = "\fmeta_info = "
    5.24 -
    5.25 -
    5.26 -
    5.27 -  /** other Isabelle environment **/
    5.28 -
    5.29 -  private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    5.30 -  {
    5.31 -    other_isabelle =>
    5.32 -
    5.33 -
    5.34 -    /* static system */
    5.35 -
    5.36 -    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    5.37 -      Isabelle_System.bash(
    5.38 -        "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
    5.39 -        env = null, cwd = isabelle_home.file, redirect = redirect,
    5.40 -        progress_stdout = progress.echo_if(echo, _),
    5.41 -        progress_stderr = progress.echo_if(echo, _))
    5.42 -
    5.43 -    def copy_dir(dir1: Path, dir2: Path): Unit =
    5.44 -      bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
    5.45 -
    5.46 -    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
    5.47 -      bash("bin/isabelle " + cmdline, redirect, echo)
    5.48 -
    5.49 -    def resolve_components(echo: Boolean): Unit =
    5.50 -      other_isabelle("components -a", redirect = true, echo = echo).check
    5.51 -
    5.52 -    val isabelle_home_user: Path =
    5.53 -      Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    5.54 -
    5.55 -    val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    5.56 -    val log_dir: Path = isabelle_home_user + Path.explode("log")
    5.57 -
    5.58 -
    5.59 -    /* reset settings */
    5.60 -
    5.61 -    def reset_settings(components_base: String, nonfree: Boolean)
    5.62 -    {
    5.63 -      if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    5.64 -        error("Cannot proceed with existing user settings file: " + etc_settings)
    5.65 -
    5.66 -      Isabelle_System.mkdirs(etc_settings.dir)
    5.67 -      File.write(etc_settings,
    5.68 -        "# generated by Isabelle " + Date.now() + "\n" +
    5.69 -        "#-*- shell-script -*- :mode=shellscript:\n")
    5.70 -
    5.71 -      val component_settings =
    5.72 -      {
    5.73 -        val components_base_path =
    5.74 -          if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    5.75 -          else Path.explode(components_base).expand
    5.76 -
    5.77 -        val catalogs =
    5.78 -          if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
    5.79 -
    5.80 -        catalogs.map(catalog =>
    5.81 -          "init_components " + File.bash_path(components_base_path) +
    5.82 -            " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
    5.83 -      }
    5.84 -      File.append(etc_settings, "\n" + Library.terminate_lines(component_settings))
    5.85 -    }
    5.86 -
    5.87 -
    5.88 -    /* augment settings */
    5.89 -
    5.90 -    def augment_settings(
    5.91 -      threads: Int,
    5.92 -      arch_64: Boolean = false,
    5.93 -      heap: Int = default_heap,
    5.94 -      max_heap: Option[Int] = None,
    5.95 -      more_settings: List[String]): String =
    5.96 -    {
    5.97 -      val (ml_platform, ml_settings) =
    5.98 -      {
    5.99 -        val windows_32 = "x86-windows"
   5.100 -        val windows_64 = "x86_64-windows"
   5.101 -        val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
   5.102 -        val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
   5.103 -        val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
   5.104 -
   5.105 -        val polyml_home =
   5.106 -          try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
   5.107 -          catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
   5.108 -
   5.109 -        def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
   5.110 -
   5.111 -        def err(platform: String): Nothing =
   5.112 -          error("Platform " + platform + " unavailable on this machine")
   5.113 -
   5.114 -        def check_dir(platform: String): Boolean =
   5.115 -          platform != "" && ml_home(platform).is_dir
   5.116 -
   5.117 -        val ml_platform =
   5.118 -          if (Platform.is_windows && arch_64) {
   5.119 -            if (check_dir(windows_64)) windows_64 else err(windows_64)
   5.120 -          }
   5.121 -          else if (Platform.is_windows && !arch_64) {
   5.122 -            if (check_dir(windows_32)) windows_32
   5.123 -            else platform_32  // x86-cygwin
   5.124 -          }
   5.125 -          else {
   5.126 -            val (platform, platform_name) =
   5.127 -              if (arch_64) (platform_64, "x86_64-" + platform_family)
   5.128 -              else (platform_32, "x86-" + platform_family)
   5.129 -            if (check_dir(platform)) platform else err(platform_name)
   5.130 -          }
   5.131 -
   5.132 -        val ml_options =
   5.133 -          "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
   5.134 -          " --gcthreads " + threads +
   5.135 -          (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
   5.136 -
   5.137 -        (ml_platform,
   5.138 -          List(
   5.139 -            "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
   5.140 -            "ML_PLATFORM=" + quote(ml_platform),
   5.141 -            "ML_OPTIONS=" + quote(ml_options)))
   5.142 -      }
   5.143 -
   5.144 -      val thread_settings =
   5.145 -        List(
   5.146 -          "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
   5.147 -          "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
   5.148 -
   5.149 -      val settings =
   5.150 -        List(ml_settings, thread_settings) :::
   5.151 -          (if (more_settings.isEmpty) Nil else List(more_settings))
   5.152 -
   5.153 -      File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
   5.154 -
   5.155 -      ml_platform
   5.156 -    }
   5.157 -  }
   5.158 -
   5.159 -
   5.160 -
   5.161 -  /** build_history **/
   5.162 -
   5.163 -  private val default_rev = "tip"
   5.164 -  private val default_threads = 1
   5.165 -  private val default_heap = 1000
   5.166 -  private val default_isabelle_identifier = "build_history"
   5.167 -
   5.168 -  def build_history(
   5.169 -    progress: Progress,
   5.170 -    hg: Mercurial.Repository,
   5.171 -    rev: String = default_rev,
   5.172 -    isabelle_identifier: String = default_isabelle_identifier,
   5.173 -    components_base: String = "",
   5.174 -    fresh: Boolean = false,
   5.175 -    nonfree: Boolean = false,
   5.176 -    multicore_base: Boolean = false,
   5.177 -    threads_list: List[Int] = List(default_threads),
   5.178 -    arch_64: Boolean = false,
   5.179 -    heap: Int = default_heap,
   5.180 -    max_heap: Option[Int] = None,
   5.181 -    more_settings: List[String] = Nil,
   5.182 -    verbose: Boolean = false,
   5.183 -    build_args: List[String] = Nil): List[Process_Result] =
   5.184 -  {
   5.185 -    /* sanity checks */
   5.186 -
   5.187 -    if (File.eq(Path.explode("~~").file, hg.root.file))
   5.188 -      error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
   5.189 -
   5.190 -    for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
   5.191 -
   5.192 -    if (heap < 100) error("Bad heap value < 100: " + heap)
   5.193 -
   5.194 -    if (max_heap.isDefined && max_heap.get < heap)
   5.195 -      error("Bad max_heap value < heap: " + max_heap.get)
   5.196 -
   5.197 -    System.getenv("ISABELLE_SETTINGS_PRESENT") match {
   5.198 -      case null | "" =>
   5.199 -      case _ => error("Cannot run build_history within existing Isabelle settings environment")
   5.200 -    }
   5.201 -
   5.202 -
   5.203 -    /* init repository */
   5.204 -
   5.205 -    hg.update(rev = rev, clean = true)
   5.206 -    progress.echo_if(verbose, hg.log(rev, options = "-l1"))
   5.207 -
   5.208 -    val isabelle_version = hg.identify(rev, options = "-i")
   5.209 -    val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
   5.210 -
   5.211 -
   5.212 -    /* main */
   5.213 -
   5.214 -    val build_history_date = Date.now()
   5.215 -    val build_host = Isabelle_System.hostname()
   5.216 -
   5.217 -    var first_build = true
   5.218 -    for (threads <- threads_list) yield
   5.219 -    {
   5.220 -      /* init settings */
   5.221 -
   5.222 -      other_isabelle.reset_settings(components_base, nonfree)
   5.223 -      other_isabelle.resolve_components(verbose)
   5.224 -      val ml_platform =
   5.225 -        other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
   5.226 -
   5.227 -      val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   5.228 -      val isabelle_output_log = isabelle_output + Path.explode("log")
   5.229 -      val isabelle_base_log = isabelle_output + Path.explode("../base_log")
   5.230 -
   5.231 -      if (first_build) {
   5.232 -        other_isabelle.resolve_components(verbose)
   5.233 -        other_isabelle.bash(
   5.234 -          "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
   5.235 -            "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
   5.236 -          redirect = true, echo = verbose).check
   5.237 -
   5.238 -        Isabelle_System.rm_tree(isabelle_base_log.file)
   5.239 -      }
   5.240 -
   5.241 -      Isabelle_System.rm_tree(isabelle_output.file)
   5.242 -      Isabelle_System.mkdirs(isabelle_output)
   5.243 -
   5.244 -
   5.245 -      /* build */
   5.246 -
   5.247 -      if (multicore_base && !first_build && isabelle_base_log.is_dir)
   5.248 -        other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
   5.249 -
   5.250 -      val build_start = Date.now()
   5.251 -      val res =
   5.252 -        other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
   5.253 -      val build_end = Date.now()
   5.254 -
   5.255 -
   5.256 -      /* output log */
   5.257 -
   5.258 -      val log_path =
   5.259 -        other_isabelle.log_dir +
   5.260 -          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
   5.261 -
   5.262 -      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
   5.263 -
   5.264 -      val meta_info =
   5.265 -        List(Build_Log.Field.build_engine -> BUILD_HISTORY,
   5.266 -          Build_Log.Field.build_host -> build_host,
   5.267 -          Build_Log.Field.build_start -> Build_Log.print_date(build_start),
   5.268 -          Build_Log.Field.build_end -> Build_Log.print_date(build_end),
   5.269 -          Build_Log.Field.isabelle_version -> isabelle_version)
   5.270 -
   5.271 -      val ml_statistics =
   5.272 -        build_info.finished_sessions.flatMap(session_name =>
   5.273 -          {
   5.274 -            val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
   5.275 -            if (session_log.is_file) {
   5.276 -              Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
   5.277 -                ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
   5.278 -            }
   5.279 -            else Nil
   5.280 -          })
   5.281 -
   5.282 -      val heap_sizes =
   5.283 -        build_info.finished_sessions.flatMap(session_name =>
   5.284 -          {
   5.285 -            val heap = isabelle_output + Path.explode(session_name)
   5.286 -            if (heap.is_file)
   5.287 -              Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
   5.288 -            else None
   5.289 -          })
   5.290 -
   5.291 -      Isabelle_System.mkdirs(log_path.dir)
   5.292 -      File.write_gzip(log_path,
   5.293 -        Library.terminate_lines(
   5.294 -          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
   5.295 -          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
   5.296 -          heap_sizes))
   5.297 -
   5.298 -      Output.writeln(log_path.implode, stdout = true)
   5.299 -
   5.300 -
   5.301 -      /* next build */
   5.302 -
   5.303 -      if (multicore_base && first_build && isabelle_output_log.is_dir)
   5.304 -        other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
   5.305 -
   5.306 -      first_build = false
   5.307 -
   5.308 -      res
   5.309 -    }
   5.310 -  }
   5.311 -
   5.312 -
   5.313 -  /* command line entry point */
   5.314 -
   5.315 -  def main(args: Array[String])
   5.316 -  {
   5.317 -    Command_Line.tool0 {
   5.318 -      var multicore_base = false
   5.319 -      var components_base = ""
   5.320 -      var heap: Option[Int] = None
   5.321 -      var max_heap: Option[Int] = None
   5.322 -      var threads_list = List(default_threads)
   5.323 -      var isabelle_identifier = default_isabelle_identifier
   5.324 -      var more_settings: List[String] = Nil
   5.325 -      var fresh = false
   5.326 -      var arch_64 = false
   5.327 -      var nonfree = false
   5.328 -      var rev = default_rev
   5.329 -      var verbose = false
   5.330 -
   5.331 -      val getopts = Getopts("""
   5.332 -Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
   5.333 -
   5.334 -  Options are:
   5.335 -    -B           first multicore build serves as base for scheduling information
   5.336 -    -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
   5.337 -    -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64)
   5.338 -    -M THREADS   multicore configurations (comma-separated list, default: """ + default_threads + """)
   5.339 -    -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
   5.340 -    -U SIZE      maximal ML heap in MB (default: unbounded)
   5.341 -    -e TEXT      additional text for generated etc/settings
   5.342 -    -f           fresh build of Isabelle/Scala components (recommended)
   5.343 -    -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
   5.344 -    -n           include nonfree components
   5.345 -    -r REV       update to revision (default: """ + default_rev + """)
   5.346 -    -v           verbose
   5.347 -
   5.348 -  Build Isabelle sessions from the history of another REPOSITORY clone,
   5.349 -  passing ARGS directly to its isabelle build tool.
   5.350 -""",
   5.351 -        "B" -> (_ => multicore_base = true),
   5.352 -        "C:" -> (arg => components_base = arg),
   5.353 -        "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
   5.354 -        "M:" -> (arg => threads_list = space_explode(',', arg).map(Value.Int.parse(_))),
   5.355 -        "N:" -> (arg => isabelle_identifier = arg),
   5.356 -        "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
   5.357 -        "e:" -> (arg => more_settings = more_settings ::: List(arg)),
   5.358 -        "f" -> (_ => fresh = true),
   5.359 -        "m:" ->
   5.360 -          {
   5.361 -            case "32" | "x86" => arch_64 = false
   5.362 -            case "64" | "x86_64" => arch_64 = true
   5.363 -            case bad => error("Bad processor architecture: " + quote(bad))
   5.364 -          },
   5.365 -        "n" -> (_ => nonfree = true),
   5.366 -        "r:" -> (arg => rev = arg),
   5.367 -        "v" -> (_ => verbose = true))
   5.368 -
   5.369 -      val more_args = getopts(args)
   5.370 -      val (root, build_args) =
   5.371 -        more_args match {
   5.372 -          case root :: build_args => (root, build_args)
   5.373 -          case _ => getopts.usage()
   5.374 -        }
   5.375 -
   5.376 -      using(Mercurial.open_repository(Path.explode(root)))(hg =>
   5.377 -        {
   5.378 -          val progress = new Console_Progress(stderr = true)
   5.379 -          val results =
   5.380 -            build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
   5.381 -              components_base = components_base, fresh = fresh, nonfree = nonfree,
   5.382 -              multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
   5.383 -              heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
   5.384 -              max_heap = max_heap, more_settings = more_settings, verbose = verbose,
   5.385 -              build_args = build_args)
   5.386 -          val rc = (0 /: results) { case (rc, res) => rc max res.rc }
   5.387 -          if (rc != 0) sys.exit(rc)
   5.388 -        })
   5.389 -    }
   5.390 -  }
   5.391 -}
     6.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 12 09:32:48 2016 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,548 +0,0 @@
     6.4 -/*  Title:      Pure/Tools/build_log.scala
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Build log parsing for current and historic formats.
     6.8 -*/
     6.9 -
    6.10 -package isabelle
    6.11 -
    6.12 -
    6.13 -import java.io.{File => JFile}
    6.14 -import java.time.ZoneId
    6.15 -import java.time.format.{DateTimeFormatter, DateTimeParseException}
    6.16 -import java.util.Locale
    6.17 -
    6.18 -import scala.collection.mutable
    6.19 -import scala.util.matching.Regex
    6.20 -
    6.21 -
    6.22 -object Build_Log
    6.23 -{
    6.24 -  /** directory content **/
    6.25 -
    6.26 -  /* file names */
    6.27 -
    6.28 -  def log_date(date: Date): String =
    6.29 -    String.format(Locale.ROOT, "%s.%05d",
    6.30 -      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
    6.31 -      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
    6.32 -
    6.33 -  def log_path(engine: String, date: Date, more: String*): Path =
    6.34 -    Path.explode(date.rep.getYear.toString) +
    6.35 -      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
    6.36 -
    6.37 -
    6.38 -  /* log file collections */
    6.39 -
    6.40 -  def is_log(file: JFile): Boolean =
    6.41 -    List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext))
    6.42 -
    6.43 -  def isatest_files(dir: Path): List[JFile] =
    6.44 -    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-"))
    6.45 -
    6.46 -  def afp_test_files(dir: Path): List[JFile] =
    6.47 -    File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-"))
    6.48 -
    6.49 -
    6.50 -
    6.51 -  /** settings **/
    6.52 -
    6.53 -  object Settings
    6.54 -  {
    6.55 -    val build_settings = List("ISABELLE_BUILD_OPTIONS")
    6.56 -    val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    6.57 -    val all_settings = build_settings ::: ml_settings
    6.58 -
    6.59 -    type Entry = (String, String)
    6.60 -    type T = List[Entry]
    6.61 -
    6.62 -    object Entry
    6.63 -    {
    6.64 -      def unapply(s: String): Option[Entry] =
    6.65 -        s.indexOf('=') match {
    6.66 -          case -1 => None
    6.67 -          case i =>
    6.68 -            val a = s.substring(0, i)
    6.69 -            val b = Library.perhaps_unquote(s.substring(i + 1))
    6.70 -            Some((a, b))
    6.71 -        }
    6.72 -      def apply(a: String, b: String): String = a + "=" + quote(b)
    6.73 -      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    6.74 -    }
    6.75 -
    6.76 -    def show(): String =
    6.77 -      cat_lines(
    6.78 -        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    6.79 -  }
    6.80 -
    6.81 -
    6.82 -
    6.83 -  /** log file **/
    6.84 -
    6.85 -  def print_date(date: Date): String = Log_File.Date_Format(date)
    6.86 -
    6.87 -  object Log_File
    6.88 -  {
    6.89 -    def apply(name: String, lines: List[String]): Log_File =
    6.90 -      new Log_File(name, lines)
    6.91 -
    6.92 -    def apply(name: String, text: String): Log_File =
    6.93 -      Log_File(name, Library.trim_split_lines(text))
    6.94 -
    6.95 -    def apply(file: JFile): Log_File =
    6.96 -    {
    6.97 -      val name = file.getName
    6.98 -      val (base_name, text) =
    6.99 -        Library.try_unsuffix(".gz", name) match {
   6.100 -          case Some(base_name) => (base_name, File.read_gzip(file))
   6.101 -          case None =>
   6.102 -            Library.try_unsuffix(".xz", name) match {
   6.103 -              case Some(base_name) => (base_name, File.read_xz(file))
   6.104 -              case None => (name, File.read(file))
   6.105 -            }
   6.106 -          }
   6.107 -      apply(base_name, text)
   6.108 -    }
   6.109 -
   6.110 -    def apply(path: Path): Log_File = apply(path.file)
   6.111 -
   6.112 -
   6.113 -    /* date format */
   6.114 -
   6.115 -    val Date_Format =
   6.116 -    {
   6.117 -      val fmts =
   6.118 -        Date.Formatter.variants(
   6.119 -          List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
   6.120 -          List(Locale.ENGLISH, Locale.GERMAN)) :::
   6.121 -        List(
   6.122 -          DateTimeFormatter.RFC_1123_DATE_TIME,
   6.123 -          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
   6.124 -
   6.125 -      def tune_timezone(s: String): String =
   6.126 -        s match {
   6.127 -          case "CET" | "MET" => "GMT+1"
   6.128 -          case "CEST" | "MEST" => "GMT+2"
   6.129 -          case "EST" => "Europe/Berlin"
   6.130 -          case _ => s
   6.131 -        }
   6.132 -      def tune_weekday(s: String): String =
   6.133 -        s match {
   6.134 -          case "Die" => "Di"
   6.135 -          case "Mit" => "Mi"
   6.136 -          case "Don" => "Do"
   6.137 -          case "Fre" => "Fr"
   6.138 -          case "Sam" => "Sa"
   6.139 -          case "Son" => "So"
   6.140 -          case _ => s
   6.141 -        }
   6.142 -
   6.143 -      def tune(s: String): String =
   6.144 -        Word.implode(
   6.145 -          Word.explode(s) match {
   6.146 -            case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
   6.147 -            case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
   6.148 -            case Nil => Nil
   6.149 -          }
   6.150 -        )
   6.151 -
   6.152 -      Date.Format.make(fmts, tune)
   6.153 -    }
   6.154 -
   6.155 -
   6.156 -    /* inlined content */
   6.157 -
   6.158 -    def print_props(marker: String, props: Properties.T): String =
   6.159 -      marker + YXML.string_of_body(XML.Encode.properties(props))
   6.160 -  }
   6.161 -
   6.162 -  class Log_File private(val name: String, val lines: List[String])
   6.163 -  {
   6.164 -    log_file =>
   6.165 -
   6.166 -    override def toString: String = name
   6.167 -
   6.168 -    def text: String = cat_lines(lines)
   6.169 -
   6.170 -    def err(msg: String): Nothing =
   6.171 -      error("Error in log file " + quote(name) + ": " + msg)
   6.172 -
   6.173 -
   6.174 -    /* date format */
   6.175 -
   6.176 -    object Strict_Date
   6.177 -    {
   6.178 -      def unapply(s: String): Some[Date] =
   6.179 -        try { Some(Log_File.Date_Format.parse(s)) }
   6.180 -        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
   6.181 -    }
   6.182 -
   6.183 -
   6.184 -    /* inlined content */
   6.185 -
   6.186 -    def find[A](f: String => Option[A]): Option[A] =
   6.187 -      lines.iterator.map(f).find(_.isDefined).map(_.get)
   6.188 -
   6.189 -    def find_match(regex: Regex): Option[String] =
   6.190 -      lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
   6.191 -        map(res => res.get.head)
   6.192 -
   6.193 -
   6.194 -    /* settings */
   6.195 -
   6.196 -    def get_setting(a: String): Option[Settings.Entry] =
   6.197 -      lines.find(_.startsWith(a + "=")) match {
   6.198 -        case Some(line) => Settings.Entry.unapply(line)
   6.199 -        case None => None
   6.200 -      }
   6.201 -
   6.202 -    def get_settings(as: List[String]): Settings.T =
   6.203 -      for { a <- as; entry <- get_setting(a) } yield entry
   6.204 -
   6.205 -
   6.206 -    /* properties (YXML) */
   6.207 -
   6.208 -    val xml_cache = new XML.Cache()
   6.209 -
   6.210 -    def parse_props(text: String): Properties.T =
   6.211 -      xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
   6.212 -
   6.213 -    def filter_props(marker: String): List[Properties.T] =
   6.214 -      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
   6.215 -
   6.216 -    def find_line(marker: String): Option[String] =
   6.217 -      find(Library.try_unprefix(marker, _))
   6.218 -
   6.219 -    def find_props(marker: String): Option[Properties.T] =
   6.220 -      find_line(marker).map(parse_props(_))
   6.221 -
   6.222 -
   6.223 -    /* parse various formats */
   6.224 -
   6.225 -    def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
   6.226 -
   6.227 -    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   6.228 -
   6.229 -    def parse_session_info(
   6.230 -        default_name: String = "",
   6.231 -        command_timings: Boolean = false,
   6.232 -        ml_statistics: Boolean = false,
   6.233 -        task_statistics: Boolean = false): Session_Info =
   6.234 -      Build_Log.parse_session_info(
   6.235 -        log_file, default_name, command_timings, ml_statistics, task_statistics)
   6.236 -  }
   6.237 -
   6.238 -
   6.239 -
   6.240 -  /** meta info **/
   6.241 -
   6.242 -  object Field
   6.243 -  {
   6.244 -    val build_engine = "build_engine"
   6.245 -    val build_host = "build_host"
   6.246 -    val build_start = "build_start"
   6.247 -    val build_end = "build_end"
   6.248 -    val isabelle_version = "isabelle_version"
   6.249 -    val afp_version = "afp_version"
   6.250 -  }
   6.251 -
   6.252 -  object Meta_Info
   6.253 -  {
   6.254 -    val empty: Meta_Info = Meta_Info(Nil, Nil)
   6.255 -  }
   6.256 -
   6.257 -  sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)])
   6.258 -  {
   6.259 -    def is_empty: Boolean = props.isEmpty && settings.isEmpty
   6.260 -  }
   6.261 -
   6.262 -  object Isatest
   6.263 -  {
   6.264 -    val engine = "isatest"
   6.265 -    val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
   6.266 -    val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
   6.267 -    val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
   6.268 -    val No_AFP_Version = new Regex("""$.""")
   6.269 -  }
   6.270 -
   6.271 -  object AFP_Test
   6.272 -  {
   6.273 -    val engine = "afp-test"
   6.274 -    val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   6.275 -    val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   6.276 -    val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   6.277 -    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   6.278 -    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   6.279 -    val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
   6.280 -  }
   6.281 -
   6.282 -  object Jenkins
   6.283 -  {
   6.284 -    val engine = "jenkins"
   6.285 -    val Start = new Regex("""^Started .*$""")
   6.286 -    val Start_Date = new Regex("""^Build started at (.+)$""")
   6.287 -    val No_End = new Regex("""$.""")
   6.288 -    val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
   6.289 -    val AFP_Version = new Regex("""^AFP id (\S+)$""")
   6.290 -    val CONFIGURATION = "=== CONFIGURATION ==="
   6.291 -    val BUILD = "=== BUILD ==="
   6.292 -    val FINISHED = "Finished: "
   6.293 -  }
   6.294 -
   6.295 -  private def parse_meta_info(log_file: Log_File): Meta_Info =
   6.296 -  {
   6.297 -    def parse(engine: String, host: String, start: Date,
   6.298 -      End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
   6.299 -    {
   6.300 -      val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
   6.301 -      val build_host = if (host == "") Nil else List(Field.build_host -> host)
   6.302 -
   6.303 -      val start_date = List(Field.build_start -> start.toString)
   6.304 -      val end_date =
   6.305 -        log_file.lines.last match {
   6.306 -          case End(log_file.Strict_Date(end_date)) =>
   6.307 -            List(Field.build_end -> end_date.toString)
   6.308 -          case _ => Nil
   6.309 -        }
   6.310 -
   6.311 -      val isabelle_version =
   6.312 -        log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
   6.313 -      val afp_version =
   6.314 -        log_file.find_match(AFP_Version).map(Field.afp_version -> _)
   6.315 -
   6.316 -      Meta_Info(build_engine ::: build_host :::
   6.317 -          start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
   6.318 -        log_file.get_settings(Settings.all_settings))
   6.319 -    }
   6.320 -
   6.321 -    log_file.lines match {
   6.322 -      case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
   6.323 -        Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
   6.324 -          log_file.get_settings(Settings.all_settings))
   6.325 -
   6.326 -      case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
   6.327 -        parse(Isatest.engine, host, start, Isatest.End,
   6.328 -          Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   6.329 -
   6.330 -      case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
   6.331 -        parse(AFP_Test.engine, host, start, AFP_Test.End,
   6.332 -          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   6.333 -
   6.334 -      case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
   6.335 -        parse(AFP_Test.engine, "", start, AFP_Test.End,
   6.336 -          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
   6.337 -
   6.338 -      case Jenkins.Start() :: _
   6.339 -      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
   6.340 -         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
   6.341 -        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
   6.342 -          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
   6.343 -            parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End,
   6.344 -              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
   6.345 -          case _ => Meta_Info.empty
   6.346 -        }
   6.347 -
   6.348 -      case line :: _ if line.startsWith("\0") => Meta_Info.empty
   6.349 -      case List(Isatest.End(_)) => Meta_Info.empty
   6.350 -      case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
   6.351 -      case Nil => Meta_Info.empty
   6.352 -
   6.353 -      case _ => log_file.err("cannot detect log file format")
   6.354 -    }
   6.355 -  }
   6.356 -
   6.357 -
   6.358 -
   6.359 -  /** build info: produced by isabelle build or build_history **/
   6.360 -
   6.361 -  val ML_STATISTICS_MARKER = "\fML_statistics = "
   6.362 -  val SESSION_NAME = "session_name"
   6.363 -
   6.364 -  object Session_Status extends Enumeration
   6.365 -  {
   6.366 -    val EXISTING = Value("existing")
   6.367 -    val FINISHED = Value("finished")
   6.368 -    val FAILED = Value("failed")
   6.369 -    val CANCELLED = Value("cancelled")
   6.370 -  }
   6.371 -
   6.372 -  sealed case class Session_Entry(
   6.373 -    chapter: String,
   6.374 -    groups: List[String],
   6.375 -    threads: Option[Int],
   6.376 -    timing: Timing,
   6.377 -    ml_timing: Timing,
   6.378 -    ml_statistics: List[Properties.T],
   6.379 -    heap_size: Option[Long],
   6.380 -    status: Session_Status.Value)
   6.381 -  {
   6.382 -    def finished: Boolean = status == Session_Status.FINISHED
   6.383 -  }
   6.384 -
   6.385 -  sealed case class Build_Info(sessions: Map[String, Session_Entry])
   6.386 -  {
   6.387 -    def session(name: String): Session_Entry = sessions(name)
   6.388 -    def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   6.389 -
   6.390 -    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   6.391 -      get_session(name) match {
   6.392 -        case Some(entry) => f(entry)
   6.393 -        case None => x
   6.394 -      }
   6.395 -
   6.396 -    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
   6.397 -    def finished(name: String): Boolean = get_default(name, _.finished, false)
   6.398 -    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   6.399 -    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   6.400 -  }
   6.401 -
   6.402 -  private def parse_build_info(log_file: Log_File): Build_Info =
   6.403 -  {
   6.404 -    object Chapter_Name
   6.405 -    {
   6.406 -      def unapply(s: String): Some[(String, String)] =
   6.407 -        space_explode('/', s) match {
   6.408 -          case List(chapter, name) => Some((chapter, name))
   6.409 -          case _ => Some(("", s))
   6.410 -        }
   6.411 -    }
   6.412 -
   6.413 -    val Session_No_Groups = new Regex("""^Session (\S+)$""")
   6.414 -    val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   6.415 -    val Session_Finished1 =
   6.416 -      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   6.417 -    val Session_Finished2 =
   6.418 -      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   6.419 -    val Session_Timing =
   6.420 -      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   6.421 -    val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   6.422 -    val Session_Failed = new Regex("""^(\S+) FAILED""")
   6.423 -    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   6.424 -    val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
   6.425 -
   6.426 -    var chapter = Map.empty[String, String]
   6.427 -    var groups = Map.empty[String, List[String]]
   6.428 -    var threads = Map.empty[String, Int]
   6.429 -    var timing = Map.empty[String, Timing]
   6.430 -    var ml_timing = Map.empty[String, Timing]
   6.431 -    var started = Set.empty[String]
   6.432 -    var failed = Set.empty[String]
   6.433 -    var cancelled = Set.empty[String]
   6.434 -    var ml_statistics = Map.empty[String, List[Properties.T]]
   6.435 -    var heap_sizes = Map.empty[String, Long]
   6.436 -
   6.437 -    def all_sessions: Set[String] =
   6.438 -      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
   6.439 -      failed ++ cancelled ++ started ++ ml_statistics.keySet ++ heap_sizes.keySet
   6.440 -
   6.441 -
   6.442 -    for (line <- log_file.lines) {
   6.443 -      line match {
   6.444 -        case Session_No_Groups(Chapter_Name(chapt, name)) =>
   6.445 -          chapter += (name -> chapt)
   6.446 -          groups += (name -> Nil)
   6.447 -
   6.448 -        case Session_Groups(Chapter_Name(chapt, name), grps) =>
   6.449 -          chapter += (name -> chapt)
   6.450 -          groups += (name -> Word.explode(grps))
   6.451 -
   6.452 -        case Session_Started(name) =>
   6.453 -          started += name
   6.454 -
   6.455 -        case Session_Finished1(name,
   6.456 -            Value.Int(e1), Value.Int(e2), Value.Int(e3),
   6.457 -            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   6.458 -          val elapsed = Time.hms(e1, e2, e3)
   6.459 -          val cpu = Time.hms(c1, c2, c3)
   6.460 -          timing += (name -> Timing(elapsed, cpu, Time.zero))
   6.461 -
   6.462 -        case Session_Finished2(name,
   6.463 -            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   6.464 -          val elapsed = Time.hms(e1, e2, e3)
   6.465 -          timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   6.466 -
   6.467 -        case Session_Timing(name,
   6.468 -            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   6.469 -          val elapsed = Time.seconds(e)
   6.470 -          val cpu = Time.seconds(c)
   6.471 -          val gc = Time.seconds(g)
   6.472 -          ml_timing += (name -> Timing(elapsed, cpu, gc))
   6.473 -          threads += (name -> t)
   6.474 -
   6.475 -        case Heap(name, Value.Long(size)) =>
   6.476 -          heap_sizes += (name -> size)
   6.477 -
   6.478 -        case _ if line.startsWith(ML_STATISTICS_MARKER) =>
   6.479 -          val (name, props) =
   6.480 -            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
   6.481 -              case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
   6.482 -              case _ => log_file.err("malformed ML_statistics " + quote(line))
   6.483 -            }
   6.484 -          ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
   6.485 -
   6.486 -        case _ =>
   6.487 -      }
   6.488 -    }
   6.489 -
   6.490 -    val sessions =
   6.491 -      Map(
   6.492 -        (for (name <- all_sessions.toList) yield {
   6.493 -          val status =
   6.494 -            if (failed(name)) Session_Status.FAILED
   6.495 -            else if (cancelled(name)) Session_Status.CANCELLED
   6.496 -            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   6.497 -              Session_Status.FINISHED
   6.498 -            else if (started(name)) Session_Status.FAILED
   6.499 -            else Session_Status.EXISTING
   6.500 -          val entry =
   6.501 -            Session_Entry(
   6.502 -              chapter.getOrElse(name, ""),
   6.503 -              groups.getOrElse(name, Nil),
   6.504 -              threads.get(name),
   6.505 -              timing.getOrElse(name, Timing.zero),
   6.506 -              ml_timing.getOrElse(name, Timing.zero),
   6.507 -              ml_statistics.getOrElse(name, Nil).reverse,
   6.508 -              heap_sizes.get(name),
   6.509 -              status)
   6.510 -          (name -> entry)
   6.511 -        }):_*)
   6.512 -    Build_Info(sessions)
   6.513 -  }
   6.514 -
   6.515 -
   6.516 -
   6.517 -  /** session info: produced by "isabelle build" **/
   6.518 -
   6.519 -  sealed case class Session_Info(
   6.520 -    session_name: String,
   6.521 -    session_timing: Properties.T,
   6.522 -    command_timings: List[Properties.T],
   6.523 -    ml_statistics: List[Properties.T],
   6.524 -    task_statistics: List[Properties.T])
   6.525 -
   6.526 -  private def parse_session_info(
   6.527 -    log_file: Log_File,
   6.528 -    default_name: String,
   6.529 -    command_timings: Boolean,
   6.530 -    ml_statistics: Boolean,
   6.531 -    task_statistics: Boolean): Session_Info =
   6.532 -  {
   6.533 -    val xml_cache = new XML.Cache()
   6.534 -
   6.535 -    val session_name =
   6.536 -      log_file.find_line("\fSession.name = ") match {
   6.537 -        case None => default_name
   6.538 -        case Some(name) if default_name == "" || default_name == name => name
   6.539 -        case Some(name) => log_file.err("log from different session " + quote(name))
   6.540 -      }
   6.541 -    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   6.542 -    val command_timings_ =
   6.543 -      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   6.544 -    val ml_statistics_ =
   6.545 -      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
   6.546 -    val task_statistics_ =
   6.547 -      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   6.548 -
   6.549 -    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   6.550 -  }
   6.551 -}
     7.1 --- a/src/Pure/Tools/ci_api.scala	Wed Oct 12 09:32:48 2016 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,74 +0,0 @@
     7.4 -/*  Title:      Pure/Tools/ci_api.scala
     7.5 -    Author:     Makarius
     7.6 -
     7.7 -API for Isabelle Jenkins continuous integration services.
     7.8 -*/
     7.9 -
    7.10 -package isabelle
    7.11 -
    7.12 -
    7.13 -import java.net.URL
    7.14 -
    7.15 -import scala.util.matching.Regex
    7.16 -
    7.17 -
    7.18 -object CI_API
    7.19 -{
    7.20 -  /* CI service */
    7.21 -
    7.22 -  def root(): String =
    7.23 -    Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
    7.24 -
    7.25 -  def invoke(url: String, args: String*): Any =
    7.26 -  {
    7.27 -    val req = url + "/api/json?" + args.mkString("&")
    7.28 -    val result = Url.read(req)
    7.29 -    try { JSON.parse(result) }
    7.30 -    catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
    7.31 -  }
    7.32 -
    7.33 -
    7.34 -  /* build jobs */
    7.35 -
    7.36 -  def build_jobs(): List[String] =
    7.37 -    for {
    7.38 -      job <- JSON.array(invoke(root()), "jobs")
    7.39 -      _class <- JSON.string(job, "_class")
    7.40 -      if _class == "hudson.model.FreeStyleProject"
    7.41 -      name <- JSON.string(job, "name")
    7.42 -    } yield name
    7.43 -
    7.44 -  sealed case class Job_Info(
    7.45 -    job_name: String,
    7.46 -    timestamp: Long,
    7.47 -    output: URL,
    7.48 -    session_logs: List[(String, URL)])
    7.49 -  {
    7.50 -    def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    7.51 -    def read_session_log(name: String): Build_Log.Log_File =
    7.52 -      Build_Log.Log_File(name,
    7.53 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    7.54 -  }
    7.55 -
    7.56 -  def build_job_builds(job_name: String): List[Job_Info] =
    7.57 -  {
    7.58 -    val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
    7.59 -
    7.60 -    for {
    7.61 -      build <- JSON.array(
    7.62 -        invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    7.63 -      number <- JSON.int(build, "number")
    7.64 -      timestamp <- JSON.long(build, "timestamp")
    7.65 -    } yield {
    7.66 -      val job_prefix = root() + "/job/" + job_name + "/" + number
    7.67 -      val output = Url(job_prefix + "/consoleText")
    7.68 -      val session_logs =
    7.69 -        for {
    7.70 -          artifact <- JSON.array(build, "artifacts")
    7.71 -          log_path <- JSON.string(artifact, "relativePath")
    7.72 -          session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
    7.73 -        } yield (session -> Url(job_prefix + "/artifact/" + log_path))
    7.74 -      Job_Info(job_name, timestamp, output, session_logs)
    7.75 -    }
    7.76 -  }
    7.77 -}
     8.1 --- a/src/Pure/Tools/ci_profile.scala	Wed Oct 12 09:32:48 2016 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,149 +0,0 @@
     8.4 -/*  Title:      Pure/Tools/ci_profile.scala
     8.5 -    Author:     Lars Hupel
     8.6 -
     8.7 -Build profile for continuous integration services.
     8.8 -*/
     8.9 -
    8.10 -package isabelle
    8.11 -
    8.12 -
    8.13 -import java.time.{Instant, ZoneId}
    8.14 -import java.time.format.DateTimeFormatter
    8.15 -import java.util.{Properties => JProperties}
    8.16 -
    8.17 -
    8.18 -abstract class CI_Profile extends Isabelle_Tool.Body
    8.19 -{
    8.20 -  private def build(options: Options): (Build.Results, Time) =
    8.21 -  {
    8.22 -    val progress = new Console_Progress(verbose = true)
    8.23 -    val start_time = Time.now()
    8.24 -    val results = progress.interrupt_handler {
    8.25 -      Build.build_selection(
    8.26 -        options = options,
    8.27 -        progress = progress,
    8.28 -        clean_build = true,
    8.29 -        verbose = true,
    8.30 -        max_jobs = jobs,
    8.31 -        dirs = include,
    8.32 -        select_dirs = select,
    8.33 -        system_mode = true,
    8.34 -        selection = select_sessions _)
    8.35 -    }
    8.36 -    val end_time = Time.now()
    8.37 -    (results, end_time - start_time)
    8.38 -  }
    8.39 -
    8.40 -  private def load_properties(): JProperties =
    8.41 -  {
    8.42 -    val props = new JProperties()
    8.43 -    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
    8.44 -
    8.45 -    if (file_name != "")
    8.46 -    {
    8.47 -      val file = Path.explode(file_name).file
    8.48 -      if (file.exists())
    8.49 -        props.load(new java.io.FileReader(file))
    8.50 -      props
    8.51 -    }
    8.52 -    else
    8.53 -      props
    8.54 -  }
    8.55 -
    8.56 -  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
    8.57 -  {
    8.58 -    val timings = results.sessions.collect {
    8.59 -      case session if group.forall(results.info(session).groups.contains(_)) =>
    8.60 -        results(session).timing
    8.61 -    }
    8.62 -    (Timing.zero /: timings)(_ + _)
    8.63 -  }
    8.64 -
    8.65 -  private def with_documents(options: Options): Options =
    8.66 -  {
    8.67 -    if (documents)
    8.68 -      options
    8.69 -        .bool.update("browser_info", true)
    8.70 -        .string.update("document", "pdf")
    8.71 -        .string.update("document_variants", "document:outline=/proof,/ML")
    8.72 -    else
    8.73 -      options
    8.74 -  }
    8.75 -
    8.76 -
    8.77 -  final def hg_id(path: Path): String =
    8.78 -    Isabelle_System.hg("id -i", path.file).out
    8.79 -
    8.80 -  final def print_section(title: String): Unit =
    8.81 -    println(s"\n=== $title ===\n")
    8.82 -
    8.83 -
    8.84 -  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
    8.85 -  final val isabelle_id = hg_id(isabelle_home)
    8.86 -  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
    8.87 -
    8.88 -
    8.89 -  override final def apply(args: List[String]): Unit =
    8.90 -  {
    8.91 -    print_section("CONFIGURATION")
    8.92 -    println(Build_Log.Settings.show())
    8.93 -    val props = load_properties()
    8.94 -    System.getProperties().putAll(props)
    8.95 -
    8.96 -    val options =
    8.97 -      with_documents(Options.init())
    8.98 -        .int.update("parallel_proofs", 2)
    8.99 -        .int.update("threads", threads)
   8.100 -
   8.101 -    print_section("BUILD")
   8.102 -    println(s"Build started at $start_time")
   8.103 -    println(s"Isabelle id $isabelle_id")
   8.104 -    pre_hook(args)
   8.105 -
   8.106 -    print_section("LOG")
   8.107 -    val (results, elapsed_time) = build(options)
   8.108 -
   8.109 -    print_section("TIMING")
   8.110 -
   8.111 -    val groups = results.sessions.map(results.info).flatMap(_.groups)
   8.112 -    for (group <- groups)
   8.113 -      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
   8.114 -
   8.115 -    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
   8.116 -    println("Overall: " + total_timing.message_resources)
   8.117 -
   8.118 -    if (!results.ok) {
   8.119 -      print_section("FAILED SESSIONS")
   8.120 -
   8.121 -      for (name <- results.sessions) {
   8.122 -        if (results.cancelled(name)) {
   8.123 -          println(s"Session $name: CANCELLED")
   8.124 -        }
   8.125 -        else {
   8.126 -          val result = results(name)
   8.127 -          if (!result.ok)
   8.128 -            println(s"Session $name: FAILED ${result.rc}")
   8.129 -        }
   8.130 -      }
   8.131 -    }
   8.132 -
   8.133 -    post_hook(results)
   8.134 -
   8.135 -    System.exit(results.rc)
   8.136 -  }
   8.137 -
   8.138 -
   8.139 -  /* profile */
   8.140 -
   8.141 -  def documents: Boolean = true
   8.142 -
   8.143 -  def threads: Int
   8.144 -  def jobs: Int
   8.145 -  def include: List[Path]
   8.146 -  def select: List[Path]
   8.147 -
   8.148 -  def pre_hook(args: List[String]): Unit
   8.149 -  def post_hook(results: Build.Results): Unit
   8.150 -
   8.151 -  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
   8.152 -}
     9.1 --- a/src/Pure/build-jars	Wed Oct 12 09:32:48 2016 +0200
     9.2 +++ b/src/Pure/build-jars	Wed Oct 12 09:38:20 2016 +0200
     9.3 @@ -9,6 +9,10 @@
     9.4  ## sources
     9.5  
     9.6  declare -a SOURCES=(
     9.7 +  Admin/build_history.scala
     9.8 +  Admin/build_log.scala
     9.9 +  Admin/ci_api.scala
    9.10 +  Admin/ci_profile.scala
    9.11    Admin/isabelle_cronjob.scala
    9.12    Concurrent/consumer_thread.scala
    9.13    Concurrent/counter.scala
    9.14 @@ -110,13 +114,9 @@
    9.15    Tools/bibtex.scala
    9.16    Tools/build.scala
    9.17    Tools/build_doc.scala
    9.18 -  Tools/build_history.scala
    9.19 -  Tools/build_log.scala
    9.20    Tools/build_stats.scala
    9.21    Tools/check_keywords.scala
    9.22    Tools/check_sources.scala
    9.23 -  Tools/ci_api.scala
    9.24 -  Tools/ci_profile.scala
    9.25    Tools/debugger.scala
    9.26    Tools/doc.scala
    9.27    Tools/main.scala