src/Pure/Admin/isabelle_cronjob.scala
changeset 64194 b5ada7dcceaa
parent 64193 7a7e370e2523
child 64195 290b8ba96ecc
equal deleted inserted replaced
64193:7a7e370e2523 64194:b5ada7dcceaa
    11 import scala.collection.mutable
    11 import scala.collection.mutable
    12 
    12 
    13 
    13 
    14 object Isabelle_Cronjob
    14 object Isabelle_Cronjob
    15 {
    15 {
    16   /** file-system state: owned by main cronjob **/
    16   /* file-system state: owned by main cronjob */
    17 
    17 
    18   val main_dir = Path.explode("~/cronjob")
    18   val main_dir = Path.explode("~/cronjob")
    19   val run_dir = main_dir + Path.explode("run")
    19   val main_state_file = main_dir + Path.explode("run/main.state")
    20   val log_dir = main_dir + Path.explode("log")
    20   val main_log = main_dir + Path.explode("log/main.log")  // owned by log service
    21 
       
    22   val main_state_file = run_dir + Path.explode("main.state")
       
    23   val main_log = log_dir + Path.explode("main.log")  // owned by log service
       
    24 
       
    25 
       
    26 
       
    27   /** particular tasks **/
       
    28 
       
    29   /* identify repository snapshots */
       
    30 
    21 
    31   val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
    22   val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
    32   val afp_repos = main_dir + Path.explode("AFP-build_history")
    23   val afp_repos = main_dir + Path.explode("AFP-build_history")
    33 
    24 
    34   val isabelle_identify =
    25 
       
    26 
       
    27   /** particular tasks **/
       
    28 
       
    29   /* identify Isabelle + AFP repository snapshots */
       
    30 
       
    31   private def pull_repos(root: Path): String =
       
    32   {
       
    33     val hg = Mercurial.repository(root)
       
    34     hg.pull(options = "-q")
       
    35     hg.identify("tip", options = "-i")
       
    36   }
       
    37 
       
    38   private val isabelle_identify =
    35     Logger_Task("isabelle_identify", logger =>
    39     Logger_Task("isabelle_identify", logger =>
    36       {
    40       {
    37         def pull_repos(root: Path): String =
       
    38         {
       
    39           val hg = Mercurial.repository(root)
       
    40           hg.pull(options = "-q")
       
    41           hg.identify("tip", options = "-i")
       
    42         }
       
    43 
       
    44         val isabelle_id = pull_repos(isabelle_repos)
    41         val isabelle_id = pull_repos(isabelle_repos)
    45         val afp_id = pull_repos(afp_repos)
    42         val afp_id = pull_repos(afp_repos)
    46 
    43 
    47         val log_path =
    44         val log_dir = main_dir + Build_Log.log_subdir(logger.start_date)
    48           main_dir +
    45         Isabelle_System.mkdirs(log_dir)
    49             Build_Log.log_subdir(logger.start_date) +
    46 
    50             Build_Log.log_filename("isabelle_identify", logger.start_date)
    47         File.write(log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
    51         Isabelle_System.mkdirs(log_path.dir)
       
    52         File.write(log_path,
       
    53           terminate_lines(
    48           terminate_lines(
    54             List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
    49             List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
    55               "",
    50               "",
    56               "Isabelle version: " + isabelle_id,
    51               "Isabelle version: " + isabelle_id,
    57               "AFP version: " + afp_id)))
    52               "AFP version: " + afp_id)))
    58       })
    53       })
    59 
    54 
    60 
    55 
    61   /* build_history_base integrity test */
    56   /* integrity test of build_history vs. build_history_base */
    62 
    57 
    63   val build_history_base =
    58   private val build_history_base =
    64     Logger_Task("build_history_base", logger =>
    59     Logger_Task("build_history_base", logger =>
    65       {
    60       {
    66         error("FIXME")
    61         val log_dir = main_dir + Build_Log.log_subdir(logger.start_date)
       
    62         Isabelle_System.mkdirs(log_dir)
       
    63 
       
    64         for {
       
    65           (result, log_path) <-
       
    66             Build_History.build_history(Mercurial.repository(isabelle_repos),
       
    67               rev = "build_history_base", fresh = true, build_args = List("FOL"))
       
    68         } {
       
    69           result.check
       
    70           File.copy(log_path, log_dir + log_path.base)
       
    71         }
    67       })
    72       })
    68 
    73 
    69 
    74 
    70 
    75 
    71   /** task logging **/
    76   /** task logging **/