--- a/src/Pure/Build/build_ci.scala Mon Jan 20 22:20:14 2025 +0100
+++ b/src/Pure/Build/build_ci.scala Tue Jan 21 11:17:05 2025 +0100
@@ -70,16 +70,14 @@
case object On_Commit extends Trigger
object Timed {
- def nightly(start_time: Time = Time.zero): Timed =
- Timed { (before, now) =>
- val start0 = before.midnight + start_time
- val start1 = now.midnight + start_time
- (before.time < start0.time && start0.time <= now.time) ||
- (before.time < start1.time && start1.time <= now.time)
- }
+ def nightly(start: Time = Time.hms(0, 17, 0)): Timed = Timed(Date.Daily(start))
+ def weekly(day: Date.Day = Date.Day.sun, start: Time = Time.hms(0, 17, 0)): Timed =
+ Timed(Date.Weekly(day, Date.Daily(start)))
}
- case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
+ case class Timed(cycle: Date.Cycle) extends Trigger {
+ def next(previous: Date, now: Date): Boolean = cycle.next(previous).time < cycle.next(now).time
+ }
/* build hooks */
--- a/src/Pure/Build/build_manager.scala Mon Jan 20 22:20:14 2025 +0100
+++ b/src/Pure/Build/build_manager.scala Tue Jan 21 11:17:05 2025 +0100
@@ -1135,7 +1135,7 @@
private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
for (ci_job <- ci_jobs)
ci_job.trigger match {
- case Build_CI.Timed(in_interval) if in_interval(previous, next) =>
+ case timer: Build_CI.Timed if timer.next(previous, next) =>
val task = CI_Build.task(ci_job)
echo("Triggered task " + task.kind)
_state = _state.add_pending(task)
@@ -1411,7 +1411,7 @@
def render_diff(data: Report.Data, components: List[Component]): XML.Body =
par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) ::
(for (component <- components if !component.is_local) yield {
- val infos =
+ val infos =
data.component_logs.toMap.get(component.name).toList.flatMap(colored) :::
data.component_diffs.toMap.get(component.name).toList.flatMap(colored)
@@ -1508,7 +1508,7 @@
Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
HTML.style("""
-:root {
+:root {
--color-secondary: var(--color-tertiary);
--color-secondary-hover: var(--color-tertiary-hover);
}
@@ -1894,7 +1894,7 @@
progress.interrupt_handler {
using(store.open_ssh()) { ssh =>
val user = ssh.execute("whoami").check.out
-
+
val build_config = User_Build(user, afp_rev, prefs, requirements, all_sessions,
base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions,
build_heap, clean_build, export_files, fresh_build, presentation, verbose)
--- a/src/Pure/General/date.scala Mon Jan 20 22:20:14 2025 +0100
+++ b/src/Pure/General/date.scala Tue Jan 21 11:17:05 2025 +0100
@@ -10,7 +10,7 @@
import java.util.Locale
import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
import java.time.format.{DateTimeFormatter, DateTimeParseException}
-import java.time.temporal.TemporalAccessor
+import java.time.temporal.{ChronoUnit, TemporalAccessor}
import scala.annotation.tailrec
@@ -99,9 +99,67 @@
def apply(t: Time, timezone: ZoneId = Date.timezone()): Date =
instant(t.instant, timezone)
+
+
+ /* varying-length calendar cycles */
+
+ enum Day { case mon, tue, wed, thu, fri, sat, sun }
+ enum Month { case jan, feb, mar, apr, may, jun, jul, aug, sep, okt, nov, dec }
+
+ sealed trait Cycle {
+ def zero(date: Date): Date
+ def next(date: Date): Date
+ }
+
+ case class Daily(at: Time = Time.zero) extends Cycle {
+ require(at >= Time.zero && at < Time.hms(24, 0, 0))
+
+ def zero(date: Date): Date = date.midnight
+ def next(date: Date): Date = {
+ val start = zero(date) + at
+ if (date.time < start.time) start else start.shift(1)
+ }
+
+ override def toString: String = "Daily(" + Format.time(Date(at, timezone_utc)) + ")"
+ }
+
+ case class Weekly(on: Day = Day.mon, step: Daily = Daily()) extends Cycle {
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfWeek.getValue).midnight
+ def next(date: Date): Date = {
+ val next = step.next(zero(date).shift(on.ordinal) - Time.ms(1))
+ if (date.time < next.time) next else Date(next.rep.plus(1, ChronoUnit.WEEKS))
+ }
+ }
+
+ case class Monthly(nth: Int = 1, step: Daily = Daily()) extends Cycle {
+ require(nth > 0 && nth <= 31)
+
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfMonth).midnight
+ def next(date: Date): Date = {
+ @tailrec def find_next(zero: Date): Date = {
+ val next = step.next(zero.shift(nth - 1) - Time.ms(1))
+ if (next.rep.getDayOfMonth == nth && date.time < next.time) next
+ else find_next(Date(zero.rep.plus(1, ChronoUnit.MONTHS)))
+ }
+ find_next(zero(date))
+ }
+ }
+
+ case class Yearly(in: Month = Month.jan, step: Monthly = Monthly()) extends Cycle {
+ def zero(date: Date): Date = date.shift(1 - date.rep.getDayOfYear).midnight
+ def next(date: Date): Date = {
+ @tailrec def find_next(zero: Date): Date = {
+ val next = step.next(Date(zero.rep.plus(in.ordinal, ChronoUnit.MONTHS)) - Time.ms(1))
+ if (next.rep.getMonthValue - 1 == in.ordinal && date.time < next.time) next
+ else find_next(Date(zero.rep.plus(1, ChronoUnit.YEARS)))
+ }
+ find_next(zero(date))
+ }
+ }
}
sealed case class Date(rep: ZonedDateTime) {
+ def shift(days: Int): Date = Date(rep.plus(days, ChronoUnit.DAYS))
def midnight: Date =
new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
--- a/src/Tools/Find_Facts/src/find_facts.scala Mon Jan 20 22:20:14 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Tue Jan 21 11:17:05 2025 +0100
@@ -577,9 +577,25 @@
} yield block)
}
+ def find_facts_index_command(
+ sessions: List[String],
+ ssh: SSH.System = SSH.Local,
+ isabelle_home: Path = Path.current,
+ options: List[Options.Spec] = Nil,
+ dirs: List[Path] = Nil,
+ clean: Boolean = false
+ ): String = {
+ ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " find_facts_index" +
+ dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
+ if_proper(clean, " -c") +
+ Options.Spec.bash_strings(options, bg = true) +
+ sessions.map(session => " " + session).mkString
+ }
+
def find_facts_index(
options: Options,
sessions: List[String],
+ afp_root: Option[Path] = None,
dirs: List[Path] = Nil,
clean: Boolean = false,
progress: Progress = new Progress
@@ -589,7 +605,8 @@
val session = Session(options, Resources.bootstrap)
val selection = Sessions.Selection(sessions = sessions)
- val session_structure = Sessions.load_structure(options, dirs = dirs).selection(selection)
+ val session_structure =
+ Sessions.load_structure(options, dirs = AFP.main_dirs(afp_root) ::: dirs).selection(selection)
val deps = Sessions.Deps.load(session_structure)
val browser_info_context = Browser_Info.context(session_structure)
@@ -599,7 +616,7 @@
using(Solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
using(Export.open_database_context(store)) { database_context =>
val document_info = Document_Info.read(database_context, deps, sessions)
-
+
def index_session(session_name: String): Unit = {
using(database_context.open_session0(session_name)) { session_context =>
val info = session_structure(session_name)
@@ -638,6 +655,7 @@
def main_tool1(args: Array[String]): Unit = {
Command_Line.tool {
+ var afp_root: Option[Path] = None
var clean = false
val dirs_buffer = new mutable.ListBuffer[Path]
var no_build = false
@@ -648,6 +666,7 @@
Usage: isabelle find_facts_index [OPTIONS] [SESSIONS ...]
Options are:
+ -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
-c clean previous index
-d DIR include session directory
-n no build -- take existing session build databases
@@ -656,6 +675,7 @@
Build and index sessions for Find_Facts.
""",
+ "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
"c" -> (_ => clean = true),
"d:" -> (arg => dirs_buffer += Path.explode(arg)),
"n" -> (_ => no_build = true),
@@ -673,7 +693,7 @@
if (!no_build) {
def build(test: Boolean = false): Build.Results =
Build.build(options, selection = Sessions.Selection(sessions = sessions), dirs = dirs,
- no_build = test, progress = if (test) new Progress else progress)
+ afp_root = afp_root, no_build = test, progress = if (test) new Progress else progress)
progress.interrupt_handler {
if (!build(test = true).ok) {
@@ -690,12 +710,12 @@
/* index */
- find_facts_index(options, sessions, dirs = dirs, clean = clean, progress = progress)
+ find_facts_index(options, sessions, dirs = dirs, afp_root = afp_root, clean = clean,
+ progress = progress)
}
}
-
/** index components **/
def find_facts_index_component(