# HG changeset patch # User wenzelm # Date 1675203464 -3600 # Node ID 7ceed24c88dc8529f37abe81e9691e5014e4462f # Parent 1250a1f2bc1e13d8c84c588987bbc7b678ba7350 alternate AFP tests on lrzcloud2, to fit better into one day; diff -r 1250a1f2bc1e -r 7ceed24c88dc src/Pure/Admin/isabelle_cronjob.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) diff -r 1250a1f2bc1e -r 7ceed24c88dc src/Pure/General/date.scala --- 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