src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Thu Mar 21 14:17:36 2019 +0100 (2 months ago)
changeset 69937 afbc075fd2da
parent 69931 31ee094dea3d
child 69952 385458b950e1
permissions -rw-r--r--
less ambitious test: lapbroy68 lacks libgmp-dev that is required for ocaml setup of zarith;
     1 /*  Title:      Pure/Admin/isabelle_cronjob.scala
     2     Author:     Makarius
     3 
     4 Main entry point for administrative cronjob at TUM.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.nio.file.Files
    11 
    12 import scala.annotation.tailrec
    13 import scala.collection.mutable
    14 
    15 
    16 object Isabelle_Cronjob
    17 {
    18   /* global resources: owned by main cronjob */
    19 
    20   val backup = "lxbroy10:cronjob"
    21   val main_dir = Path.explode("~/cronjob")
    22   val main_state_file = main_dir + Path.explode("run/main.state")
    23   val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
    24   val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
    25 
    26   val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
    27   val isabelle_repos = main_dir + Path.explode("isabelle")
    28   val afp_repos = main_dir + Path.explode("AFP")
    29 
    30   val build_log_dirs =
    31     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
    32 
    33 
    34 
    35   /** logger tasks **/
    36 
    37   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    38 
    39 
    40   /* init and exit */
    41 
    42   def get_rev(): String = Mercurial.repository(isabelle_repos).id()
    43   def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
    44 
    45   val init =
    46     Logger_Task("init", logger =>
    47       {
    48         Isabelle_Devel.make_index()
    49 
    50         Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
    51         Mercurial.setup_repository(AFP.repos_source, afp_repos)
    52 
    53         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
    54           Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
    55 
    56         Isabelle_System.bash(
    57           """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
    58             Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
    59 
    60         if (!Isabelle_Devel.cronjob_log.is_file)
    61           Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
    62       })
    63 
    64   val exit =
    65     Logger_Task("exit", logger =>
    66       {
    67         Isabelle_System.bash(
    68           "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
    69             .check
    70       })
    71 
    72 
    73   /* build release */
    74 
    75   val build_release =
    76     Logger_Task("build_release", logger =>
    77       {
    78         Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
    79       })
    80 
    81 
    82   /* integrity test of build_history vs. build_history_base */
    83 
    84   val build_history_base =
    85     Logger_Task("build_history_base", logger =>
    86       {
    87         using(logger.ssh_context.open_session("lxbroy10"))(ssh =>
    88           {
    89             val results =
    90               Build_History.remote_build_history(ssh,
    91                 isabelle_repos,
    92                 isabelle_repos.ext("build_history_base"),
    93                 isabelle_identifier = "cronjob_build_history",
    94                 self_update = true,
    95                 rev = "build_history_base",
    96                 options = "-f",
    97                 args = "HOL")
    98 
    99             for ((log_name, bytes) <- results) {
   100               Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
   101             }
   102           })
   103       })
   104 
   105 
   106   /* remote build_history */
   107 
   108   sealed case class Item(
   109     known: Boolean,
   110     isabelle_version: String,
   111     afp_version: Option[String],
   112     pull_date: Date)
   113   {
   114     def unknown: Boolean = !known
   115     def versions: (String, Option[String]) = (isabelle_version, afp_version)
   116 
   117     def known_versions(rev: String, afp_rev: Option[String]): Boolean =
   118       known && rev != "" && isabelle_version == rev &&
   119       (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get)
   120   }
   121 
   122   def recent_items(db: SQL.Database,
   123     days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
   124   {
   125     val afp = afp_rev.isDefined
   126     val select =
   127       Build_Log.Data.select_recent_versions(
   128         days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
   129 
   130     db.using_statement(select)(stmt =>
   131       stmt.execute_query().iterator(res =>
   132       {
   133         val known = res.bool(Build_Log.Data.known)
   134         val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
   135         val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
   136         val pull_date = res.date(Build_Log.Data.pull_date(afp))
   137         Item(known, isabelle_version, afp_version, pull_date)
   138       }).toList)
   139   }
   140 
   141   def unknown_runs(items: List[Item]): List[List[Item]] =
   142   {
   143     val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
   144     if (run.nonEmpty) run :: unknown_runs(rest) else Nil
   145   }
   146 
   147   sealed case class Remote_Build(
   148     description: String,
   149     host: String,
   150     user: String = "",
   151     port: Int = 0,
   152     ssh_host: String = "",
   153     ssh_permissive: Boolean = false,
   154     proxy_host: String = "",
   155     proxy_user: String = "",
   156     proxy_port: Int = 0,
   157     self_update: Boolean = false,
   158     historic: Boolean = false,
   159     history: Int = 0,
   160     history_base: String = "build_history_base",
   161     options: String = "",
   162     args: String = "",
   163     afp: Boolean = false,
   164     bulky: Boolean = false,
   165     more_hosts: List[String] = Nil,
   166     detect: SQL.Source = "",
   167     active: Boolean = true)
   168   {
   169     def ssh_session(context: SSH.Context): SSH.Session =
   170       context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port,
   171         proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
   172         permissive = ssh_permissive)
   173 
   174     def sql: SQL.Source =
   175       Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
   176       SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
   177       (if (detect == "") "" else " AND " + SQL.enclose(detect))
   178 
   179     def profile: Build_Status.Profile =
   180       Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
   181 
   182     def pick(
   183       options: Options,
   184       rev: String = "",
   185       filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
   186     {
   187       val afp_rev = if (afp) Some(get_afp_rev()) else None
   188 
   189       val store = Build_Log.store(options)
   190       using(store.open_database())(db =>
   191       {
   192         def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
   193         {
   194           val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
   195           def runs = unknown_runs(items).filter(run => run.length >= gap)
   196 
   197           if (historic || items.exists(_.known_versions(rev, afp_rev))) {
   198             val longest_run =
   199               (List.empty[Item] /: runs)({ case (item1, item2) =>
   200                 if (item1.length >= item2.length) item1 else item2
   201               })
   202             if (longest_run.isEmpty) None
   203             else Some(longest_run(longest_run.length / 2).versions)
   204           }
   205           else if (rev != "") Some((rev, afp_rev))
   206           else runs.flatten.headOption.map(_.versions)
   207         }
   208 
   209         pick_days(options.int("build_log_history") max history, 2) orElse
   210         pick_days(200, 5) orElse
   211         pick_days(2000, 1)
   212       })
   213     }
   214   }
   215 
   216   val remote_builds_old: List[Remote_Build] =
   217     List(
   218       Remote_Build("AFP", "lxbroy7",
   219           args = "-N -X large -X slow",
   220           afp = true,
   221           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
   222       Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
   223         history_base = "37074e22e8be",
   224         options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
   225         args = "-N -g timing",
   226         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " +
   227           Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
   228       Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
   229         history_base = "a9d5b59c3e12",
   230         options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
   231         args = "-N -g timing",
   232         detect =
   233           Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
   234           Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
   235       Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
   236         history_base = "37074e22e8be",
   237         options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
   238         args = "-a",
   239         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
   240       Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
   241         history_base = "a9d5b59c3e12",
   242         options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
   243         args = "-a",
   244         detect =
   245         Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
   246         Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
   247       Remote_Build("Poly/ML test", "lxbroy8",
   248         options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
   249         args = "-N -g timing",
   250         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
   251       Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
   252         detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
   253 
   254   val remote_builds1: List[List[Remote_Build]] =
   255   {
   256     List(
   257       List(Remote_Build("Linux A", "lxbroy9",
   258         options = "-m32 -B -M1x2,2", args = "-N -g timing")),
   259       List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
   260         options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
   261       List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
   262         options = "-m32 -B -M1x2,2 -t Benchmarks" +
   263             " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
   264             " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true -e ISABELLE_SMLNJ=sml" +
   265             " -e ISABELLE_SWIPL=swipl",
   266           args = "-N -a -d '~~/src/Benchmarks'",
   267           detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
   268       List(
   269         Remote_Build("Mac OS X", "macbroy2",
   270           options = "-m32 -M8" +
   271             " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
   272             " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
   273             " -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml",
   274           args = "-a",
   275           detect = Build_Log.Prop.build_tags.undefined,
   276           history_base = "2c0f24e927dd"),
   277         Remote_Build("Mac OS X, quick_and_dirty", "macbroy2",
   278           options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
   279           detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"),
   280           history_base = "2c0f24e927dd"),
   281         Remote_Build("Mac OS X, skip_proofs", "macbroy2",
   282           options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
   283           detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"),
   284           history_base = "2c0f24e927dd")),
   285       List(
   286         Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a",
   287           detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
   288       List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")),
   289       List(Remote_Build("Mac OS X 10.14 High Sierra", "lapbroy68", self_update = true,
   290         options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true",
   291         args = "-a -d '~~/src/Benchmarks'")),
   292       List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3", self_update = true,
   293         options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true",
   294         args = "-a -d '~~/src/Benchmarks'")),
   295       List(
   296         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
   297           options = "-m32 -M4" +
   298             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
   299             " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
   300             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
   301           args = "-a",
   302           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
   303         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
   304           options = "-m64 -M4" +
   305             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
   306             " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
   307             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
   308           args = "-a",
   309           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
   310     ) :::
   311     {
   312       for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
   313       yield {
   314         List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail,
   315           options = "-m32 -M1x2 -t AFP -P" + n +
   316             " -e ISABELLE_GHC=ghc" +
   317             " -e ISABELLE_MLTON=mlton" +
   318             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
   319             " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml",
   320           args = "-N -X large -X slow",
   321           afp = true,
   322           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
   323       }
   324     }
   325   }
   326 
   327   val remote_builds2: List[List[Remote_Build]] =
   328     List(
   329       List(
   330         Remote_Build("AFP bulky", "lrzcloud1", self_update = true,
   331           proxy_host = "lxbroy10", proxy_user = "i21isatest",
   332           ssh_host = "10.155.208.96", ssh_permissive = true,
   333           options = "-m64 -M6 -U30000 -s10 -t AFP",
   334           args = "-g large -g slow",
   335           afp = true,
   336           bulky = true,
   337           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
   338 
   339   def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
   340     : Logger_Task =
   341   {
   342     val task_name = "build_history-" + r.host
   343     Logger_Task(task_name, logger =>
   344       {
   345         using(r.ssh_session(logger.ssh_context))(ssh =>
   346           {
   347             val results =
   348               Build_History.remote_build_history(ssh,
   349                 isabelle_repos,
   350                 isabelle_repos.ext(r.host),
   351                 isabelle_identifier = "cronjob_build_history",
   352                 self_update = r.self_update,
   353                 rev = rev,
   354                 afp_rev = afp_rev,
   355                 options =
   356                   " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
   357                   " -f -h " + Bash.string(r.host) + " " + r.options,
   358                 args = "-o timeout=10800 " + r.args)
   359 
   360             for ((log_name, bytes) <- results) {
   361               logger.log(Date.now(), log_name)
   362               Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
   363             }
   364           })
   365       })
   366   }
   367 
   368   val build_status_profiles: List[Build_Status.Profile] =
   369     (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
   370 
   371 
   372 
   373   /** task logging **/
   374 
   375   object Log_Service
   376   {
   377     def apply(options: Options, progress: Progress = No_Progress): Log_Service =
   378       new Log_Service(SSH.init_context(options), progress)
   379   }
   380 
   381   class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
   382   {
   383     current_log.file.delete
   384 
   385     private val thread: Consumer_Thread[String] =
   386       Consumer_Thread.fork("cronjob: logger", daemon = true)(
   387         consume = (text: String) =>
   388           { // critical
   389             File.append(current_log, text + "\n")
   390             File.append(cumulative_log, text + "\n")
   391             progress.echo(text)
   392             true
   393           })
   394 
   395     def shutdown() { thread.shutdown() }
   396 
   397     val hostname = Isabelle_System.hostname()
   398 
   399     def log(date: Date, task_name: String, msg: String): Unit =
   400       if (task_name != "")
   401         thread.send(
   402           "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
   403 
   404     def start_logger(start_date: Date, task_name: String): Logger =
   405       new Logger(this, start_date, task_name)
   406 
   407     def run_task(start_date: Date, task: Logger_Task)
   408     {
   409       val logger = start_logger(start_date, task.name)
   410       val res = Exn.capture { task.body(logger) }
   411       val end_date = Date.now()
   412       val err =
   413         res match {
   414           case Exn.Res(_) => None
   415           case Exn.Exn(exn) =>
   416             Output.writeln("Exception trace for " + quote(task.name) + ":")
   417             exn.printStackTrace()
   418             val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
   419             Some(first_line)
   420         }
   421       logger.log_end(end_date, err)
   422     }
   423 
   424     def fork_task(start_date: Date, task: Logger_Task): Task =
   425       new Task(task.name, run_task(start_date, task))
   426   }
   427 
   428   class Logger private[Isabelle_Cronjob](
   429     val log_service: Log_Service, val start_date: Date, val task_name: String)
   430   {
   431     def ssh_context: SSH.Context = log_service.ssh_context
   432     def options: Options = ssh_context.options
   433 
   434     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
   435 
   436     def log_end(end_date: Date, err: Option[String])
   437     {
   438       val elapsed_time = end_date.time - start_date.time
   439       val msg =
   440         (if (err.isEmpty) "finished" else "ERROR " + err.get) +
   441         (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
   442       log(end_date, msg)
   443     }
   444 
   445     val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
   446 
   447     Isabelle_System.mkdirs(log_dir)
   448     log(start_date, "started")
   449   }
   450 
   451   class Task private[Isabelle_Cronjob](name: String, body: => Unit)
   452   {
   453     private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
   454     def is_finished: Boolean = future.is_finished
   455   }
   456 
   457 
   458 
   459   /** cronjob **/
   460 
   461   def cronjob(progress: Progress, exclude_task: Set[String])
   462   {
   463     /* soft lock */
   464 
   465     val still_running =
   466       try { Some(File.read(main_state_file)) }
   467       catch { case ERROR(_) => None }
   468 
   469     still_running match {
   470       case None | Some("") =>
   471       case Some(running) =>
   472         error("Isabelle cronjob appears to be still running: " + running)
   473     }
   474 
   475 
   476     /* log service */
   477 
   478     val log_service = Log_Service(Options.init(), progress = progress)
   479 
   480     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
   481 
   482     def run_now(task: Logger_Task) { run(Date.now(), task) }
   483 
   484 
   485     /* structured tasks */
   486 
   487     def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
   488       for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
   489         run_now(task))
   490 
   491     def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
   492       {
   493         @tailrec def join(running: List[Task])
   494         {
   495           running.partition(_.is_finished) match {
   496             case (Nil, Nil) =>
   497             case (Nil, _ :: _) => Thread.sleep(500); join(running)
   498             case (_ :: _, remaining) => join(remaining)
   499           }
   500         }
   501         val start_date = Date.now()
   502         val running =
   503           for (task <- tasks if !exclude_task(task.name))
   504             yield log_service.fork_task(start_date, task)
   505         join(running)
   506       })
   507 
   508 
   509     /* repository structure */
   510 
   511     val hg = Mercurial.repository(isabelle_repos)
   512     val hg_graph = hg.graph()
   513 
   514     def history_base_filter(r: Remote_Build): Item => Boolean =
   515     {
   516       val base_rev = hg.id(r.history_base)
   517       val nodes = hg_graph.all_succs(List(base_rev)).toSet
   518       (item: Item) => nodes(item.isabelle_version)
   519     }
   520 
   521 
   522     /* main */
   523 
   524     val main_start_date = Date.now()
   525     File.write(main_state_file, main_start_date + " " + log_service.hostname)
   526 
   527     run(main_start_date,
   528       Logger_Task("isabelle_cronjob", logger =>
   529         run_now(
   530           SEQ(List(
   531             init,
   532             build_history_base,
   533             PAR(
   534               build_release ::
   535               List(remote_builds1, remote_builds2).map(remote_builds =>
   536               SEQ(List(
   537                 PAR(remote_builds.map(_.filter(_.active)).map(seq =>
   538                   SEQ(
   539                     for {
   540                       (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
   541                       (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
   542                     } yield remote_build_history(rev, afp_rev, i, r)))),
   543                 Logger_Task("jenkins_logs", _ =>
   544                   Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
   545                 Logger_Task("build_log_database",
   546                   logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
   547                 Logger_Task("build_status",
   548                   logger => Isabelle_Devel.build_status(logger.options)))))),
   549             exit)))))
   550 
   551     log_service.shutdown()
   552 
   553     main_state_file.file.delete
   554   }
   555 
   556 
   557 
   558   /** command line entry point **/
   559 
   560   def main(args: Array[String])
   561   {
   562     Command_Line.tool0 {
   563       var force = false
   564       var verbose = false
   565       var exclude_task = Set.empty[String]
   566 
   567       val getopts = Getopts("""
   568 Usage: Admin/cronjob/main [OPTIONS]
   569 
   570   Options are:
   571     -f           apply force to do anything
   572     -v           verbose
   573     -x NAME      exclude tasks with this name
   574 """,
   575         "f" -> (_ => force = true),
   576         "v" -> (_ => verbose = true),
   577         "x:" -> (arg => exclude_task += arg))
   578 
   579       val more_args = getopts(args)
   580       if (more_args.nonEmpty) getopts.usage()
   581 
   582       val progress = if (verbose) new Console_Progress() else No_Progress
   583 
   584       if (force) cronjob(progress, exclude_task)
   585       else error("Need to apply force to do anything")
   586     }
   587   }
   588 }