diff -r a0c2cbe2fc8e -r 568cd5123952 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 12 19:03:35 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 12 21:35:36 2016 +0200 @@ -20,19 +20,73 @@ val log_dir = main_dir + Path.explode("log") val main_state_file = run_dir + Path.explode("main.state") - val main_log = log_dir + Path.explode("main.log") // owned by logger + val main_log = log_dir + Path.explode("main.log") // owned by log service - /* managed repository clones */ + /* task logging */ + + sealed case class Logger_Task(name: String, body: Logger => Unit) - val isabelle_repos = main_dir + Path.explode("isabelle-build_history") - val afp_repos = main_dir + Path.explode("AFP-build_history") + class Log_Service private[Isabelle_Cronjob](progress: Progress) + { + private val thread: Consumer_Thread[String] = + Consumer_Thread.fork("cronjob: logger", daemon = true)( + consume = (text: String) => + { + File.append(main_log, text + "\n") // critical + progress.echo(text) + true + }) + + def shutdown() { thread.shutdown() } + + val hostname = Isabelle_System.hostname() + + def log(date: Date, task_name: String, msg: String): Unit = + 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 pull_repos(root: Path): String = + 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) => Some(Exn.message(exn)) + } + 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) { - val hg = Mercurial.repository(root) - hg.pull(options = "-q") - hg.identify("tip", options = "-i") + 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 " + elapsed_time.message_hms) + log(end_date, msg) + } + + 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 } @@ -41,44 +95,41 @@ /* identify repository snapshots */ - def isabelle_identify(start_date: Date) - { - val isabelle_id = pull_repos(isabelle_repos) - val afp_id = pull_repos(afp_repos) + val isabelle_repos = main_dir + Path.explode("isabelle-build_history") + val afp_repos = main_dir + Path.explode("AFP-build_history") + + 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 log_path = log_dir + Build_Log.log_path("isabelle_identify", start_date) - Isabelle_System.mkdirs(log_path.dir) - File.write(log_path, - Library.terminate_lines( - List("isabelle_identify: " + Build_Log.print_date(start_date), - "", - "Isabelle version: " + isabelle_id, - "AFP version: " + afp_id))) - } + val isabelle_id = pull_repos(isabelle_repos) + val afp_id = pull_repos(afp_repos) + + val log_path = log_dir + Build_Log.log_path("isabelle_identify", logger.start_date) + Isabelle_System.mkdirs(log_path.dir) + File.write(log_path, + Library.terminate_lines( + List("isabelle_identify: " + Build_Log.print_date(logger.start_date), + "", + "Isabelle version: " + isabelle_id, + "AFP version: " + afp_id))) + }) /** cronjob **/ - private class Task(val name: String, body: Date => Unit) - { - override def toString: String = "cronjob: " + name - - val start_date: Date = Date.now() - - private val future: Future[Unit] = Future.thread(toString) { body(start_date) } - def is_finished: Boolean = future.is_finished - - def success: Boolean = - future.join_result match { - case Exn.Res(_) => true - case Exn.Exn(_) => false - } - } + private val all_tasks = List(isabelle_identify) def cronjob(progress: Progress) { - /* check */ + /* soft lock */ val still_running = try { Some(File.read(main_state_file)) } @@ -90,69 +141,37 @@ error("Isabelle cronjob appears to be still running: " + running) } - - /* logger */ - - val hostname = Isabelle_System.hostname() - - val logger: Consumer_Thread[String] = - Consumer_Thread.fork("cronjob: logger", daemon = true)( - consume = (text: String) => - { - File.append(main_log, text + "\n") - progress.echo(text) - true - }) + val main_start_date = Date.now() + val log_service = new Log_Service(progress) - def log(date: Date, task_name: String, msg: String) - { - logger.send( - "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg) - } - - def log_start(task: Task) { log(task.start_date, task.name, "started") } - - def log_end(end_date: Date, task: Task) - { - val elapsed_time = end_date.time - task.start_date.time - val msg = - (if (task.success) "finished" else "FAILED") + - (if (elapsed_time.seconds < 3.0) "" else ", elapsed time " + elapsed_time.message_hms) - log(end_date, task.name, msg) - } + File.write(main_state_file, main_start_date + " " + log_service.hostname) - /* manage tasks */ + /* parallel tasks */ - def manage_tasks(task_specs: List[(String, Date => Unit)]) + def parallel_tasks(tasks: List[Logger_Task]) { @tailrec def await(running: List[Task]) { running.partition(_.is_finished) match { case (Nil, Nil) => case (Nil, _ :: _) => Thread.sleep(500); await(running) - case (finished, remaining) => - val end_date = Date.now() - finished.foreach(log_end(end_date, _)) - await(remaining) + case (_ :: _, remaining) => await(remaining) } } - await(task_specs.map({ case (name, body) => new Task(name, body) })) + val start_date = Date.now() + await(tasks.map(task => log_service.fork_task(start_date, task))) } /* main */ - val main_task = new Task("main", _ => ()) - File.write(main_state_file, main_task.start_date + " " + hostname) - log_start(main_task) + log_service.run_task(main_start_date, + Logger_Task("isabelle_cronjob", _ => parallel_tasks(all_tasks))) - manage_tasks(List("isabelle_identify" -> isabelle_identify _)) + log_service.shutdown() - log_end(Date.now(), main_task) main_state_file.file.delete - - logger.shutdown() }