src/Pure/Admin/isabelle_cronjob.scala
changeset 67753 f28aee3ad1e6
parent 67752 636f633552a3
child 67754 197366313aaf
equal deleted inserted replaced
67752:636f633552a3 67753:f28aee3ad1e6
    18   val main_dir = Path.explode("~/cronjob")
    18   val main_dir = Path.explode("~/cronjob")
    19   val main_state_file = main_dir + Path.explode("run/main.state")
    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
    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
    21   val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
    22 
    22 
       
    23   val isabelle_repos_source = "https://isabelle.in.tum.de/repos/isabelle"
    23   val isabelle_repos = main_dir + Path.explode("isabelle")
    24   val isabelle_repos = main_dir + Path.explode("isabelle")
    24   val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
    25   val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
    25   val afp_repos = main_dir + Path.explode("AFP")
    26   val afp_repos = main_dir + Path.explode("AFP")
    26 
    27 
    27   val build_log_dirs =
    28   val build_log_dirs =
    34   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    35   sealed case class Logger_Task(name: String = "", body: Logger => Unit)
    35 
    36 
    36 
    37 
    37   /* init and identify Isabelle + AFP repository snapshots */
    38   /* init and identify Isabelle + AFP repository snapshots */
    38 
    39 
       
    40   def get_rev(): String = Mercurial.repository(isabelle_repos).id()
       
    41   def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
       
    42 
    39   val init =
    43   val init =
    40     Logger_Task("init", logger =>
    44     Logger_Task("init", logger =>
    41       {
    45       {
    42         Isabelle_Devel.make_index()
    46         Isabelle_Devel.make_index()
    43 
    47 
    44         val rev = Mercurial.repository(isabelle_repos).id()
    48         Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
    45         val afp_rev = Mercurial.setup_repository(AFP.repos_source, afp_repos).id()
    49         Mercurial.setup_repository(AFP.repos_source, afp_repos)
    46 
    50 
    47         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
    51         File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
    48           Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
    52           Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
    49       })
    53       })
    50 
    54 
    51 
    55 
    52   /* build release */
    56   /* build release */
    53 
    57 
    54   val build_release =
    58   val build_release =
    55     Logger_Task("build_release", logger =>
    59     Logger_Task("build_release", logger =>
    56       {
    60       {
    57         val rev = Mercurial.repository(isabelle_repos).id()
    61         Isabelle_Devel.release_snapshot(rev = get_rev(), afp_rev = get_afp_rev(),
    58         val afp_rev = Mercurial.repository(afp_repos).id()
       
    59 
       
    60         Isabelle_Devel.release_snapshot(rev = rev, afp_rev = afp_rev,
       
    61           parallel_jobs = 4, remote_mac = "macbroy31")
    62           parallel_jobs = 4, remote_mac = "macbroy31")
    62       })
    63       })
    63 
    64 
    64 
    65 
    65   /* integrity test of build_history vs. build_history_base */
    66   /* integrity test of build_history vs. build_history_base */
   158     def pick(
   159     def pick(
   159       options: Options,
   160       options: Options,
   160       rev: String = "",
   161       rev: String = "",
   161       filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
   162       filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
   162     {
   163     {
   163       val afp_rev = if (afp) Some(Mercurial.repository(afp_repos).id()) else None
   164       val afp_rev = if (afp) Some(get_afp_rev()) else None
   164 
   165 
   165       val store = Build_Log.store(options)
   166       val store = Build_Log.store(options)
   166       using(store.open_database())(db =>
   167       using(store.open_database())(db =>
   167       {
   168       {
   168         def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
   169         def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =