diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala
+++ b/src/Pure/Admin/build_history.scala
@@ -1,589 +1,589 @@
 /*  Title:      Pure/Admin/build_history.scala
     Author:     Makarius
 
 Build other history versions.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.time.format.DateTimeFormatter
 import java.util.Locale
 
 
 object Build_History
 {
   /* log files */
 
   val engine = "build_history"
   val log_prefix = engine + "_"
   val META_INFO_MARKER = "\fmeta_info = "
 
 
   /* augment settings */
 
   def augment_settings(
     other_isabelle: Other_Isabelle,
     threads: Int,
     arch_64: Boolean,
     heap: Int,
     max_heap: Option[Int],
     more_settings: List[String]): String =
   {
     val (ml_platform, ml_settings) =
     {
       val windows_32 = "x86-windows"
       val windows_64 = "x86_64-windows"
       val platform_32 = other_isabelle("getenv -b ISABELLE_PLATFORM32").check.out
       val platform_64 = other_isabelle("getenv -b ISABELLE_PLATFORM64").check.out
       val platform_family = other_isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
 
       val polyml_home =
         try { Path.explode(other_isabelle("getenv -b ML_HOME").check.out).dir }
         catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
 
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
 
       def err(platform: String): Nothing =
         error("Platform " + platform + " unavailable on this machine")
 
       def check_dir(platform: String): Boolean =
         platform != "" && ml_home(platform).is_dir
 
       val ml_platform =
         if (Platform.is_windows && arch_64) {
           if (check_dir(windows_64)) windows_64 else err(windows_64)
         }
         else if (Platform.is_windows && !arch_64) {
           if (check_dir(windows_32)) windows_32
           else platform_32  // x86-cygwin
         }
         else {
           val (platform, platform_name) =
             if (arch_64) (platform_64, "x86_64-" + platform_family)
             else (platform_32, "x86-" + platform_family)
           if (check_dir(platform)) platform else err(platform_name)
         }
 
       val ml_options =
         "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") +
         " --gcthreads " + threads +
         (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
 
       (ml_platform,
         List(
           "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
           "ML_PLATFORM=" + quote(ml_platform),
           "ML_OPTIONS=" + quote(ml_options)))
     }
 
     val thread_settings =
       List(
         "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"",
         "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"")
 
     val settings =
       List(ml_settings, thread_settings) :::
       (if (more_settings.isEmpty) Nil else List(more_settings))
 
     File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
 
     ml_platform
   }
 
 
 
   /** build_history **/
 
   private val default_user_home = Path.explode("$USER_HOME")
   private val default_rev = "tip"
   private val default_multicore = (1, 1)
   private val default_heap = 1500
   private val default_isabelle_identifier = "build_history"
 
   def build_history(
     options: Options,
     root: Path,
     user_home: Path = default_user_home,
     progress: Progress = No_Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
     afp_partition: Int = 0,
     isabelle_identifier: String = default_isabelle_identifier,
     ml_statistics_step: Int = 1,
     components_base: String = "",
     fresh: Boolean = false,
     nonfree: Boolean = false,
     multicore_base: Boolean = false,
     multicore_list: List[(Int, Int)] = List(default_multicore),
     arch_64: Boolean = false,
     heap: Int = default_heap,
     max_heap: Option[Int] = None,
     init_settings: List[String] = Nil,
     more_settings: List[String] = Nil,
     verbose: Boolean = false,
     build_tags: List[String] = Nil,
     build_args: List[String] = Nil): List[(Process_Result, Path)] =
   {
     /* sanity checks */
 
     if (File.eq(Path.explode("~~"), root))
       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
 
     for ((threads, _) <- multicore_list if threads < 1)
       error("Bad threads value < 1: " + threads)
     for ((_, processes) <- multicore_list if processes < 1)
       error("Bad processes value < 1: " + processes)
 
     if (heap < 100) error("Bad heap value < 100: " + heap)
 
     if (max_heap.isDefined && max_heap.get < heap)
       error("Bad max_heap value < heap: " + max_heap.get)
 
     System.getenv("ISABELLE_SETTINGS_PRESENT") match {
       case null | "" =>
       case _ => error("Cannot run build_history within existing Isabelle settings environment")
     }
 
 
     /* checkout Isabelle + AFP repository */
 
     def checkout(dir: Path, version: String): String =
     {
       val hg = Mercurial.repository(dir)
       hg.update(rev = version, clean = true)
       progress.echo_if(verbose, hg.log(version, options = "-l1"))
       hg.id(rev = version)
     }
 
     val isabelle_version = checkout(root, rev)
 
     val afp_repos = root + Path.explode("AFP")
     val afp_version = afp_rev.map(checkout(afp_repos, _))
 
     val (afp_build_args, afp_sessions) =
       if (afp_rev.isEmpty) (Nil, Nil)
       else {
         val afp = AFP.init(options, afp_repos)
         (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
       }
 
 
     /* main */
 
     val other_isabelle =
       Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
         user_home = user_home, progress = progress)
 
     val build_host = Isabelle_System.hostname()
     val build_history_date = Date.now()
     val build_group_id = build_host + ":" + build_history_date.time.ms
 
     var first_build = true
     for ((threads, processes) <- multicore_list) yield
     {
       /* init settings */
 
       other_isabelle.init_settings(components_base, nonfree, init_settings)
       other_isabelle.resolve_components(verbose)
       val ml_platform =
         augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings)
 
       val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
       val isabelle_output_log = isabelle_output + Path.explode("log")
       val isabelle_base_log = isabelle_output + Path.explode("../base_log")
 
       if (first_build) {
         other_isabelle.resolve_components(verbose)
 
         if (fresh)
           Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes"))
         other_isabelle.bash(
           "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " +
             "bin/isabelle jedit -b", redirect = true, echo = verbose).check
 
         Isabelle_System.rm_tree(isabelle_base_log)
       }
 
       Isabelle_System.rm_tree(isabelle_output)
       Isabelle_System.mkdirs(isabelle_output)
 
       val log_path =
         other_isabelle.isabelle_home_user +
           Build_Log.log_subdir(build_history_date) +
           Build_Log.log_filename(Build_History.engine, build_history_date,
             List(build_host, ml_platform, "M" + threads) ::: build_tags)
 
       Isabelle_System.mkdirs(log_path.dir)
 
       val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out")
       val build_out_progress = new File_Progress(build_out)
       build_out.file.delete
 
 
       /* build */
 
       if (multicore_base && !first_build && isabelle_base_log.is_dir)
         Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log)
 
       val build_start = Date.now()
       val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args
       val build_result =
         Other_Isabelle(root, isabelle_identifier = isabelle_identifier,
           user_home = user_home, progress = build_out_progress)(
             "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true,
             strict = false)
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =
         Build_Log.Log_File(log_path.base_name, build_result.out_lines).
           parse_build_info(ml_statistics = true)
 
 
       /* output log */
 
       val store = Sessions.store()
 
       val meta_info =
         Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
         Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
         List(
           Build_Log.Prop.build_group_id.name -> build_group_id,
           Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms),
           Build_Log.Prop.build_engine.name -> Build_History.engine,
           Build_Log.Prop.build_host.name -> build_host,
           Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start),
           Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end),
           Build_Log.Prop.isabelle_version.name -> isabelle_version) :::
         afp_version.map(Build_Log.Prop.afp_version.name -> _).toList
 
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
 
             if (database.is_file) {
               using(SQLite.open_database(database))(db =>
               {
                 val theory_timings =
                   try {
                     store.read_theory_timings(db, session_name).map(ps =>
                       Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER,
                         (Build_Log.SESSION_NAME, session_name) :: ps))
                   }
                   catch { case ERROR(_) => Nil }
 
                 val session_sources =
                   store.read_build(db, session_name).map(_.sources) match {
                     case Some(sources) if sources.length == SHA1.digest_length =>
                       List("Sources " + session_name + " " + sources)
                     case _ => Nil
                   }
 
                 theory_timings ::: session_sources
               })
             }
             else Nil
           })
 
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val log_gz = isabelle_output + store.log_gz(session_name)
 
             val properties =
               if (database.is_file) {
                 using(SQLite.open_database(database))(db =>
                   store.read_ml_statistics(db, session_name))
               }
               else if (log_gz.is_file) {
                 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
               }
               else Nil
 
             val trimmed_properties =
               if (ml_statistics_step <= 0) Nil
               else if (ml_statistics_step == 1) properties
               else {
                 (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 }
                  yield ps).toList
               }
 
             trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps)
           })
 
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
         build_info.failed_sessions.flatMap(session_name =>
           {
             val database = isabelle_output + store.database(session_name)
             val errors =
               if (database.is_file) {
                 try {
                   using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
                 } // column "errors" could be missing
                 catch { case _: java.sql.SQLException => Nil }
               }
               else Nil
             errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg))
           })
 
       build_out_progress.echo("Reading heap sizes ...")
       val heap_sizes =
         build_info.finished_sessions.flatMap(session_name =>
           {
             val heap = isabelle_output + Path.explode(session_name)
             if (heap.is_file)
               Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)")
             else None
           })
 
       build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...")
       File.write_xz(log_path.ext("xz"),
         terminate_lines(
           Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines :::
           session_build_info :::
           ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) :::
           session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) :::
           heap_sizes), XZ.options(6))
 
 
       /* next build */
 
       if (multicore_base && first_build && isabelle_output_log.is_dir)
         Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log)
 
       Isabelle_System.rm_tree(isabelle_output)
 
       first_build = false
 
       (build_result, log_path.ext("xz"))
     }
   }
 
 
   /* command line entry point */
 
   private object Multicore
   {
     private val Pat1 = """^(\d+)$""".r
     private val Pat2 = """^(\d+)x(\d+)$""".r
 
     def parse(s: String): (Int, Int) =
       s match {
         case Pat1(Value.Int(x)) => (x, 1)
         case Pat2(Value.Int(x), Value.Int(y)) => (x, y)
         case _ => error("Bad multicore configuration: " + quote(s))
       }
   }
 
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       var afp_rev: Option[String] = None
       var multicore_base = false
       var components_base = ""
       var heap: Option[Int] = None
       var max_heap: Option[Int] = None
       var multicore_list = List(default_multicore)
       var isabelle_identifier = default_isabelle_identifier
       var afp_partition = 0
       var more_settings: List[String] = Nil
       var fresh = false
       var init_settings: List[String] = Nil
       var arch_64 = false
       var nonfree = false
       var output_file = ""
       var rev = default_rev
       var ml_statistics_step = 1
       var build_tags = List.empty[String]
       var user_home = default_user_home
       var verbose = false
       var exit_code = false
 
       val getopts = Getopts("""
 Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...]
 
   Options are:
     -A REV       include $ISABELLE_HOME/AFP repository at given revision
     -B           first multicore build serves as base for scheduling information
     -C DIR       base directory for Isabelle components (default: $ISABELLE_HOME_USER/../contrib)
     -H SIZE      minimal ML heap in MB (default: """ + default_heap + """ for x86, """ +
       default_heap * 2 + """ for x86_64)
     -M MULTICORE multicore configurations (see below)
     -N NAME      alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """)
     -P NUMBER    AFP partition number (0, 1, 2, default: 0=unrestricted)
     -U SIZE      maximal ML heap in MB (default: unbounded)
     -e TEXT      additional text for generated etc/settings
     -f           fresh build of Isabelle/Scala components (recommended)
     -i TEXT      initial text for generated etc/settings
     -m ARCH      processor architecture (32=x86, 64=x86_64, default: x86)
     -n           include nonfree components
     -o FILE      output file for log names (default: stdout)
     -r REV       update to revision (default: """ + default_rev + """)
     -s NUMBER    step size for ML statistics (0=none, 1=all, n=step, default: 1)
     -t TAG       free-form build tag (multiple occurrences possible)
     -u DIR       alternative USER_HOME directory
     -v           verbose
     -x           return overall exit code from build processes
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
   passing ARGS directly to its isabelle build tool.
 
   Each MULTICORE configuration consists of one or two numbers (default 1):
   THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4.
 """,
         "A:" -> (arg => afp_rev = Some(arg)),
         "B" -> (_ => multicore_base = true),
         "C:" -> (arg => components_base = arg),
         "H:" -> (arg => heap = Some(Value.Int.parse(arg))),
         "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse(_))),
         "N:" -> (arg => isabelle_identifier = arg),
         "P:" -> (arg => afp_partition = Value.Int.parse(arg)),
         "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))),
         "e:" -> (arg => more_settings = more_settings ::: List(arg)),
         "f" -> (_ => fresh = true),
         "i:" -> (arg => init_settings = init_settings ::: List(arg)),
         "m:" ->
           {
             case "32" | "x86" => arch_64 = false
             case "64" | "x86_64" => arch_64 = true
             case bad => error("Bad processor architecture: " + quote(bad))
           },
         "n" -> (_ => nonfree = true),
         "o:" -> (arg => output_file = arg),
         "r:" -> (arg => rev = arg),
         "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)),
         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
         "u:" -> (arg => user_home = Path.explode(arg)),
         "v" -> (_ => verbose = true),
         "x" -> (_ => exit_code = true))
 
       val more_args = getopts(args)
       val (root, build_args) =
         more_args match {
           case root :: build_args => (Path.explode(root), build_args)
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress(stderr = true)
 
       val results =
         build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev,
           afp_rev = afp_rev, afp_partition = afp_partition,
           isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step,
           components_base = components_base, fresh = fresh, nonfree = nonfree,
           multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64,
           heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap),
           max_heap = max_heap, init_settings = init_settings, more_settings = more_settings,
           verbose = verbose, build_tags = build_tags, build_args = build_args)
 
       if (output_file == "") {
         for ((_, log_path) <- results)
           Output.writeln(log_path.implode, stdout = true)
       }
       else {
         File.write(Path.explode(output_file),
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0 && exit_code) sys.exit(rc)
     }
   }
 
 
 
   /** remote build_history -- via command-line **/
 
   def remote_build_history(
     ssh: SSH.Session,
     isabelle_repos_self: Path,
     isabelle_repos_other: Path,
-    isabelle_repos_source: String = "https://isabelle.in.tum.de/repos/isabelle",
+    isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
     afp_repos_source: String = AFP.repos_source,
     isabelle_identifier: String = "remote_build_history",
     self_update: Boolean = false,
     push_isabelle_home: Boolean = false,
     progress: Progress = No_Progress,
     rev: String = "",
     afp_rev: Option[String] = None,
     options: String = "",
     args: String = ""): List[(String, Bytes)] =
   {
     /* Isabelle self repository */
 
     val isabelle_hg =
       Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh)
 
     def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
       ssh.execute(
         Isabelle_System.export_isabelle_identifier(isabelle_identifier) +
           ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args,
         progress_stdout = progress.echo_if(echo, _),
         progress_stderr = progress.echo_if(echo, _),
         strict = strict).check
 
     if (self_update) {
       val self_rev =
         if (push_isabelle_home) {
           val isabelle_home_hg = Mercurial.repository(Path.explode("~~"))
           val self_rev = isabelle_home_hg.id()
           isabelle_home_hg.push(isabelle_hg.root_url, rev = self_rev, force = true)
           self_rev
         }
         else {
           isabelle_hg.pull()
           isabelle_hg.id()
         }
       isabelle_hg.update(rev = self_rev, clean = true)
       execute("bin/isabelle", "components -I")
       execute("bin/isabelle", "components -a", echo = true)
       execute("Admin/build", "jars_fresh")
     }
 
 
     /* Isabelle other + AFP repository */
 
     if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) {
       ssh.rm_tree(isabelle_repos_other)
     }
     val other_hg =
       Mercurial.clone_repository(
         ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev, ssh = ssh)
 
     val afp_options =
       if (afp_rev.isEmpty) ""
       else {
         val afp_repos = isabelle_repos_other + Path.explode("AFP")
         val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
         " -A " + Bash.string(afp_rev.get)
       }
 
 
     /* Admin/build_history */
 
     ssh.with_tmp_dir(tmp_dir =>
     {
       val output_file = tmp_dir + Path.explode("output")
 
       execute("Admin/build_history",
         "-o " + ssh.bash_path(output_file) +
           (if (rev == "") "" else " -r " + Bash.string(rev)) + " " +
           options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
         echo = true, strict = false)
 
       for (line <- split_lines(ssh.read(output_file)))
       yield {
         val log = Path.explode(line)
         val bytes = ssh.read_bytes(log)
         ssh.rm(log)
         (log.base_name, bytes)
       }
     })
   }
 }
diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala
+++ b/src/Pure/Admin/isabelle_cronjob.scala
@@ -1,548 +1,549 @@
 /*  Title:      Pure/Admin/isabelle_cronjob.scala
     Author:     Makarius
 
 Main entry point for administrative cronjob at TUM.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 
 
 object Isabelle_Cronjob
 {
   /* global resources: owned by main cronjob */
 
   val main_dir = Path.explode("~/cronjob")
   val main_state_file = main_dir + Path.explode("run/main.state")
   val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
   val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
 
+  val isabelle_repos_source = "https://isabelle.in.tum.de/repos/isabelle"
   val isabelle_repos = main_dir + Path.explode("isabelle")
   val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
   val afp_repos = main_dir + Path.explode("AFP")
 
   val build_log_dirs =
     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
 
 
 
   /** logger tasks **/
 
   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
 
 
   /* init and identify Isabelle + AFP repository snapshots */
 
+  def get_rev(): String = Mercurial.repository(isabelle_repos).id()
+  def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
+
   val init =
     Logger_Task("init", logger =>
       {
         Isabelle_Devel.make_index()
 
-        val rev = Mercurial.repository(isabelle_repos).id()
-        val afp_rev = Mercurial.setup_repository(AFP.repos_source, afp_repos).id()
+        Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
+        Mercurial.setup_repository(AFP.repos_source, afp_repos)
 
         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
-          Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
+          Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
       })
 
 
   /* build release */
 
   val build_release =
     Logger_Task("build_release", logger =>
       {
-        val rev = Mercurial.repository(isabelle_repos).id()
-        val afp_rev = Mercurial.repository(afp_repos).id()
-
-        Isabelle_Devel.release_snapshot(rev = rev, afp_rev = afp_rev,
+        Isabelle_Devel.release_snapshot(rev = get_rev(), afp_rev = get_afp_rev(),
           parallel_jobs = 4, remote_mac = "macbroy31")
       })
 
 
   /* integrity test of build_history vs. build_history_base */
 
   val build_history_base =
     Logger_Task("build_history_base", logger =>
       {
         val hg =
           Mercurial.setup_repository(
             File.standard_path(isabelle_repos), isabelle_repos_test)
         for {
           (result, log_path) <-
             Build_History.build_history(logger.options, isabelle_repos_test,
               rev = "build_history_base", fresh = true, build_args = List("HOL"))
         } {
           result.check
           File.move(log_path, logger.log_dir + log_path.base)
         }
       })
 
 
   /* remote build_history */
 
   sealed case class Item(
     known: Boolean,
     isabelle_version: String,
     afp_version: Option[String],
     pull_date: Date)
   {
     def unknown: Boolean = !known
     def versions: (String, Option[String]) = (isabelle_version, afp_version)
 
     def known_versions(rev: String, afp_rev: Option[String]): Boolean =
       known && rev != "" && isabelle_version == rev &&
       (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get)
   }
 
   def recent_items(db: SQL.Database,
     days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
   {
     val afp = afp_rev.isDefined
     val select =
       Build_Log.Data.select_recent_versions(
         days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
 
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
       {
         val known = res.bool(Build_Log.Data.known)
         val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
         val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
         val pull_date = res.date(Build_Log.Data.pull_date(afp))
         Item(known, isabelle_version, afp_version, pull_date)
       }).toList)
   }
 
   def unknown_runs(items: List[Item]): List[List[Item]] =
   {
     val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
     if (run.nonEmpty) run :: unknown_runs(rest) else Nil
   }
 
   sealed case class Remote_Build(
     description: String,
     host: String,
     user: String = "",
     port: Int = 0,
     ssh_host: String = "",
     proxy_host: String = "",
     proxy_user: String = "",
     proxy_port: Int = 0,
     shared_home: Boolean = true,
     historic: Boolean = false,
     history: Int = 0,
     history_base: String = "build_history_base",
     options: String = "",
     args: String = "",
     afp: Boolean = false,
     slow: Boolean = false,
     more_hosts: List[String] = Nil,
     detect: SQL.Source = "",
     active: Boolean = true)
   {
     def ssh_session(context: SSH.Context): SSH.Session =
       context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port,
         proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port)
 
     def sql: SQL.Source =
       Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
       SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
       (if (detect == "") "" else " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
       Build_Status.Profile(description, history = history, afp = afp, slow = slow, sql = sql)
 
     def pick(
       options: Options,
       rev: String = "",
       filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
     {
-      val afp_rev = if (afp) Some(Mercurial.repository(afp_repos).id()) else None
+      val afp_rev = if (afp) Some(get_afp_rev()) else None
 
       val store = Build_Log.store(options)
       using(store.open_database())(db =>
       {
         def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
         {
           val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
           def runs = unknown_runs(items).filter(run => run.length >= gap)
 
           if (historic || items.exists(_.known_versions(rev, afp_rev))) {
             val longest_run =
               (List.empty[Item] /: runs)({ case (item1, item2) =>
                 if (item1.length >= item2.length) item1 else item2
               })
             if (longest_run.isEmpty) None
             else Some(longest_run(longest_run.length / 2).versions)
           }
           else if (rev != "") Some((rev, afp_rev))
           else runs.flatten.headOption.map(_.versions)
         }
 
         pick_days(options.int("build_log_history") max history, 2) orElse
         pick_days(200, 5) orElse
         pick_days(2000, 1)
       })
     }
   }
 
   val remote_builds_old: List[Remote_Build] =
     List(
       Remote_Build("AFP", "lxbroy7",
           args = "-N -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
       Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
         history_base = "37074e22e8be",
         options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
         args = "-N -g timing",
         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " +
           Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
       Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
         history_base = "a9d5b59c3e12",
         options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
         args = "-N -g timing",
         detect =
           Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
           Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
       Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
         history_base = "37074e22e8be",
         options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
         args = "-a",
         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
       Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
         history_base = "a9d5b59c3e12",
         options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
         args = "-a",
         detect =
         Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
         Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
       Remote_Build("Poly/ML test", "lxbroy8",
         options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
         args = "-N -g timing",
         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
       Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
         detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
 
 
   val remote_builds1: List[List[Remote_Build]] =
   {
     List(
       List(Remote_Build("Linux A", "lxbroy9",
         options = "-m32 -B -M1x2,2", args = "-N -g timing")),
       List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
         options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
       List(
         Remote_Build("Mac OS X", "macbroy2",
           options = "-m32 -M8" +
             " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
             " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml",
           args = "-a",
           detect = Build_Log.Prop.build_tags.undefined,
           history_base = "2c0f24e927dd"),
         Remote_Build("Mac OS X, quick_and_dirty", "macbroy2",
           options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"),
           history_base = "2c0f24e927dd"),
         Remote_Build("Mac OS X, skip_proofs", "macbroy2",
           options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"),
           history_base = "2c0f24e927dd")),
       List(
         Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a",
           detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
       List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")),
       List(
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, shared_home = false,
           options = "-m32 -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
             " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
           args = "-a",
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, shared_home = false,
           options = "-m64 -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
             " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
           args = "-a",
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
     ) :::
     {
       for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
       yield {
         List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail,
           options = "-m32 -M1x2 -t AFP -P" + n +
             " -e ISABELLE_GHC=ghc" +
             " -e ISABELLE_MLTON=mlton" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
             " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml",
           args = "-N -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
       }
     }
   }
 
   val remote_builds2: List[List[Remote_Build]] =
     List(
       List(
         Remote_Build("AFP slow", "lrzcloud1", shared_home = false,
           options = "-m64 -M6 -U30000 -s10 -t AFP",
           args = "-g slow",
           afp = true,
           slow = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
 
   def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
     : Logger_Task =
   {
     val task_name = "build_history-" + r.host
     Logger_Task(task_name, logger =>
       {
         using(r.ssh_session(logger.ssh_context))(ssh =>
           {
             val self_update = !r.shared_home
             val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
 
             val results =
               Build_History.remote_build_history(ssh,
                 isabelle_repos,
                 isabelle_repos.ext(r.host),
                 isabelle_identifier = "cronjob_build_history",
                 self_update = self_update,
                 push_isabelle_home = push_isabelle_home,
                 rev = rev,
                 afp_rev = afp_rev,
                 options =
                   " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
                   " -f " + r.options,
                 args = "-o timeout=10800 " + r.args)
 
             for ((log_name, bytes) <- results) {
               logger.log(Date.now(), log_name)
               Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
             }
           })
       })
   }
 
   val build_status_profiles: List[Build_Status.Profile] =
     (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
 
 
 
   /** task logging **/
 
   object Log_Service
   {
     def apply(options: Options, progress: Progress = No_Progress): Log_Service =
       new Log_Service(SSH.init_context(options), progress)
   }
 
   class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
   {
     current_log.file.delete
 
     private val thread: Consumer_Thread[String] =
       Consumer_Thread.fork("cronjob: logger", daemon = true)(
         consume = (text: String) =>
           { // critical
             File.append(current_log, text + "\n")
             File.append(cumulative_log, text + "\n")
             progress.echo(text)
             true
           })
 
     def shutdown() { thread.shutdown() }
 
     val hostname = Isabelle_System.hostname()
 
     def log(date: Date, task_name: String, msg: String): Unit =
       if (task_name != "")
         thread.send(
           "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
 
     def start_logger(start_date: Date, task_name: String): Logger =
       new Logger(this, start_date, task_name)
 
     def run_task(start_date: Date, task: Logger_Task)
     {
       val logger = start_logger(start_date, task.name)
       val res = Exn.capture { task.body(logger) }
       val end_date = Date.now()
       val err =
         res match {
           case Exn.Res(_) => None
           case Exn.Exn(exn) =>
             Output.writeln("Exception trace for " + quote(task.name) + ":")
             exn.printStackTrace()
             val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
             Some(first_line)
         }
       logger.log_end(end_date, err)
     }
 
     def fork_task(start_date: Date, task: Logger_Task): Task =
       new Task(task.name, run_task(start_date, task))
   }
 
   class Logger private[Isabelle_Cronjob](
     val log_service: Log_Service, val start_date: Date, val task_name: String)
   {
     def ssh_context: SSH.Context = log_service.ssh_context
     def options: Options = ssh_context.options
 
     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
 
     def log_end(end_date: Date, err: Option[String])
     {
       val elapsed_time = end_date.time - start_date.time
       val msg =
         (if (err.isEmpty) "finished" else "ERROR " + err.get) +
         (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
       log(end_date, msg)
     }
 
     val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
 
     Isabelle_System.mkdirs(log_dir)
     log(start_date, "started")
   }
 
   class Task private[Isabelle_Cronjob](name: String, body: => Unit)
   {
     private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
     def is_finished: Boolean = future.is_finished
   }
 
 
 
   /** cronjob **/
 
   def cronjob(progress: Progress, exclude_task: Set[String])
   {
     /* soft lock */
 
     val still_running =
       try { Some(File.read(main_state_file)) }
       catch { case ERROR(_) => None }
 
     still_running match {
       case None | Some("") =>
       case Some(running) =>
         error("Isabelle cronjob appears to be still running: " + running)
     }
 
 
     /* log service */
 
     val log_service = Log_Service(Options.init(), progress = progress)
 
     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
 
     def run_now(task: Logger_Task) { run(Date.now(), task) }
 
 
     /* structured tasks */
 
     def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
       for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
         run_now(task))
 
     def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
       {
         @tailrec def join(running: List[Task])
         {
           running.partition(_.is_finished) match {
             case (Nil, Nil) =>
             case (Nil, _ :: _) => Thread.sleep(500); join(running)
             case (_ :: _, remaining) => join(remaining)
           }
         }
         val start_date = Date.now()
         val running =
           for (task <- tasks if !exclude_task(task.name))
             yield log_service.fork_task(start_date, task)
         join(running)
       })
 
 
     /* repository structure */
 
     val hg = Mercurial.repository(isabelle_repos)
     val hg_graph = hg.graph()
 
     def history_base_filter(r: Remote_Build): Item => Boolean =
     {
       val base_rev = hg.id(r.history_base)
       val nodes = hg_graph.all_succs(List(base_rev)).toSet
       (item: Item) => nodes(item.isabelle_version)
     }
 
 
     /* main */
 
     val main_start_date = Date.now()
     File.write(main_state_file, main_start_date + " " + log_service.hostname)
 
     run(main_start_date,
       Logger_Task("isabelle_cronjob", logger =>
         run_now(
           SEQ(List(init, build_release, build_history_base,
             PAR(List(remote_builds1, remote_builds2).map(remote_builds =>
               SEQ(List(
                 PAR(remote_builds.map(_.filter(_.active)).map(seq =>
                   SEQ(
                     for {
                       (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
                       (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
                     } yield remote_build_history(rev, afp_rev, i, r)))),
                 Logger_Task("jenkins_logs", _ =>
                   Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
                 Logger_Task("build_log_database",
                   logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
                 Logger_Task("build_status",
                   logger => Isabelle_Devel.build_status(logger.options)))))))))))
 
     log_service.shutdown()
 
     main_state_file.file.delete
   }
 
 
 
   /** command line entry point **/
 
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       var force = false
       var verbose = false
       var exclude_task = Set.empty[String]
 
       val getopts = Getopts("""
 Usage: Admin/cronjob/main [OPTIONS]
 
   Options are:
     -f           apply force to do anything
     -v           verbose
     -x NAME      exclude tasks with this name
 """,
         "f" -> (_ => force = true),
         "v" -> (_ => verbose = true),
         "x:" -> (arg => exclude_task += arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = if (verbose) new Console_Progress() else No_Progress
 
       if (force) cronjob(progress, exclude_task)
       else error("Need to apply force to do anything")
     }
   }
 }