alternate AFP tests on lrzcloud2, to fit better into one day;
authorwenzelm
Tue, 31 Jan 2023 23:17:44 +0100
changeset 77163 7ceed24c88dc
parent 77162 1250a1f2bc1e
child 77165 646e36bf24ae
alternate AFP tests on lrzcloud2, to fit better into one day;
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/General/date.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 31 20:44:35 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Jan 31 23:17:44 2023 +0100
@@ -149,7 +149,7 @@
     bulky: Boolean = false,
     more_hosts: List[String] = Nil,
     detect: PostgreSQL.Source = "",
-    active: Boolean = true
+    active: () => Boolean = () => true
   ) {
     def open_session(options: Options): SSH.Session =
       SSH.open_session(options, host = host, user = user, port = port)
@@ -383,14 +383,16 @@
             " -e ISABELLE_SMLNJ=sml",
           args = "-a -X large -X slow",
           afp = true,
-          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
+          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
+          active = () => Date.now().unix_epoch_day % 2 == 0),
         Remote_Build("AFP", "lrzcloud2",
           java_heap = "8g",
           options = "-m64 -M8 -U30000 -s10 -t AFP",
           args = "-g large -g slow",
           afp = true,
           bulky = true,
-          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))))
+          detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"),
+          active = () => Date.now().unix_epoch_day % 2 == 1)))
 
   def remote_build_history(
     rev: String,
@@ -588,7 +590,7 @@
             PAR(
               List(remote_builds1, remote_builds2).map(remote_builds =>
               SEQ(List(
-                PAR(remote_builds.map(_.filter(_.active)).map(seq =>
+                PAR(remote_builds.map(_.filter(_.active())).map(seq =>
                   SEQ(
                     for {
                       (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
--- a/src/Pure/General/date.scala	Tue Jan 31 20:44:35 2023 +0100
+++ b/src/Pure/General/date.scala	Tue Jan 31 23:17:44 2023 +0100
@@ -106,6 +106,7 @@
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
 
   def unix_epoch: Long = rep.toEpochSecond
+  def unix_epoch_day: Long = rep.toLocalDate.toEpochDay
   def instant: Instant = Instant.from(rep)
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone