clarified log_subdir vs. log_filename;
authorwenzelm
Thu Oct 13 16:14:41 2016 +0200 (2016-10-13)
changeset 641937a7e370e2523
parent 64192 4c0d19b3a882
child 64194 b5ada7dcceaa
clarified log_subdir vs. log_filename;
support for sequential and parallel task blocks (unnamed);
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/build_history.scala	Thu Oct 13 15:44:24 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Thu Oct 13 16:14:41 2016 +0200
     1.3 @@ -191,8 +191,10 @@
     1.4        /* output log */
     1.5  
     1.6        val log_path =
     1.7 -        other_isabelle.isabelle_home_user + Path.explode("log") +
     1.8 -          Build_Log.log_path(BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
     1.9 +        other_isabelle.isabelle_home_user +
    1.10 +          Build_Log.log_subdir(build_history_date) +
    1.11 +          Build_Log.log_filename(
    1.12 +            BUILD_HISTORY, build_history_date, ml_platform, "M" + threads).ext("gz")
    1.13  
    1.14        val build_info = Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info()
    1.15  
     2.1 --- a/src/Pure/Admin/build_log.scala	Thu Oct 13 15:44:24 2016 +0200
     2.2 +++ b/src/Pure/Admin/build_log.scala	Thu Oct 13 16:14:41 2016 +0200
     2.3 @@ -27,9 +27,11 @@
     2.4        DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
     2.5        new java.lang.Long((date.time - date.midnight.time).ms / 1000))
     2.6  
     2.7 -  def log_path(engine: String, date: Date, more: String*): Path =
     2.8 -    Path.explode(date.rep.getYear.toString) +
     2.9 -      Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
    2.10 +  def log_subdir(date: Date): Path =
    2.11 +    Path.explode("log") + Path.explode(date.rep.getYear.toString)
    2.12 +
    2.13 +  def log_filename(engine: String, date: Date, more: String*): Path =
    2.14 +    Path.explode((engine :: log_date(date) :: more.toList).mkString("", "_", ".log"))
    2.15  
    2.16  
    2.17    /* log file collections */
     3.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 15:44:24 2016 +0200
     3.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Oct 13 16:14:41 2016 +0200
     3.3 @@ -44,7 +44,10 @@
     3.4          val isabelle_id = pull_repos(isabelle_repos)
     3.5          val afp_id = pull_repos(afp_repos)
     3.6  
     3.7 -        val log_path = log_dir + Build_Log.log_path("isabelle_identify", logger.start_date)
     3.8 +        val log_path =
     3.9 +          main_dir +
    3.10 +            Build_Log.log_subdir(logger.start_date) +
    3.11 +            Build_Log.log_filename("isabelle_identify", logger.start_date)
    3.12          Isabelle_System.mkdirs(log_path.dir)
    3.13          File.write(log_path,
    3.14            terminate_lines(
    3.15 @@ -55,10 +58,19 @@
    3.16        })
    3.17  
    3.18  
    3.19 +  /* build_history_base integrity test */
    3.20 +
    3.21 +  val build_history_base =
    3.22 +    Logger_Task("build_history_base", logger =>
    3.23 +      {
    3.24 +        error("FIXME")
    3.25 +      })
    3.26 +
    3.27 +
    3.28  
    3.29    /** task logging **/
    3.30  
    3.31 -  sealed case class Logger_Task(name: String, body: Logger => Unit)
    3.32 +  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    3.33  
    3.34    class Log_Service private[Isabelle_Cronjob](progress: Progress)
    3.35    {
    3.36 @@ -76,8 +88,9 @@
    3.37      val hostname = Isabelle_System.hostname()
    3.38  
    3.39      def log(date: Date, task_name: String, msg: String): Unit =
    3.40 -      thread.send(
    3.41 -        "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
    3.42 +      if (task_name != "")
    3.43 +        thread.send(
    3.44 +          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
    3.45  
    3.46      def start_logger(start_date: Date, task_name: String): Logger =
    3.47        new Logger(this, start_date, task_name)
    3.48 @@ -148,15 +161,16 @@
    3.49      File.write(main_state_file, main_start_date + " " + log_service.hostname)
    3.50  
    3.51  
    3.52 -    /* manage tasks */
    3.53 +    /* run tasks */
    3.54 +
    3.55 +    def run(start_date: Date, task: Logger_Task): Unit =
    3.56 +      log_service.run_task(start_date, task)
    3.57  
    3.58 -    def sequential_tasks(tasks: List[Logger_Task])
    3.59 -    {
    3.60 -      for (task <- tasks.iterator if !exclude_task(task.name))
    3.61 -        log_service.run_task(Date.now(), task)
    3.62 -    }
    3.63 +    def run_sequential(tasks: Logger_Task*): Unit =
    3.64 +      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
    3.65 +        run(Date.now(), task)
    3.66  
    3.67 -    def parallel_tasks(tasks: List[Logger_Task])
    3.68 +    def run_parallel(tasks: Logger_Task*)
    3.69      {
    3.70        @tailrec def join(running: List[Task])
    3.71        {
    3.72 @@ -169,16 +183,23 @@
    3.73  
    3.74        val start_date = Date.now()
    3.75        val running =
    3.76 -        for (task <- tasks if !exclude_task(task.name))
    3.77 +        for (task <- tasks.toList if !exclude_task(task.name))
    3.78            yield log_service.fork_task(start_date, task)
    3.79        join(running)
    3.80      }
    3.81  
    3.82 +    def SEQ(tasks: Logger_Task*): Logger_Task =
    3.83 +      Logger_Task(body = _ => run_sequential(tasks:_*))
    3.84 +
    3.85 +    def PAR(tasks: Logger_Task*): Logger_Task =
    3.86 +      Logger_Task(body = _ => run_parallel(tasks:_*))
    3.87 +
    3.88  
    3.89      /* main */
    3.90  
    3.91 -    log_service.run_task(main_start_date,
    3.92 -      Logger_Task("isabelle_cronjob", _ => parallel_tasks(List(isabelle_identify))))
    3.93 +    run(main_start_date,
    3.94 +      Logger_Task("isabelle_cronjob", _ =>
    3.95 +        run_sequential(isabelle_identify, build_history_base)))
    3.96  
    3.97      log_service.shutdown()
    3.98