# HG changeset patch
# User wenzelm
# Date 1547925506 -3600
# Node ID 06153e2e0cdbc32208d95a101859d7aa1a1b04dc
# Parent  3b777286c3ecd1fc27c84f6da67af881ce5f8924
more official AFP.groups;
clarified bulky sessions;

diff -r 3b777286c3ec -r 06153e2e0cdb src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sat Jan 19 19:16:58 2019 +0100
+++ b/src/Pure/Admin/afp.scala	Sat Jan 19 20:18:26 2019 +0100
@@ -11,6 +11,13 @@
 {
   val repos_source = "https://bitbucket.org/isa-afp/afp-devel"
 
+  val groups: Map[String, String] =
+    Map("large" -> "full 64-bit memory model or word arithmetic required",
+      "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
+      "very_slow" -> "elapsed time of many hours (on high-end hardware)")
+
+  def groups_bulky: List[String] = List("large", "slow")
+
   def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP =
     new AFP(options, base_dir)
 
diff -r 3b777286c3ec -r 06153e2e0cdb src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat Jan 19 19:16:58 2019 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Jan 19 20:18:26 2019 +0100
@@ -22,7 +22,7 @@
   /* data profiles */
 
   sealed case class Profile(
-    description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String)
+    description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String)
   {
     def days(options: Options): Int = options.int("build_log_history") max history
 
@@ -319,7 +319,8 @@
                   Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
               }
 
-            if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
+            if ((!afp || chapter == "AFP") &&
+                (!profile.bulky || groups.contains(AFP.groups_bulky.toSet))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))
             }
           }
diff -r 3b777286c3ec -r 06153e2e0cdb src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Jan 19 19:16:58 2019 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Jan 19 20:18:26 2019 +0100
@@ -161,7 +161,7 @@
     options: String = "",
     args: String = "",
     afp: Boolean = false,
-    slow: Boolean = false,
+    bulky: Boolean = false,
     more_hosts: List[String] = Nil,
     detect: SQL.Source = "",
     active: Boolean = true)
@@ -177,7 +177,7 @@
       (if (detect == "") "" else " AND " + SQL.enclose(detect))
 
     def profile: Build_Status.Profile =
-      Build_Status.Profile(description, history = history, afp = afp, slow = slow, sql = sql)
+      Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
 
     def pick(
       options: Options,
@@ -216,7 +216,7 @@
   val remote_builds_old: List[Remote_Build] =
     List(
       Remote_Build("AFP", "lxbroy7",
-          args = "-N -X slow",
+          args = "-N -X large -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
       Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
@@ -315,7 +315,7 @@
             " -e ISABELLE_MLTON=mlton" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
             " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml",
-          args = "-N -X slow",
+          args = "-N -X large -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
       }
@@ -329,9 +329,9 @@
           proxy_host = "lxbroy10", proxy_user = "i21isatest",
           ssh_host = "10.155.208.96", ssh_permissive = true,
           options = "-m64 -M6 -U30000 -s10 -t AFP",
-          args = "-g slow",
+          args = "-g large -g slow",
           afp = true,
-          slow = true,
+          bulky = true,
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
 
   def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)