clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
authorwenzelm
Sun, 19 Nov 2023 19:29:19 +0100
changeset 78996 674954a49364
parent 78995 b9d59669904a
child 78997 39fb869160d6
clarified signature: explicit Remote_Build.count instead of duplicate entries (see also ee8c014526dc);
src/Pure/Admin/build_status.scala
src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/build_status.scala	Sun Nov 19 15:15:09 2023 +0100
+++ b/src/Pure/Admin/build_status.scala	Sun Nov 19 19:29:19 2023 +0100
@@ -14,8 +14,7 @@
   val default_image_size = (800, 600)
   val default_history = 30
 
-  def default_profiles: List[Profile] =
-    Library.distinct(Isabelle_Cronjob.build_status_profiles)
+  def default_profiles: List[Profile] = Isabelle_Cronjob.build_status_profiles
 
 
   /* data profiles */
@@ -252,7 +251,7 @@
     val store = Build_Log.store(options)
 
     using(store.open_database()) { db =>
-      for (profile <- Library.distinct(profiles).sortBy(_.description)) {
+      for (profile <- profiles.sortBy(_.description)) {
         progress.echo("input " + quote(profile.description))
 
         val afp = profile.afp
--- a/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 15:15:09 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun Nov 19 19:29:19 2023 +0100
@@ -137,8 +137,10 @@
     bulky: Boolean = false,
     more_hosts: List[String] = Nil,
     detect: PostgreSQL.Source = "",
-    active: () => Boolean = () => true
+    count: () => Int = () => 1
   ) {
+    def active(): Boolean = count() > 0
+
     def open_session(options: Options): SSH.Session =
       SSH.open_session(options, host = host, user = user, port = port)
 
@@ -311,33 +313,35 @@
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
           args = "-a -d '~~/src/Benchmarks'")),
-      Library.replicate(2,
+      List(
         Remote_Build("macOS 14 Sonoma (ARM)", "studio1-sonoma",
           history_base = "8e590adaac5e",
           options = "-m32 -B -M1x4,2x4,4x2,8 -p pide_session=false" +
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/opt/homebrew/bin/swipl",
-          args = "-a -d '~~/src/Benchmarks'")),
+          args = "-a -d '~~/src/Benchmarks'",
+          count = () => 2)),
       List(
         Remote_Build("macOS, quick_and_dirty", "mini2",
           options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
           args = "-a -o quick_and_dirty",
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
-          active = () => false),
+          count = () => 0),
         Remote_Build("macOS, skip_proofs", "mini2",
           options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
-          active = () => false)),
-      Library.replicate(3,
+          count = () => 0)),
+      List(
         Remote_Build("macOS 13 Ventura (ARM)", "mini3",
           history_base = "8e590adaac5e",
           options = "-a -m32 -B -M1x4,2x2,4 -p pide_session=false" +
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_MLTON=/opt/homebrew/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_SWIPL=/opt/homebrew/bin/swipl",
-          args = "-a -d '~~/src/Benchmarks'")),
-      Library.replicate(2,
+          args = "-a -d '~~/src/Benchmarks'",
+          count = () => 3)),
+      List(
         Remote_Build("Windows", "vmnipkow9", history = 90,
           components_base = "/cygdrive/d/isatest/contrib",
           options = "-m32 -M4" +
@@ -347,8 +351,8 @@
           args = "-a",
           detect =
             Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " +
-            Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows"))) :::
-      Library.replicate(2,
+            Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows"),
+          count = () => 2),
         Remote_Build("Windows", "vmnipkow9", history = 90,
           components_base = "/cygdrive/d/isatest/contrib",
           options = "-m64 -M4" +
@@ -357,7 +361,9 @@
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
           args = "-a",
-          detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows"))))
+          detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows"),
+          count = () => 2))
+    )
   }
 
   val remote_builds2: List[List[Remote_Build]] =
@@ -373,7 +379,7 @@
           args = "-a -X large -X slow",
           afp = true,
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
-          active = () => Date.now().unix_epoch_day % 2 == 0),
+          count = () => if (Date.now().unix_epoch_day % 2 == 0) 1 else 0),
         Remote_Build("AFP", "lrzcloud2",
           java_heap = "8g",
           options = "-m64 -M8 -U30000 -s10 -t AFP",
@@ -381,7 +387,7 @@
           afp = true,
           bulky = true,
           detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
-          active = () => Date.now().unix_epoch_day % 2 == 1)))
+          count = () => if (Date.now().unix_epoch_day % 2 == 1) 1 else 0)))
 
   def remote_build_history(
     rev: String,
@@ -596,10 +602,11 @@
             PAR(
               List(remote_builds1, remote_builds2).map(remote_builds =>
                 SEQUENTIAL(
-                  PAR(remote_builds.map(_.filter(_.active())).map(seq =>
+                  PAR(remote_builds.map(seq =>
                     SEQ(
                       for {
                         (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
+                        _ <- List.from(1 to r.count())
                       } yield () => {
                         r.pick(logger.options)
                           .map({ case (rev, afp_rev) =>