# HG changeset patch
# User wenzelm
# Date 1476782654 -7200
# Node ID 544481988e659ea322a2289bbce6f63fea70ff1c
# Parent  6aefa7e66888286d05ecd3b2f13f99d146c718da
explicit identification of builds and correlated build groups;

diff -r 6aefa7e66888 -r 544481988e65 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 18 10:11:22 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 11:24:14 2016 +0200
@@ -146,8 +146,9 @@
 
     /* main */
 
+    val build_host = Isabelle_System.hostname()
     val build_history_date = Date.now()
-    val build_host = Isabelle_System.hostname()
+    val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
     for (threads <- threads_list) yield
@@ -183,23 +184,27 @@
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
-      val res =
+      val build_result =
         other_isabelle("build -v " + File.bash_args(build_args), redirect = true, echo = verbose)
       val build_end = Date.now()
 
-
-      /* output log */
-
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
           Build_Log.log_filename(
             BUILD_HISTORY, build_history_date, build_host, ml_platform, "M" + threads)
 
-      val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
+      val build_info =
+        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).parse_build_info()
+
+
+      /* output log */
 
       val meta_info =
-        List(Build_Log.Field.build_engine -> BUILD_HISTORY,
+        List(
+          Build_Log.Field.build_group_id -> build_group_id,
+          Build_Log.Field.build_id -> (build_host + ":" + build_start.time.ms),
+          Build_Log.Field.build_engine -> BUILD_HISTORY,
           Build_Log.Field.build_host -> build_host,
           Build_Log.Field.build_start -> Build_Log.print_date(build_start),
           Build_Log.Field.build_end -> Build_Log.print_date(build_end),
@@ -228,7 +233,7 @@
       Isabelle_System.mkdirs(log_path.dir)
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
-          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
+          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
           heap_sizes), XZ.options(6))
 
@@ -242,7 +247,7 @@
 
       first_build = false
 
-      (res, log_path.ext("xz"))
+      (build_result, log_path.ext("xz"))
     }
   }
 
diff -r 6aefa7e66888 -r 544481988e65 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Oct 18 10:11:22 2016 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 18 11:24:14 2016 +0200
@@ -247,6 +247,8 @@
 
   object Field
   {
+    val build_group_id = "build_group_id"
+    val build_id = "build_id"
     val build_engine = "build_engine"
     val build_host = "build_host"
     val build_start = "build_start"
@@ -303,6 +305,11 @@
     def parse(engine: String, host: String, start: Date,
       End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
     {
+      val build_id =
+      {
+        val prefix = if (host != "") host else if (engine != "") engine else ""
+        (if (prefix == "") "build" else prefix) + ":" + start.time.ms
+      }
       val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine)
       val build_host = if (host == "") Nil else List(Field.build_host -> host)
 
@@ -319,7 +326,7 @@
       val afp_version =
         log_file.find_match(AFP_Version).map(Field.afp_version -> _)
 
-      Meta_Info(build_engine ::: build_host :::
+      Meta_Info((Field.build_id -> build_id) :: build_engine ::: build_host :::
           start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
         log_file.get_settings(Settings.all_settings))
     }