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