integrity test of build_history vs. build_history_base;
misc tuning and clarification;

--- a/src/Pure/Admin/build_history.scala	Thu Oct 13 16:14:41 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Oct 13 17:22:32 2016 +0200
@@ -101,8 +101,8 @@
   private val default_isabelle_identifier = "build_history"
 
   def build_history(
-    progress: Progress,
     hg: Mercurial.Repository,
+    progress: Progress = Ignore_Progress,
     rev: String = default_rev,
     isabelle_identifier: String = default_isabelle_identifier,
     components_base: String = "",
@@ -115,7 +115,7 @@
     max_heap: Option[Int] = None,
     more_settings: List[String] = Nil,
     verbose: Boolean = false,
-    build_args: List[String] = Nil): List[Process_Result] =
+    build_args: List[String] = Nil): List[(Process_Result, Path)] =
   {
     /* sanity checks */
 
@@ -232,8 +232,6 @@
           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
           heap_sizes))
 
-      Output.writeln(log_path.implode, stdout = true)
-
 
       /* next build */
 
@@ -242,7 +240,7 @@
 
       first_build = false
 
-      res
+      (res, log_path)
     }
   }
 
@@ -313,14 +311,17 @@
       val hg = Mercurial.repository(Path.explode(root))
       val progress = new Console_Progress(stderr = true)
       val results =
-        build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
+        build_history(hg, progress = progress, rev = rev, isabelle_identifier = isabelle_identifier,
           components_base = components_base, fresh = fresh, nonfree = nonfree,
           multicore_base = multicore_base, threads_list = threads_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, more_settings = more_settings, verbose = verbose,
           build_args = build_args)
 
-      val rc = (0 /: results) { case (rc, res) => rc max res.rc }
+      for ((_, log_path) <- results)
+        Output.writeln(log_path.implode, stdout = true)
+
+      val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0) sys.exit(rc)
     }
   }

--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 16:14:41 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 17:22:32 2016 +0200
@@ -13,43 +13,38 @@
 
 object Isabelle_Cronjob
 {
-  /** file-system state: owned by main cronjob **/
+  /* file-system state: owned by main cronjob */
 
   val main_dir = Path.explode("~/cronjob")
-  val run_dir = main_dir + Path.explode("run")
-  val log_dir = main_dir + Path.explode("log")
+  val main_state_file = main_dir + Path.explode("run/main.state")
+  val main_log = main_dir + Path.explode("log/main.log")  // owned by log service
 
-  val main_state_file = run_dir + Path.explode("main.state")
-  val main_log = log_dir + Path.explode("main.log")  // owned by log service
+  val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
+  val afp_repos = main_dir + Path.explode("AFP-build_history")
 
 
 
   /** particular tasks **/
 
-  /* identify repository snapshots */
+  /* identify Isabelle + AFP repository snapshots */
 
-  val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
-  val afp_repos = main_dir + Path.explode("AFP-build_history")
+  private def pull_repos(root: Path): String =
+  {
+    val hg = Mercurial.repository(root)
+    hg.pull(options = "-q")
+    hg.identify("tip", options = "-i")
+  }
 
-  val isabelle_identify =
+  private val isabelle_identify =
     Logger_Task("isabelle_identify", logger =>
       {
-        def pull_repos(root: Path): String =
-        {
-          val hg = Mercurial.repository(root)
-          hg.pull(options = "-q")
-          hg.identify("tip", options = "-i")
-        }
-
         val isabelle_id = pull_repos(isabelle_repos)
         val afp_id = pull_repos(afp_repos)
 
-        val log_path =
-          main_dir +
-            Build_Log.log_subdir(logger.start_date) +
-            Build_Log.log_filename("isabelle_identify", logger.start_date)
-        Isabelle_System.mkdirs(log_path.dir)
-        File.write(log_path,
+        val log_dir = main_dir + Build_Log.log_subdir(logger.start_date)
+        Isabelle_System.mkdirs(log_dir)
+
+        File.write(log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
           terminate_lines(
             List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
               "",
@@ -58,12 +53,22 @@
       })
 
 
-  /* build_history_base integrity test */
+  /* integrity test of build_history vs. build_history_base */
 
-  val build_history_base =
+  private val build_history_base =
     Logger_Task("build_history_base", logger =>
       {
-        error("FIXME")
+        val log_dir = main_dir + Build_Log.log_subdir(logger.start_date)
+        Isabelle_System.mkdirs(log_dir)
+
+        for {
+          (result, log_path) <-
+            Build_History.build_history(Mercurial.repository(isabelle_repos),
+              rev = "build_history_base", fresh = true, build_args = List("FOL"))
+        } {
+          result.check
+          File.copy(log_path, log_dir + log_path.base)
+        }
       })