src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Mon May 08 12:04:58 2017 +0200 (2017-05-08)
changeset 65770 fb8a7962f2ae
parent 65768 b8da621a3297
child 65771 688a7dd22cbb
permissions -rw-r--r--
clarified modules;
     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 scala.annotation.tailrec
    11 import scala.collection.mutable
    12 
    13 
    14 object Isabelle_Cronjob
    15 {
    16   /* file-system state: owned by main cronjob */
    17 
    18   val main_dir = Path.explode("~/cronjob")
    19   val main_state_file = main_dir + Path.explode("run/main.state")
    20   val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
    21   val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
    22 
    23   val isabelle_repos = main_dir + Path.explode("isabelle")
    24   val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
    25   val afp_repos = main_dir + Path.explode("AFP")
    26 
    27   val isabelle_dev_source = "http://isabelle.in.tum.de/repos/isabelle"
    28   val isabelle_release_source = "http://bitbucket.org/isabelle_project/isabelle-release"
    29   val afp_source = "https://bitbucket.org/isa-afp/afp-devel"
    30 
    31   val jenkins_jobs = "identify" :: Jenkins.build_log_jobs
    32 
    33 
    34 
    35   /** particular tasks **/
    36 
    37   /* identify Isabelle + AFP repository snapshots and build release */
    38 
    39   private val build_release =
    40     Logger_Task("build_release", logger =>
    41         {
    42           val rev = Mercurial.repository(isabelle_repos).id()
    43           val afp_rev = Mercurial.setup_repository(afp_source, afp_repos).id()
    44 
    45           File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
    46             Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
    47 
    48           Isabelle_Devel.release_snapshot(rev = rev, afp_rev = afp_rev,
    49             parallel_jobs = 4, remote_mac = "macbroy31")
    50         })
    51 
    52 
    53   /* integrity test of build_history vs. build_history_base */
    54 
    55   private val build_history_base =
    56     Logger_Task("build_history_base", logger =>
    57       {
    58         val hg =
    59           Mercurial.setup_repository(
    60             File.standard_path(isabelle_repos), isabelle_repos_test)
    61         for {
    62           (result, log_path) <-
    63             Build_History.build_history(
    64               hg, rev = "build_history_base", fresh = true, build_args = List("HOL"))
    65         } {
    66           result.check
    67           File.move(log_path, logger.log_dir + log_path.base)
    68         }
    69       })
    70 
    71 
    72   /* remote build_history */
    73 
    74   sealed case class Remote_Build(
    75     description: String,
    76     host: String,
    77     user: String = "",
    78     port: Int = 0,
    79     shared_home: Boolean = true,
    80     options: String = "",
    81     args: String = "",
    82     detect: SQL.Source = "")
    83   {
    84     def profile: Build_Status.Profile =
    85     {
    86       val sql =
    87         Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
    88         Build_Log.Prop.build_host + " = " + SQL.string(host) +
    89         (if (detect == "") "" else " AND " + SQL.enclose(detect))
    90       Build_Status.Profile(description, sql)
    91     }
    92   }
    93 
    94   private val remote_builds: List[List[Remote_Build]] =
    95   {
    96     List(
    97       List(Remote_Build("Poly/ML test", "lxbroy8",
    98         options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
    99         args = "-N -g timing",
   100         detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test"))),
   101       List(Remote_Build("Linux A", "lxbroy9",
   102         options = "-m32 -B -M1x2,2", args = "-N -g timing")),
   103       List(Remote_Build("Linux B", "lxbroy10",
   104         options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
   105       List(
   106         Remote_Build("Mac OS X 10.9 Mavericks", "macbroy2", options = "-m32 -M8", args = "-a",
   107           detect = Build_Log.Prop.build_tags + " IS NULL"),
   108         Remote_Build("Mac OS X 10.9 Mavericks, quick_and_dirty", "macbroy2",
   109           options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
   110           detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
   111         Remote_Build("Mac OS X 10.9 Mavericks, skip_proofs", "macbroy2",
   112           options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
   113           detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))),
   114       List(
   115         Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a",
   116           detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
   117       List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")),
   118       List(
   119         Remote_Build("Windows", "vmnipkow9", shared_home = false,
   120           options = "-m32 -M4", args = "-a",
   121           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
   122         Remote_Build("Windows", "vmnipkow9", shared_home = false,
   123           options = "-m64 -M4", args = "-a",
   124           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
   125   }
   126 
   127   private val remote_builds_old: List[Remote_Build] =
   128     List(
   129       Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
   130         detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
   131 
   132   private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
   133   {
   134     val task_name = "build_history-" + r.host
   135     Logger_Task(task_name, logger =>
   136       {
   137         using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
   138           ssh =>
   139             {
   140               val self_update = !r.shared_home
   141               val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
   142 
   143               val (results, _) =
   144                 Build_History.remote_build_history(ssh,
   145                   isabelle_repos,
   146                   isabelle_repos.ext(r.host),
   147                   isabelle_repos_source = isabelle_dev_source,
   148                   self_update = self_update,
   149                   push_isabelle_home = push_isabelle_home,
   150                   options =
   151                     "-r " + Bash.string(rev) + " -N " + Bash.string(task_name) + " -f " + r.options,
   152                   args = "-o timeout=10800 " + r.args)
   153 
   154               for ((log_name, bytes) <- results) {
   155                 logger.log(Date.now(), log_name)
   156                 Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
   157               }
   158             })
   159       })
   160   }
   161 
   162   val build_status_profiles: List[Build_Status.Profile] =
   163     (remote_builds_old :: remote_builds).flatten.map(_.profile)
   164 
   165 
   166 
   167   /** task logging **/
   168 
   169   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
   170 
   171   class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH.Context)
   172   {
   173     current_log.file.delete
   174 
   175     private val thread: Consumer_Thread[String] =
   176       Consumer_Thread.fork("cronjob: logger", daemon = true)(
   177         consume = (text: String) =>
   178           { // critical
   179             File.append(current_log, text + "\n")
   180             File.append(cumulative_log, text + "\n")
   181             progress.echo(text)
   182             true
   183           })
   184 
   185     def shutdown() { thread.shutdown() }
   186 
   187     val hostname = Isabelle_System.hostname()
   188 
   189     def log(date: Date, task_name: String, msg: String): Unit =
   190       if (task_name != "")
   191         thread.send(
   192           "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
   193 
   194     def start_logger(start_date: Date, task_name: String): Logger =
   195       new Logger(this, start_date, task_name)
   196 
   197     def run_task(start_date: Date, task: Logger_Task)
   198     {
   199       val logger = start_logger(start_date, task.name)
   200       val res = Exn.capture { task.body(logger) }
   201       val end_date = Date.now()
   202       val err =
   203         res match {
   204           case Exn.Res(_) => None
   205           case Exn.Exn(exn) =>
   206             System.err.println("Exception trace for " + quote(task.name) + ":")
   207             exn.printStackTrace()
   208             val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
   209             Some(first_line)
   210         }
   211       logger.log_end(end_date, err)
   212     }
   213 
   214     def fork_task(start_date: Date, task: Logger_Task): Task =
   215       new Task(task.name, run_task(start_date, task))
   216   }
   217 
   218   class Logger private[Isabelle_Cronjob](
   219     val log_service: Log_Service, val start_date: Date, val task_name: String)
   220   {
   221     def ssh_context: SSH.Context = log_service.ssh_context
   222     def options: Options = ssh_context.options
   223 
   224     def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
   225 
   226     def log_end(end_date: Date, err: Option[String])
   227     {
   228       val elapsed_time = end_date.time - start_date.time
   229       val msg =
   230         (if (err.isEmpty) "finished" else "ERROR " + err.get) +
   231         (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
   232       log(end_date, msg)
   233     }
   234 
   235     val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
   236 
   237     Isabelle_System.mkdirs(log_dir)
   238     log(start_date, "started")
   239   }
   240 
   241   class Task private[Isabelle_Cronjob](name: String, body: => Unit)
   242   {
   243     private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
   244     def is_finished: Boolean = future.is_finished
   245   }
   246 
   247 
   248 
   249   /** cronjob **/
   250 
   251   def cronjob(progress: Progress, exclude_task: Set[String])
   252   {
   253     /* soft lock */
   254 
   255     val still_running =
   256       try { Some(File.read(main_state_file)) }
   257       catch { case ERROR(_) => None }
   258 
   259     still_running match {
   260       case None | Some("") =>
   261       case Some(running) =>
   262         error("Isabelle cronjob appears to be still running: " + running)
   263     }
   264 
   265 
   266     /* log service */
   267 
   268     val log_service = new Log_Service(progress, SSH.init_context(Options.init()))
   269 
   270     def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
   271 
   272     def run_now(task: Logger_Task) { run(Date.now(), task) }
   273 
   274 
   275     /* structured tasks */
   276 
   277     def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
   278       for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
   279         run_now(task))
   280 
   281     def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
   282       {
   283         @tailrec def join(running: List[Task])
   284         {
   285           running.partition(_.is_finished) match {
   286             case (Nil, Nil) =>
   287             case (Nil, _ :: _) => Thread.sleep(500); join(running)
   288             case (_ :: _, remaining) => join(remaining)
   289           }
   290         }
   291         val start_date = Date.now()
   292         val running =
   293           for (task <- tasks if !exclude_task(task.name))
   294             yield log_service.fork_task(start_date, task)
   295         join(running)
   296       })
   297 
   298 
   299     /* main */
   300 
   301     val main_start_date = Date.now()
   302     File.write(main_state_file, main_start_date + " " + log_service.hostname)
   303 
   304     val rev = Mercurial.repository(isabelle_repos).id()
   305 
   306     run(main_start_date,
   307       Logger_Task("isabelle_cronjob", _ =>
   308         run_now(
   309           SEQ(List(build_release, build_history_base,
   310             PAR(remote_builds.map(seq => SEQ(seq.map(remote_build_history(rev, _))))),
   311             Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
   312             Logger_Task("build_log_database",
   313               logger => Isabelle_Devel.build_log_database(logger.options)),
   314             Logger_Task("build_status",
   315               logger => Isabelle_Devel.build_status(logger.options)))))))
   316 
   317     log_service.shutdown()
   318 
   319     main_state_file.file.delete
   320   }
   321 
   322 
   323 
   324   /** command line entry point **/
   325 
   326   def main(args: Array[String])
   327   {
   328     Command_Line.tool0 {
   329       var force = false
   330       var verbose = false
   331       var exclude_task = Set.empty[String]
   332 
   333       val getopts = Getopts("""
   334 Usage: Admin/cronjob/main [OPTIONS]
   335 
   336   Options are:
   337     -f           apply force to do anything
   338     -v           verbose
   339     -x NAME      exclude tasks with this name
   340 """,
   341         "f" -> (_ => force = true),
   342         "v" -> (_ => verbose = true),
   343         "x:" -> (arg => exclude_task += arg))
   344 
   345       val more_args = getopts(args)
   346       if (more_args.nonEmpty) getopts.usage()
   347 
   348       val progress = if (verbose) new Console_Progress() else No_Progress
   349 
   350       if (force) cronjob(progress, exclude_task)
   351       else error("Need to apply force to do anything")
   352     }
   353   }
   354 }