--- 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)
--- 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)))
}
}
--- 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)