tuned output;
authorwenzelm
Wed Nov 01 17:29:14 2017 +0100 (17 months ago)
changeset 669808947cf58cb86
parent 66979 58b166fd8447
child 66981 e76c6cb0d461
tuned output;
src/Pure/Admin/build_status.scala
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed Nov 01 17:07:43 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed Nov 01 17:29:14 2017 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    /* data profiles */
     1.5  
     1.6    sealed case class Profile(
     1.7 -    description: String, history: Int = 0, afp: Boolean = false, sql: String)
     1.8 +    description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String)
     1.9    {
    1.10      def days(options: Options): Int = options.int("build_log_history") max history
    1.11  
    1.12 @@ -168,6 +168,7 @@
    1.13              Build_Log.Settings.ML_PLATFORM,
    1.14              Build_Log.Data.session_name,
    1.15              Build_Log.Data.chapter,
    1.16 +            Build_Log.Data.groups,
    1.17              Build_Log.Data.threads,
    1.18              Build_Log.Data.timing_elapsed,
    1.19              Build_Log.Data.timing_cpu,
    1.20 @@ -191,6 +192,7 @@
    1.21            while (res.next()) {
    1.22              val session_name = res.string(Build_Log.Data.session_name)
    1.23              val chapter = res.string(Build_Log.Data.chapter)
    1.24 +            val groups = split_lines(res.string(Build_Log.Data.groups))
    1.25              val threads =
    1.26              {
    1.27                val threads1 =
    1.28 @@ -248,7 +250,7 @@
    1.29              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.30              val session = Session(session_name, threads, entry :: entries, ml_stats)
    1.31  
    1.32 -            if (!afp || chapter == "AFP") {
    1.33 +            if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
    1.34                data_entries += (data_name -> (sessions + (session_name -> session)))
    1.35              }
    1.36            }
     2.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 01 17:07:43 2017 +0100
     2.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Nov 01 17:29:14 2017 +0100
     2.3 @@ -123,6 +123,7 @@
     2.4      options: String = "",
     2.5      args: String = "",
     2.6      afp: Boolean = false,
     2.7 +    slow: Boolean = false,
     2.8      detect: SQL.Source = "")
     2.9    {
    2.10      def sql: SQL.Source =
    2.11 @@ -131,7 +132,7 @@
    2.12        (if (detect == "") "" else " AND " + SQL.enclose(detect))
    2.13  
    2.14      def profile: Build_Status.Profile =
    2.15 -      Build_Status.Profile(description, history = history, afp = afp, sql = sql)
    2.16 +      Build_Status.Profile(description, history = history, afp = afp, slow = slow, sql = sql)
    2.17  
    2.18      def pick(
    2.19        options: Options,
    2.20 @@ -261,6 +262,7 @@
    2.21            options = "-m64 -M6 -U30000 -s10 -t AFP",
    2.22            args = "-g slow",
    2.23            afp = true,
    2.24 +          slow = true,
    2.25            detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
    2.26  
    2.27    private def remote_build_history(