--- 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()
}