src/Pure/Admin/isabelle_cronjob.scala
changeset 66864 5cb8ccc46e3e
parent 66861 f6676691ef8a
child 66865 c8b18abf23e1
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 20:58:52 2017 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Oct 14 21:50:12 2017 +0200
     1.3 @@ -69,23 +69,37 @@
     1.4  
     1.5    /* remote build_history */
     1.6  
     1.7 -  sealed case class Item(known: Boolean, isabelle_version: String, pull_date: Date)
     1.8 +  sealed case class Item(
     1.9 +    known: Boolean,
    1.10 +    isabelle_version: String,
    1.11 +    afp_version: Option[String],
    1.12 +    pull_date: Date)
    1.13    {
    1.14      def unknown: Boolean = !known
    1.15 +    def versions: (String, Option[String]) = (isabelle_version, afp_version)
    1.16 +
    1.17 +    def known_versions(rev: String, afp_rev: Option[String]): Boolean =
    1.18 +      known && rev != "" && isabelle_version == rev &&
    1.19 +      (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get)
    1.20    }
    1.21  
    1.22 -  def recent_items(db: SQL.Database, days: Int, rev: String, sql: SQL.Source): List[Item] =
    1.23 +  def recent_items(db: SQL.Database,
    1.24 +    days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
    1.25    {
    1.26      val select =
    1.27 -      Build_Log.Data.select_recent_versions(days = days, rev = rev, sql = "WHERE " + sql)
    1.28 +      Build_Log.Data.select_recent_versions(
    1.29 +        days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
    1.30  
    1.31      db.using_statement(select)(stmt =>
    1.32        stmt.execute_query().iterator(res =>
    1.33        {
    1.34          val known = res.bool(Build_Log.Data.known)
    1.35          val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
    1.36 +        val afp_version =
    1.37 +          if (afp_rev.isEmpty) None
    1.38 +          else proper_string(res.string(Build_Log.Prop.afp_version))
    1.39          val pull_date = res.date(Build_Log.Data.pull_date)
    1.40 -        Item(known, isabelle_version, pull_date)
    1.41 +        Item(known, isabelle_version, afp_version, pull_date)
    1.42        }).toList)
    1.43    }
    1.44  
    1.45 @@ -106,6 +120,7 @@
    1.46      history_base: String = "build_history_base",
    1.47      options: String = "",
    1.48      args: String = "",
    1.49 +    afp: Boolean = false,
    1.50      detect: SQL.Source = "")
    1.51    {
    1.52      def sql: SQL.Source =
    1.53 @@ -123,32 +138,33 @@
    1.54        (rev0 :: graph.all_succs(List(rev0))).toSet
    1.55      }
    1.56  
    1.57 -    def pick(options: Options, rev: String = "", filter: String => Boolean = (_: String) => true)
    1.58 -      : Option[String] =
    1.59 +    def pick(
    1.60 +      options: Options,
    1.61 +      rev: String = "",
    1.62 +      filter: String => Boolean = (_: String) => true): Option[(String, Option[String])] =
    1.63      {
    1.64 +      val afp_rev = if (afp) Some(Mercurial.repository(afp_repos).id()) else None
    1.65 +
    1.66        val store = Build_Log.store(options)
    1.67        using(store.open_database())(db =>
    1.68        {
    1.69 -        def pick_days(days: Int, gap: Int): Option[String] =
    1.70 +        def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
    1.71          {
    1.72            val items =
    1.73 -            recent_items(db, days = days, rev = rev, sql = sql).
    1.74 +            recent_items(db, days, rev, afp_rev, sql).
    1.75                filter(item => filter(item.isabelle_version))
    1.76            def runs = unknown_runs(items).filter(run => run.length >= gap)
    1.77  
    1.78 -          val known_rev =
    1.79 -            rev != "" && items.exists(item => item.known && item.isabelle_version == rev)
    1.80 -
    1.81 -          if (historic || known_rev) {
    1.82 +          if (historic || items.exists(_.known_versions(rev, afp_rev))) {
    1.83              val longest_run =
    1.84                (List.empty[Item] /: runs)({ case (item1, item2) =>
    1.85                  if (item1.length >= item2.length) item1 else item2
    1.86                })
    1.87              if (longest_run.isEmpty) None
    1.88 -            else Some(longest_run(longest_run.length / 2).isabelle_version)
    1.89 +            else Some(longest_run(longest_run.length / 2).versions)
    1.90            }
    1.91 -          else if (rev != "") Some(rev)
    1.92 -          else runs.flatten.headOption.map(_.isabelle_version)
    1.93 +          else if (rev != "") Some((rev, afp_rev))
    1.94 +          else runs.flatten.headOption.map(_.versions)
    1.95          }
    1.96  
    1.97          pick_days(options.int("build_log_history") max history, 2) orElse
    1.98 @@ -227,10 +243,22 @@
    1.99              " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
   1.100              " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
   1.101            args = "-a",
   1.102 -          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
   1.103 +          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
   1.104 +    ) :::
   1.105 +    {
   1.106 +      for { (host, n) <- List("lxbroy6" -> 1, "lxbroy7" -> 2) }
   1.107 +      yield {
   1.108 +        List(Remote_Build("AFP " + n, host = host,
   1.109 +          options = "-m32 -M1x2 -t AFP -P" + n,
   1.110 +          args = "-N -X slow",
   1.111 +          afp = true,
   1.112 +          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
   1.113 +      }
   1.114 +    }
   1.115    }
   1.116  
   1.117 -  private def remote_build_history(rev: String, i: Int, r: Remote_Build): Logger_Task =
   1.118 +  private def remote_build_history(
   1.119 +    rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
   1.120    {
   1.121      val task_name = "build_history-" + r.host
   1.122      Logger_Task(task_name, logger =>
   1.123 @@ -249,6 +277,7 @@
   1.124                    self_update = self_update,
   1.125                    push_isabelle_home = push_isabelle_home,
   1.126                    rev = rev,
   1.127 +                  afp_rev = afp_rev,
   1.128                    options =
   1.129                      " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
   1.130                      " -f " + r.options,
   1.131 @@ -415,8 +444,8 @@
   1.132                SEQ(
   1.133                  for {
   1.134                    (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
   1.135 -                  rev <- r.pick(logger.options, rev, r.history_base_filter(hg))
   1.136 -                } yield remote_build_history(rev, i, r)))),
   1.137 +                  (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, r.history_base_filter(hg))
   1.138 +                } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
   1.139              Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
   1.140              Logger_Task("build_log_database",
   1.141                logger => Isabelle_Devel.build_log_database(logger.options)),