1/* Title: Pure/Admin/isabelle_cronjob.scala 2 Author: Makarius 3 4Main entry point for administrative cronjob at TUM. 5*/ 6 7package isabelle 8 9 10import java.nio.file.Files 11 12import scala.annotation.tailrec 13import scala.collection.mutable 14 15 16object 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) 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 proxy_host: String = "", 154 proxy_user: String = "", 155 proxy_port: Int = 0, 156 self_update: Boolean = false, 157 historic: Boolean = false, 158 history: Int = 0, 159 history_base: String = "build_history_base", 160 options: String = "", 161 args: String = "", 162 afp: Boolean = false, 163 bulky: Boolean = false, 164 more_hosts: List[String] = Nil, 165 detect: SQL.Source = "", 166 active: Boolean = true) 167 { 168 def ssh_session(context: SSH.Context): SSH.Session = 169 context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port, 170 proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, 171 permissive = proxy_host.nonEmpty) 172 173 def sql: SQL.Source = 174 Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " + 175 SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) + 176 (if (detect == "") "" else " AND " + SQL.enclose(detect)) 177 178 def profile: Build_Status.Profile = 179 Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql) 180 181 def pick( 182 options: Options, 183 rev: String = "", 184 filter: Item => Boolean = _ => true): Option[(String, Option[String])] = 185 { 186 val afp_rev = if (afp) Some(get_afp_rev()) else None 187 188 val store = Build_Log.store(options) 189 using(store.open_database())(db => 190 { 191 def pick_days(days: Int, gap: Int): Option[(String, Option[String])] = 192 { 193 val items = recent_items(db, days, rev, afp_rev, sql).filter(filter) 194 def runs = unknown_runs(items).filter(run => run.length >= gap) 195 196 if (historic || items.exists(_.known_versions(rev, afp_rev))) { 197 val longest_run = 198 (List.empty[Item] /: runs)({ case (item1, item2) => 199 if (item1.length >= item2.length) item1 else item2 200 }) 201 if (longest_run.isEmpty) None 202 else Some(longest_run(longest_run.length / 2).versions) 203 } 204 else if (rev != "") Some((rev, afp_rev)) 205 else runs.flatten.headOption.map(_.versions) 206 } 207 208 pick_days(options.int("build_log_history") max history, 2) orElse 209 pick_days(200, 5) orElse 210 pick_days(2000, 1) 211 }) 212 } 213 } 214 215 val remote_builds_old: List[Remote_Build] = 216 List( 217 Remote_Build("AFP bulky", "lrzcloud1", self_update = true, 218 proxy_host = "lxbroy10", proxy_user = "i21isatest", 219 ssh_host = "10.155.208.96", 220 options = "-m64 -M6 -U30000 -s10 -t AFP", 221 args = "-g large -g slow", 222 afp = true, 223 bulky = true, 224 detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), 225 Remote_Build("AFP", "lxbroy7", 226 args = "-N -X large -X slow", 227 afp = true, 228 detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), 229 Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", 230 history_base = "37074e22e8be", 231 options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", 232 args = "-N -g timing", 233 detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " + 234 Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")), 235 Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8", 236 history_base = "a9d5b59c3e12", 237 options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", 238 args = "-N -g timing", 239 detect = 240 Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + 241 Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), 242 Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2", 243 history_base = "37074e22e8be", 244 options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'", 245 args = "-a", 246 detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")), 247 Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2", 248 history_base = "a9d5b59c3e12", 249 options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'", 250 args = "-a", 251 detect = 252 Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " + 253 Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")), 254 Remote_Build("Poly/ML test", "lxbroy8", 255 options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'", 256 args = "-N -g timing", 257 detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")), 258 Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a", 259 detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) 260 261 val remote_builds1: List[List[Remote_Build]] = 262 { 263 List( 264 List(Remote_Build("Linux A", "lxbroy9", 265 options = "-m32 -B -M1x2,2", args = "-N -g timing")), 266 List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90, 267 options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")), 268 List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90, 269 options = "-m32 -B -M1x2,2 -t Benchmarks" + 270 " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + 271 " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" + 272 " -e ISABELLE_SWIPL=swipl", 273 args = "-N -a -d '~~/src/Benchmarks'", 274 detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))), 275 List( 276 Remote_Build("Mac OS X", "macbroy2", 277 options = "-m32 -M8" + 278 " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" + 279 " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + 280 " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" + 281 " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml", 282 args = "-a", 283 detect = Build_Log.Prop.build_tags.undefined, 284 history_base = "2c0f24e927dd"), 285 Remote_Build("Mac OS X, quick_and_dirty", "macbroy2", 286 options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty", 287 detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"), 288 history_base = "2c0f24e927dd"), 289 Remote_Build("Mac OS X, skip_proofs", "macbroy2", 290 options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs", 291 detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"), 292 history_base = "2c0f24e927dd")), 293 List( 294 Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a", 295 detect = Build_Log.Prop.build_start + " > date '2017-03-03'")), 296 List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")), 297 List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68", 298 options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true", 299 self_update = true, args = "-a -d '~~/src/Benchmarks'")), 300 List(Remote_Build("macOS 10.14 Mojave", "lapnipkow3", 301 options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true", 302 self_update = true, args = "-a -d '~~/src/Benchmarks'")), 303 List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius", 304 proxy_host = "laraserver", proxy_user = "makarius", 305 self_update = true, options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true", 306 args = "-a -d '~~/src/Benchmarks'")), 307 List( 308 Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, 309 options = "-m32 -M4" + 310 " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + 311 " -e ISABELLE_GHC_SETUP=true" + 312 " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", 313 args = "-a", 314 detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")), 315 Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true, 316 options = "-m64 -M4" + 317 " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + 318 " -e ISABELLE_GHC_SETUP=true" + 319 " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml", 320 args = "-a", 321 detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))) 322 ) ::: 323 { 324 for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) } 325 yield { 326 List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail, 327 options = "-m32 -M1x2 -t AFP -P" + n + 328 " -e ISABELLE_GHC=ghc" + 329 " -e ISABELLE_MLTON=mlton" + 330 " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + 331 " -e ISABELLE_SMLNJ=sml", 332 args = "-N -X large -X slow", 333 afp = true, 334 detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))) 335 } 336 } 337 } 338 339 val remote_builds2: List[List[Remote_Build]] = 340 List( 341 List( 342 Remote_Build("AFP2", "lrzcloud2", self_update = true, 343 proxy_host = "lxbroy10", proxy_user = "i21isatest", 344 ssh_host = "10.195.2.10", 345 options = "-m32 -M1x8 -t AFP" + 346 " -e ISABELLE_GHC=ghc" + 347 " -e ISABELLE_MLTON=mlton" + 348 " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" + 349 " -e ISABELLE_SMLNJ=sml", 350 args = "-a -X large -X slow", 351 afp = true, 352 detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")), 353 Remote_Build("AFP bulky2", "lrzcloud2", self_update = true, 354 proxy_host = "lxbroy10", proxy_user = "i21isatest", 355 ssh_host = "10.195.2.10", 356 options = "-m64 -M8 -U30000 -s10 -t AFP", 357 args = "-g large -g slow", 358 afp = true, 359 bulky = true, 360 detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))) 361 362 def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build) 363 : Logger_Task = 364 { 365 val task_name = "build_history-" + r.host 366 Logger_Task(task_name, logger => 367 { 368 using(r.ssh_session(logger.ssh_context))(ssh => 369 { 370 val results = 371 Build_History.remote_build_history(ssh, 372 isabelle_repos, 373 isabelle_repos.ext(r.host), 374 isabelle_identifier = "cronjob_build_history", 375 self_update = r.self_update, 376 rev = rev, 377 afp_rev = afp_rev, 378 options = 379 " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + 380 " -f -h " + Bash.string(r.host) + " " + r.options, 381 args = "-o timeout=10800 " + r.args) 382 383 for ((log_name, bytes) <- results) { 384 logger.log(Date.now(), log_name) 385 Bytes.write(logger.log_dir + Path.explode(log_name), bytes) 386 } 387 }) 388 }) 389 } 390 391 val build_status_profiles: List[Build_Status.Profile] = 392 (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile) 393 394 395 396 /** task logging **/ 397 398 object Log_Service 399 { 400 def apply(options: Options, progress: Progress = No_Progress): Log_Service = 401 new Log_Service(SSH.init_context(options), progress) 402 } 403 404 class Log_Service private(val ssh_context: SSH.Context, progress: Progress) 405 { 406 current_log.file.delete 407 408 private val thread: Consumer_Thread[String] = 409 Consumer_Thread.fork("cronjob: logger", daemon = true)( 410 consume = (text: String) => 411 { // critical 412 File.append(current_log, text + "\n") 413 File.append(cumulative_log, text + "\n") 414 progress.echo(text) 415 true 416 }) 417 418 def shutdown() { thread.shutdown() } 419 420 val hostname = Isabelle_System.hostname() 421 422 def log(date: Date, task_name: String, msg: String): Unit = 423 if (task_name != "") 424 thread.send( 425 "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) 426 427 def start_logger(start_date: Date, task_name: String): Logger = 428 new Logger(this, start_date, task_name) 429 430 def run_task(start_date: Date, task: Logger_Task) 431 { 432 val logger = start_logger(start_date, task.name) 433 val res = Exn.capture { task.body(logger) } 434 val end_date = Date.now() 435 val err = 436 res match { 437 case Exn.Res(_) => None 438 case Exn.Exn(exn) => 439 Output.writeln("Exception trace for " + quote(task.name) + ":") 440 exn.printStackTrace() 441 val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" 442 Some(first_line) 443 } 444 logger.log_end(end_date, err) 445 } 446 447 def fork_task(start_date: Date, task: Logger_Task): Task = 448 new Task(task.name, run_task(start_date, task)) 449 } 450 451 class Logger private[Isabelle_Cronjob]( 452 val log_service: Log_Service, val start_date: Date, val task_name: String) 453 { 454 def ssh_context: SSH.Context = log_service.ssh_context 455 def options: Options = ssh_context.options 456 457 def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg) 458 459 def log_end(end_date: Date, err: Option[String]) 460 { 461 val elapsed_time = end_date.time - start_date.time 462 val msg = 463 (if (err.isEmpty) "finished" else "ERROR " + err.get) + 464 (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)") 465 log(end_date, msg) 466 } 467 468 val log_dir: Path = main_dir + Build_Log.log_subdir(start_date) 469 470 Isabelle_System.mkdirs(log_dir) 471 log(start_date, "started") 472 } 473 474 class Task private[Isabelle_Cronjob](name: String, body: => Unit) 475 { 476 private val future: Future[Unit] = Future.thread("cronjob: " + name) { body } 477 def is_finished: Boolean = future.is_finished 478 } 479 480 481 482 /** cronjob **/ 483 484 def cronjob(progress: Progress, exclude_task: Set[String]) 485 { 486 /* soft lock */ 487 488 val still_running = 489 try { Some(File.read(main_state_file)) } 490 catch { case ERROR(_) => None } 491 492 still_running match { 493 case None | Some("") => 494 case Some(running) => 495 error("Isabelle cronjob appears to be still running: " + running) 496 } 497 498 499 /* log service */ 500 501 val log_service = Log_Service(Options.init(), progress = progress) 502 503 def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) } 504 505 def run_now(task: Logger_Task) { run(Date.now(), task) } 506 507 508 /* structured tasks */ 509 510 def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => 511 for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "") 512 run_now(task)) 513 514 def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ => 515 { 516 @tailrec def join(running: List[Task]) 517 { 518 running.partition(_.is_finished) match { 519 case (Nil, Nil) => 520 case (Nil, _ :: _) => Thread.sleep(500); join(running) 521 case (_ :: _, remaining) => join(remaining) 522 } 523 } 524 val start_date = Date.now() 525 val running = 526 for (task <- tasks if !exclude_task(task.name)) 527 yield log_service.fork_task(start_date, task) 528 join(running) 529 }) 530 531 532 /* repository structure */ 533 534 val hg = Mercurial.repository(isabelle_repos) 535 val hg_graph = hg.graph() 536 537 def history_base_filter(r: Remote_Build): Item => Boolean = 538 { 539 val base_rev = hg.id(r.history_base) 540 val nodes = hg_graph.all_succs(List(base_rev)).toSet 541 (item: Item) => nodes(item.isabelle_version) 542 } 543 544 545 /* main */ 546 547 val main_start_date = Date.now() 548 File.write(main_state_file, main_start_date + " " + log_service.hostname) 549 550 run(main_start_date, 551 Logger_Task("isabelle_cronjob", logger => 552 run_now( 553 SEQ(List( 554 init, 555 build_history_base, 556 build_release, 557 PAR( 558 List(remote_builds1, remote_builds2).map(remote_builds => 559 SEQ(List( 560 PAR(remote_builds.map(_.filter(_.active)).map(seq => 561 SEQ( 562 for { 563 (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex) 564 (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r)) 565 } yield remote_build_history(rev, afp_rev, i, r)))), 566 Logger_Task("jenkins_logs", _ => 567 Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)), 568 Logger_Task("build_log_database", 569 logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)), 570 Logger_Task("build_status", 571 logger => Isabelle_Devel.build_status(logger.options)))))), 572 exit))))) 573 574 log_service.shutdown() 575 576 main_state_file.file.delete 577 } 578 579 580 581 /** command line entry point **/ 582 583 def main(args: Array[String]) 584 { 585 Command_Line.tool0 { 586 var force = false 587 var verbose = false 588 var exclude_task = Set.empty[String] 589 590 val getopts = Getopts(""" 591Usage: Admin/cronjob/main [OPTIONS] 592 593 Options are: 594 -f apply force to do anything 595 -v verbose 596 -x NAME exclude tasks with this name 597""", 598 "f" -> (_ => force = true), 599 "v" -> (_ => verbose = true), 600 "x:" -> (arg => exclude_task += arg)) 601 602 val more_args = getopts(args) 603 if (more_args.nonEmpty) getopts.usage() 604 605 val progress = if (verbose) new Console_Progress() else No_Progress 606 607 if (force) cronjob(progress, exclude_task) 608 else error("Need to apply force to do anything") 609 } 610 } 611} 612