| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/Build/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 74 kB |
|
Quelle build_manager.scala Sprache: Scala |
|||||||||
|
/* Title: Pure/Build/build_manager.scala
Author: Fabian Huch, TU Muenchen Isabelle manager for automated and quasi-interactive builds, with web frontend. */ package isabelle import scala.collection.mutable import scala.annotation.tailrec object Build_Manager { /** task state synchronized via db **/ object Component { def parse(s: String): Component = space_explode('/', s) match { case name :: Nil => Component(name) case name :: rev :: Nil => Component(name, rev) case _ => error("Malformed component: " + quote(s)) } val Isabelle = "Isabelle" val AFP = "AFP" def isabelle(rev: String = "") = Component(Isabelle, rev) def afp(rev: String = "") = Component(AFP, rev) } case class Component(name: String, rev: String = "") { override def toString: String = name + if_proper(rev, "/" + rev) def is_local: Boolean = rev.isEmpty } sealed trait Build_Config { def name: String def extra_components: List[Component] def fresh_build: Boolean def build_cluster: Boolean def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String } object CI_Build { def apply(job: Build_CI.Job): CI_Build = CI_Build(job.name, job.hosts.build_cluster, job.components.map(Component(_, "defaul def task(job: Build_CI.Job): Task = Task(CI_Build(job), job.hosts.hosts_spec, job.timeout, other_settings = job.other_set isabelle_rev = "default") } case class CI_Build(name: String, build_cluster: Boolean, extra_components: List[Compon extends Build_Config { def fresh_build: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = " build_ci" + " -u " + Bash.string(job_url.toString) + if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkS " " + name } object User_Build { val name: String = "user" } case class User_Build( user: String, afp_rev: Option[String] = None, prefs: List[Options.Spec] = Nil, requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil, build_heap: Boolean = false, clean_build: Boolean = false, export_files: Boolean = false, fresh_build: Boolean = false, presentation: Boolean = false, verbose: Boolean = false ) extends Build_Config { def name: String = User_Build.name def extra_components: List[Component] = afp_rev.map(Component.afp).toList def build_cluster: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = { " build" + if_proper(afp_rev, " -A:") + base_sessions.map(session => " -B " + Bash.string(session)).mkString + build_hosts.map(host => " -H " + Bash.string(host.print)).mkString + if_proper(presentation, " -P:") + if_proper(requirements, " -R") + exclude_session_groups.map(session => " -X " + Bash.string(session)).mkString + if_proper(all_sessions, " -a") + if_proper(build_heap, " -b") + if_proper(clean_build, " -c") + if_proper(export_files, " -e") + if_proper(fresh_build, " -f") + session_groups.map(session => " -g " + Bash.string(session)).mkString + Options.Spec.bash_strings(prefs, bg = true) + if_proper(verbose, " -v") + exclude_sessions.map(session => " -x " + Bash.string(session)).mkString + sessions.map(session => " " + Bash.string(session)).mkString } } enum Priority { case low, normal, high } object Build { def name(kind: String, id: Long): String = kind + "/" + id } sealed trait Build extends Name.T sealed case class Task( build_config: Build_Config, hosts_spec: String, timeout: Time, other_settings: List[String] = Nil, uuid: UUID.T = UUID.random(), submit_date: Date = Date.now(), priority: Priority = Priority.normal, isabelle_rev: String = "" ) extends Build { def name: String = uuid.toString def kind: String = build_config.name def user: Option[String] = Some(build_config).collect { case build: User_Build => build.use def components: List[Component] = Component.isabelle(isabelle_rev) :: extra_components def extra_components: List[Component] = build_config.extra_components def build_cluster = build_config.build_cluster def build_hosts: List[Build_Cluster.Host] = Build_Cluster.Host.parse(Registry.global, hosts_spec) def >(t: Task): Boolean = priority.ordinal > t.priority.ordinal || (priority == t.priority && submit_date.time < t.submit_date.time) } sealed case class Job( uuid: UUID.T, kind: String, id: Long, build_cluster: Boolean, hostnames: List[String], components: List[Component], timeout: Time, user: Option[String], start_date: Date = Date.now(), cancelled: Boolean = false ) extends Build { def name: String = Build.name(kind, id) } object Status { def from_result(result: Process_Result): Status = { if (result.ok) Status.ok else if (result.interrupted) Status.cancelled else Status.failed } } enum Status { case ok, cancelled, aborted, failed } sealed case class Result( kind: String, id: Long, status: Status, uuid: Option[UUID.T], build_host: String, start_date: Date, end_date: Option[Date], isabelle_version: Option[String], afp_version: Option[String], user: Option[String], serial: Long = 0, ) extends Build { def name: String = Build.name(kind, id) def components: List[Component] = isabelle_version.map(Component.isabelle).toList ::: afp_version.map(Component.afp) } object State { def max_serial(serials: Iterable[Long]): Long = serials.maxOption.getOrElse(0L) def inc_serial(serial: Long): Long = { require(serial < Long.MaxValue, "number overflow") serial + 1 } type Pending = Name.Data[Task] type Running = Name.Data[Job] type Finished = Map[String, Result] } sealed case class State( serial: Long = 0, pending: State.Pending = Map.empty, running: State.Running = Map.empty, finished: State.Finished = Map.empty ) { def next_serial: Long = State.inc_serial(serial) def add_pending(task: Task): State = copy(pending = pending + (task.name -> task)) def remove_pending(name: String): State = copy(pending = pending - name) def num_builds = running.size + finished.size def next(build_hosts: List[Build_Cluster.Host]): Option[Task] = { val cluster_running = running.values.exists(_.build_cluster) val available = build_hosts.map(_.hostname).toSet -- running.values.flatMap(_.hostnam val ready = for { (_, task) <- pending if !task.build_cluster || !cluster_running if task.build_hosts.map(_.hostname).forall(available.contains) } yield task if (ready.isEmpty) None else { val priority = ready.map(_.priority).maxBy(_.ordinal) ready.filter(_.priority == priority).toList.sortBy(_.submit_date)(Date.Ordering).h } } def add_running(job: Job): State = copy(running = running + (job.name -> job)) def remove_running(name: String): State = copy(running = running - name) def cancel_running(name: String): State = running.get(name) match { case Some(job) => copy(running = (running - name) + (name -> job.copy(cancelled = true))) case None => this } def add_finished(result: Result): State = copy(finished = finished + (result.name -> result) lazy val kinds = ( pending.values.map(_.kind) ++ running.values.map(_.kind) ++ finished.values.map(_.kind)).toList.distinct def next_id(kind: String): Long = { val serials = get_finished(kind).map(_.id) ::: get_running(kind).map(_.id) State.inc_serial(State.max_serial(serials)) } def get_running(kind: String): List[Job] = (for ((_, job) <- running if job.kind == kind) yield job).toList def get_finished(kind: String): List[Result] = (for ((_, result) <- finished if result.kind == kind) yield result).toList def get(name: String): Option[Build] = pending.get(name).orElse(running.get(name)).orElse(finished.get(name)) def get(uuid: UUID.T): Option[Build] = pending.values.find(_.uuid == uuid).orElse( running.values.find(_.uuid == uuid)).orElse( finished.values.find(_.uuid.contains(uuid))) } /** SQL data model **/ object private_data extends SQL.Data("isabelle_build_manager") { /* tables */ override lazy val tables: SQL.Tables = SQL.Tables(State.table, Pending.table, Running.table, Finished.table) /* state */ object State { val serial = SQL.Column.long("serial").make_primary_key val table = make_table(List(serial), name = "state") } def read_serial(db: SQL.Database): Long = db.execute_query_statementO[Long]( State.table.select(List(State.serial.max)), _.long(State.serial)).getOrElse(0L) def pull_state(db: SQL.Database, state: State): State = { val serial_db = read_serial(db) if (serial_db == state.serial) state else { val serial = serial_db max state.serial val pending = pull_pending(db) val running = pull_running(db) val finished = pull_finished(db, state.finished) state.copy(serial = serial, pending = pending, running = running, finished = finished) } } def push_state(db: SQL.Database, old_state: State, state: State): State = { val finished = push_finished(db, state.finished) val updates = List( update_pending(db, old_state.pending, state.pending), update_running(db, old_state.running, state.running), ).filter(_.defined) if (updates.isEmpty && finished == old_state.finished) state else { val serial = state.next_serial db.execute_statement(State.table.delete(State.serial.where_equal(old_state.seria db.execute_statement(State.table.insert(), body = { (stmt: SQL.Statement) => stmt.long(1) = serial }) state.copy(serial = serial, finished = finished) } } /* pending */ object Pending { val kind = SQL.Column.string("kind") val build_cluster = SQL.Column.bool("build_cluster") val hosts_spec = SQL.Column.string("hosts_spec") val timeout = SQL.Column.long("timeout") val other_settings = SQL.Column.string("other_settings") val uuid = SQL.Column.string("uuid").make_primary_key val submit_date = SQL.Column.date("submit_date") val priority = SQL.Column.string("priority") val isabelle_rev = SQL.Column.string("isabelle_rev") val extra_components = SQL.Column.string("extra_components") val user = SQL.Column.string("user") val prefs = SQL.Column.string("prefs") val requirements = SQL.Column.bool("requirements") val all_sessions = SQL.Column.bool("all_sessions") val base_sessions = SQL.Column.string("base_sessions") val exclude_session_groups = SQL.Column.string("exclude_session_groups") val exclude_sessions = SQL.Column.string("exclude_sessions") val session_groups = SQL.Column.string("session_groups") val sessions = SQL.Column.string("sessions") val build_heap = SQL.Column.bool("build_heap") val clean_build = SQL.Column.bool("clean_build") val export_files = SQL.Column.bool("export_files") val fresh_build = SQL.Column.bool("fresh_build") val presentation = SQL.Column.bool("presentation") val verbose = SQL.Column.bool("verbose") val table = make_table(List(kind, build_cluster, hosts_spec, timeout, other_settings, uuid, submit priority, isabelle_rev, extra_components, user, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, fresh_build, presentation, verbose), name = "pending") } def pull_pending(db: SQL.Database): Build_Manager.State.Pending = db.execute_query_statement(Pending.table.select(), Map.from[String, Task], get = { res => val kind = res.string(Pending.kind) val build_cluster = res.bool(Pending.build_cluster) val hosts_spec = res.string(Pending.hosts_spec) val timeout = Time.ms(res.long(Pending.timeout)) val other_settings = split_lines(res.string(Pending.other_settings)) val uuid = res.string(Pending.uuid) val submit_date = res.date(Pending.submit_date) val priority = Priority.valueOf(res.string(Pending.priority)) val isabelle_rev = res.string(Pending.isabelle_rev) val extra_components = space_explode(',', res.string(Pending.extra_components)).map(Component.parse) val build_config = if (kind != User_Build.name) CI_Build(kind, build_cluster, extra_components) else { val user = res.string(Pending.user) val prefs = Options.Spec.parse(res.string(Pending.prefs)) val requirements = res.bool(Pending.requirements) val all_sessions = res.bool(Pending.all_sessions) val base_sessions = space_explode(',', res.string(Pending.base_sessions)) val exclude_session_groups = space_explode(',', res.string(Pending.exclude_session_groups)) val exclude_sessions = space_explode(',', res.string(Pending.exclude_sessions)) val session_groups = space_explode(',', res.string(Pending.session_groups)) val sessions = space_explode(',', res.string(Pending.sessions)) val build_heap = res.bool(Pending.build_heap) val clean_build = res.bool(Pending.clean_build) val export_files = res.bool(Pending.export_files) val fresh_build = res.bool(Pending.fresh_build) val presentation = res.bool(Pending.presentation) val verbose = res.bool(Pending.verbose) val afp_rev = extra_components.find(_.name == Component.AFP).map(_.rev) 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) } val task = Task(build_config, hosts_spec, timeout, other_settings, UUID.make(uuid), submit_date, priority, isabelle_rev) task.name -> task }) def update_pending( db: SQL.Database, old_pending: Build_Manager.State.Pending, pending: Build_Manager.State.Pending ): Update = { val update = Update.make(old_pending, pending) val delete = update.delete.map(old_pending(_).uuid.toString) if (update.deletes) db.execute_statement(Pending.table.delete(Pending.uuid.where_member(delete))) if (update.inserts) { db.execute_batch_statement(Pending.table.insert(), batch = for (name <- update.insert) yield { (stmt: SQL.Statement) => val task = pending(name) stmt.string(1) = task.kind stmt.bool(2) = task.build_cluster stmt.string(3) = task.hosts_spec stmt.long(4) = task.timeout.ms stmt.string(5) = cat_lines(task.other_settings) stmt.string(6) = task.uuid.toString stmt.date(7) = task.submit_date stmt.string(8) = task.priority.toString stmt.string(9) = task.isabelle_rev stmt.string(10) = task.extra_components.mkString(",") stmt.string(11) = task.user def get[A](f: User_Build => A): Option[A] = task.build_config match { case user_build: User_Build => Some(f(user_build)) case _ => None } stmt.string(12) = get(user_build => user_build.prefs.map(_.print).mkString(",")) stmt.bool(13) = get(_.requirements) stmt.bool(14) = get(_.all_sessions) stmt.string(15) = get(_.base_sessions.mkString(",")) stmt.string(16) = get(_.exclude_session_groups.mkString(",")) stmt.string(17) = get(_.exclude_sessions.mkString(",")) stmt.string(18) = get(_.session_groups.mkString(",")) stmt.string(19) = get(_.sessions.mkString(",")) stmt.bool(20) = get(_.build_heap) stmt.bool(21) = get(_.clean_build) stmt.bool(22) = get(_.export_files) stmt.bool(23) = get(_.fresh_build) stmt.bool(24) = get(_.presentation) stmt.bool(25) = get(_.verbose) }) } update } /* running */ object Running { val uuid = SQL.Column.string("uuid").make_primary_key val kind = SQL.Column.string("kind") val id = SQL.Column.long("id") val build_cluster = SQL.Column.bool("build_cluster") val hostnames = SQL.Column.string("hostnames") val components = SQL.Column.string("components") val timeout = SQL.Column.long("timeout") val user = SQL.Column.string("user") val start_date = SQL.Column.date("start_date") val cancelled = SQL.Column.bool("cancelled") val table = make_table(List(uuid, kind, id, build_cluster, hostnames, components, timeout, user, start_date, cancelled), name = "running") } def pull_running(db: SQL.Database): Build_Manager.State.Running = db.execute_query_statement(Running.table.select(), Map.from[String, Job], get = { res => val uuid = res.string(Running.uuid) val kind = res.string(Running.kind) val id = res.long(Running.id) val build_cluster = res.bool(Running.build_cluster) val hostnames = space_explode(',', res.string(Running.hostnames)) val components = space_explode(',', res.string(Running.components)).map(Component.pa val timeout = Time.ms(res.long(Running.timeout)) val user = res.get_string(Running.user) val start_date = res.date(Running.start_date) val cancelled = res.bool(Running.cancelled) val job = Job(UUID.make(uuid), kind, id, build_cluster, hostnames, components, timeout, user, start_date, cancelled) job.name -> job }) def update_running( db: SQL.Database, old_running: Build_Manager.State.Running, running: Build_Manager.State.Running ): Update = { val update = Update.make(old_running, running) val delete = update.delete.map(old_running(_).uuid.toString) if (update.deletes) db.execute_statement(Running.table.delete(Running.uuid.where_member(delete))) if (update.inserts) { db.execute_batch_statement(Running.table.insert(), batch = for (name <- update.insert) yield { (stmt: SQL.Statement) => val job = running(name) stmt.string(1) = job.uuid.toString stmt.string(2) = job.kind stmt.long(3) = job.id stmt.bool(4) = job.build_cluster stmt.string(5) = job.hostnames.mkString(",") stmt.string(6) = job.components.mkString(",") stmt.long(7) = job.timeout.ms stmt.string(8) = job.user stmt.date(9) = job.start_date stmt.bool(10) = job.cancelled }) } update } /* finished */ object Finished { val kind = SQL.Column.string("kind") val id = SQL.Column.long("id") val status = SQL.Column.string("status") val uuid = SQL.Column.string("uuid") val build_host = SQL.Column.string("build_host") val start_date = SQL.Column.date("start_date") val end_date = SQL.Column.date("end_date") val isabelle_version = SQL.Column.string("isabelle_version") val afp_version = SQL.Column.string("afp_version") val user = SQL.Column.string("user") val serial = SQL.Column.long("serial").make_primary_key val table = make_table( List(kind, id, status, uuid, build_host, start_date, end_date, isabelle_version, afp_version, user, serial), name = "finished") } def read_finished_serial(db: SQL.Database): Long = db.execute_query_statementO[Long]( Finished.table.select(List(Finished.serial.max)), _.long(Finished.serial)).getOrElse(0L) def pull_finished( db: SQL.Database, finished: Build_Manager.State.Finished ): Build_Manager.State.Finished = { val max_serial0 = Build_Manager.State.max_serial(finished.values.map(_.serial)) val max_serial1 = read_finished_serial(db) val missing = (max_serial0 + 1) to max_serial1 finished ++ db.execute_query_statement( Finished.table.select(sql = Finished.serial.where_member_long(missing)), Map.from[String, Result], get = { res => val kind = res.string(Finished.kind) val id = res.long(Finished.id) val status = Status.valueOf(res.string(Finished.status)) val uuid = res.get_string(Finished.uuid).map(UUID.make) val build_host = res.string(Finished.build_host) val start_date = res.date(Finished.start_date) val end_date = res.get_date(Finished.end_date) val isabelle_version = res.get_string(Finished.isabelle_version) val afp_version = res.get_string(Finished.afp_version) val user = res.get_string(Finished.user) val serial = res.long(Finished.serial) val result = Result(kind, id, status, uuid, build_host, start_date, end_date, isabelle_version, afp_version, user, serial) result.name -> result } ) } def push_finished( db: SQL.Database, finished: Build_Manager.State.Finished ): Build_Manager.State.Finished = { val (insert0, old) = finished.partition(_._2.serial == 0L) val max_serial = Build_Manager.State.max_serial(finished.map(_._2.serial)) val insert = for (((_, result), n) <- insert0.zipWithIndex) yield result.copy(serial = max_serial + 1 + n) if (insert.nonEmpty) db.execute_batch_statement(Finished.table.insert(), batch = for (result <- insert) yield { (stmt: SQL.Statement) => stmt.string(1) = result.kind stmt.long(2) = result.id stmt.string(3) = result.status.toString stmt.string(4) = result.uuid.map(_.toString) stmt.string(5) = result.build_host stmt.date(6) = result.start_date stmt.date(7) = result.end_date stmt.string(8) = result.isabelle_version stmt.string(9) = result.afp_version stmt.string(10) = result.user stmt.long(11) = result.serial }) old ++ insert.map(result => result.serial.toString -> result) } } /** build reports **/ object Report { case class Data( build_log: String, component_logs: List[(String, String)], component_diffs: List[(String, String)]) } case class Report(kind: String, id: Long, dir: Path) { private val log_name = "build-manager" private val diff_ext = "diff" private val log_ext = "log" private def log_file = dir + Path.basic(log_name).log private def log_file_gz = dir + Path.basic(log_name).log.gz def init(): Unit = Isabelle_System.make_directory(dir) def ok: Boolean = log_file.is_file != log_file_gz.is_file def progress: Progress = new File_Progress(log_file) private def read_gz(file: Path, ext: String): Option[(String, String)] = if (!File.is_gz(file.file_name) || file.drop_ext.get_ext != ext) None else Some(file.drop_ext.drop_ext.file_name -> File.read_gzip(file)) def read: Report.Data = { val build_log = if_proper(ok, if (log_file.is_file) File.read(log_file) else File.read_gzip(log_file_ val component_diffs = File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), diff_ext)) val component_logs = File.read_dir(dir).flatMap(name => read_gz(dir + Path.basic(name), log_ext)) Report.Data(build_log, component_logs, component_diffs) } def write_log( component: String, repository: Mercurial.Repository, rev0: String, rev: String ): Unit = if (rev0.nonEmpty && rev.nonEmpty && rev0 != rev) { val log_opts = "--graph --color always" val rev1 = "children(" + rev0 + ")" val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts) val log = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log) } def write_diff( component: String, repository: Mercurial.Repository, rev0: String, rev: String ): Unit = if (rev0.nonEmpty && rev.nonEmpty) { val diff_opts = "--noprefix --nodates --ignore-all-space --color always" val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts) val diff = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff } def result(uuid: Option[UUID.T] = None, user: Option[String] = None): Result = { val End = """^Job ended at [^,]+, with status (\w+)$""".r val build_log_file = Build_Log.Log_File(log_name, Library.trim_split_lines(read.buil val meta_info = build_log_file.parse_meta_info() val status = build_log_file.lines.last match { case End(status) => Status.valueOf(status) case _ => Status.aborted } val build_host = meta_info.get_build_host.getOrElse(error("No build host")) val start_date = meta_info.get_build_start.getOrElse(error("No start date")) val end_date = meta_info.get_build_end val isabelle_version = meta_info.get(Build_Log.Prop.isabelle_version) val afp_version = meta_info.get(Build_Log.Prop.afp_version) if (log_file.is_file) { File.write_gzip(log_file_gz, build_log_file.text) Isabelle_System.rm_tree(log_file) } Result(kind, id, status, uuid, build_host, start_date, end_date, isabelle_version, afp_version, user) } } /** running build manager processes **/ abstract class Loop_Process[A](name: String, store: Store, progress: Progress) extends Runnable { val options = store.options private val _database = try { store.open_database() } catch { case exn: Throwable => close(); throw exn } def close(): Unit = Option(_database).foreach(_.close()) protected var _state = State() protected def synchronized_database[A](label: String)(body: => A): A = synchronized { Build_Manager.private_data.transaction_lock(_database, label = name + "." + label) { val old_state = Build_Manager.private_data.pull_state(_database, _state) _state = old_state val res = body _state = Build_Manager.private_data.push_state(_database, old_state, _state) res } } protected def delay = options.seconds("build_manager_delay") def init: A def loop_body(a: A): A def stopped(a: A): Boolean = progress.stopped private val interrupted = Synchronized(false) private def sleep(time_limit: Time): Unit = interrupted.timed_access(_ => Some(time_limit), b => if (b) Some((), false) else None) def interrupt(): Unit = interrupted.change(_ => true) @tailrec private def loop(a: A): Unit = if (!stopped(a)) { val start = Time.now() val a1 = loop_body(a) if (!stopped(a)) { sleep(start + delay) loop(a1) } } override def run(): Unit = { progress.echo("Started " + name) loop(init) close() progress.echo("Stopped " + name) } def echo(msg: String) = progress.echo(name + ": " + msg) def echo_error_message(msg: String) = progress.echo_error_message(name + ": " + msg) } /* build runner */ object Runner { object State { def init(options: Options): State = new State(Map.empty, Map.empty, Map.empty, options.seconds("build_manager_cancel_tim } class State private( process_futures: Map[String, Future[Build_Process]], result_futures: Map[String, Future[Process_Result]], cancelling_until: Map[String, Time], cancel_timeout: Time ) { private def copy( process_futures: Map[String, Future[Build_Process]] = process_futures, result_futures: Map[String, Future[Process_Result]] = result_futures, cancelling_until: Map[String, Time] = cancelling_until, ): State = new State(process_futures, result_futures, cancelling_until, cancel_timeout) def is_empty = process_futures.isEmpty && result_futures.isEmpty def init(context: Context): State = { val process_future = Future.fork(Build_Process.open(context)) val result_future = Future.fork( process_future.join_result match { case Exn.Res(process) => process.run() case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessag }) copy( process_futures + (context.name -> process_future), result_futures + (context.name -> result_future)) } def running: List[String] = process_futures.keys.toList.filterNot(cancelling_until.c private def maybe_result(name: String): Option[Process_Result] = for (future <- result_futures.get(name) if future.is_finished) yield future.join_result match { case Exn.Res(result) => result case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessag } private def do_terminate(name: String): Boolean = { val is_late = Time.now() > cancelling_until(name) if (is_late) process_futures(name).join.terminate() is_late } def update: (State, Map[String, Process_Result]) = { val finished0 = for { (name, _) <- result_futures result <- maybe_result(name) } yield name -> result val (terminated, cancelling_until1) = cancelling_until .filterNot((name, _) => finished0.contains(name)) .partition((name, _) => do_terminate(name)) val finished = finished0 ++ terminated.map((name, _) => name -> maybe_result(name).getOrElse(Process_Result(Process_Result.RC.timeout))) val state1 = copy( process_futures.filterNot((name, _) => finished.contains(name)), result_futures.filterNot((name, _) => finished.contains(name)), cancelling_until1) (state1, finished) } private def do_cancel(process_future: Future[Build_Process]): Boolean = { val is_finished = process_future.is_finished if (is_finished) process_future.join.cancel() else process_future.cancel() is_finished } def cancel(cancelled: List[String]): State = { val cancelling_until1 = for { name <- cancelled process_future <- process_futures.get(name) if do_cancel(process_future) } yield name -> (Time.now() + cancel_timeout) copy(cancelling_until = cancelling_until ++ cancelling_until1) } } } class Runner( store: Store, build_hosts: List[Build_Cluster.Host], isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], progress: Progress ) extends Loop_Process[Runner.State]("Runner", store, progress) { val rsync_context = Rsync.Context() private def sync(repository: Mercurial.Repository, rev: String, target: Path): String = { val pull_result = Exn.capture(repository.pull()) if (Exn.is_exn(pull_result)) { echo_error_message("Could not read from repository: " + Exn.the_exn(pull_result).g } if (rev.nonEmpty) repository.sync(rsync_context, target, rev = rev) Exn.capture(repository.id(File.read(target + Mercurial.Hg_Sync.PATH_ID))) match { case Exn.Res(res) => res case Exn.Exn(_) => "" } } private def start_next(): Option[Context] = synchronized_database("start_next") { for ((name, task) <- _state.pending if Exn.is_exn(Exn.capture(task.build_hosts))) { progress.echo("Invalid host spec for task " + name + ": " + quote(task.hosts_spec)) _state = _state.remove_pending(name) } _state.next(build_hosts).flatMap { task => echo("Initializing " + task.name) _state = _state.remove_pending(task.name) val id = _state.next_id(task.kind) val context = Context(store, task, id) val start_date = Date.now() val start_msg = "Starting job " + Build.name(task.kind, id) + " at " + Build_Log.print_date(start_date) + "," + " on " + ( if (task.build_cluster) "cluster" else Library.the_single(task.build_hosts).hostname) echo(start_msg + " (id " + task.uuid + ")") Exn.capture { context.report.init() context.report.progress.echo(start_msg) store.sync_permissions(context.task_dir) val isabelle_rev = sync(isabelle_repository, task.isabelle_rev, context.task_dir) val hostnames = task.build_hosts.map(_.hostname).distinct val extra_components = for (extra_component <- task.extra_components) yield sync_dirs.find(_.name == extra_component.name) match { case Some(sync_dir) => val target = context.task_dir + sync_dir.target val rev = sync(sync_dir.hg, extra_component.rev, target) if (!extra_component.is_local) File.append(context.task_dir + Sync.DIRS_ROOTS, sync_dir.roots_entry + "\n") extra_component.copy(rev = rev) case None => if (extra_component.is_local) extra_component else error("Unknown component " + extra_component) } if (task.kind != User_Build.name && _state.get_finished(task.kind).nonEmpty) { val previous = _state.get_finished(task.kind).maxBy(_.id) for (isabelle_rev0 <- previous.isabelle_version) { context.report.write_log(Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev) context.report.write_diff(Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev) } for { afp_rev0 <- previous.afp_version afp <- extra_components.find(_.name == Component.AFP) sync_dir <- sync_dirs.find(_.name == afp.name) } { context.report.write_log(afp.name, sync_dir.hg, afp_rev0, afp.rev) context.report.write_diff(afp.name, sync_dir.hg, afp_rev0, afp.rev) } } val components = Component.isabelle(isabelle_rev) :: extra_components Job(task.uuid, task.kind, id, task.build_cluster, hostnames, components, task.timeout, task.user, start_date) } match { case Exn.Res(job) => _state = _state.add_running(job) for (component <- job.components) context.report.progress.echo("Using " + component.toString) Some(context) case Exn.Exn(exn) => context.report.progress.echo_error_message("Failed to start job: " + exn.getMessag echo_error_message("Failed to start " + task.uuid + ": " + exn.getMessage) Isabelle_System.rm_tree(context.task_dir) _state = _state.add_finished(context.report.result(Some(task.uuid), task.user)) None } } } private def stop_cancelled(state: Runner.State): Runner.State = synchronized_database("stop_cancelled") { val now = Date.now() for { name <- state.running job = _state.running(name) if now - job.start_date > job.timeout } { _state = _state.cancel_running(name) val timeout_msg = "Timeout after " + job.timeout.message_hms store.report(job.kind, job.id).progress.echo_error_message(timeout_msg) echo(job.name + ": " + timeout_msg) } val cancelled = for { name <- state.running job = _state.running(name) if job.cancelled } yield job cancelled.foreach(job => store.report(job.kind, job.id).progress.echo("Cancelling .. state.cancel(cancelled.map(_.name)) } private def finish_job(name: String, process_result: Process_Result): Unit = synchronized_database("finish_job") { val job = _state.running(name) val end_date = Date.now() val status = Status.from_result(process_result) val end_msg = "Job ended at " + Build_Log.print_date(end_date) + ", with status " + statu val report = store.report(job.kind, job.id) report.progress.echo(end_msg) val interrupted_error = process_result.interrupted && process_result.err.nonEmpty val err_msg = if_proper(interrupted_error, ": " + process_result.err) echo(end_msg + " (code " + process_result.rc + ")" + err_msg) _state = _state .remove_running(job.name) .add_finished(report.result(Some(job.uuid), job.user)) } override def stopped(state: Runner.State): Boolean = progress.stopped && state.is_empty def init: Runner.State = synchronized_database("init") { for ((name, job) <- _state.running) { echo("Cleaned up job " + job.uuid) val report = store.report(job.kind, job.id) _state = _state .remove_running(job.name) .add_finished(report.result(Some(job.uuid), job.user)) } Runner.State.init(store.options) } def loop_body(state: Runner.State): Runner.State = { val state1 = if (progress.stopped) state else { start_next() match { case None => state case Some(context) => state.init(context) } } val state2 = stop_cancelled(state1) val (state3, results) = state2.update results.foreach(finish_job) state3 } } /* repository poller */ object Poller { case class State(current: List[Component], next: Future[List[Component]]) } class Poller( ci_jobs: List[Build_CI.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], progress: Progress ) extends Loop_Process[Poller.State]("Poller", store, progress) { override def delay = options.seconds("build_manager_poll_delay") private def current: List[Component] = Component.isabelle(isabelle_repository.id("default")) :: sync_dirs.map(dir => Component(dir.name, dir.hg.id("default"))) private def poll: Future[List[Component]] = Future.fork { Par_List.map((repo: Mercurial.Repository) => repo.pull(), isabelle_repository :: sync_dirs.map(_.hg)) current } val init: Poller.State = Poller.State(current, poll) private def add_tasks(current: List[Component], next: List[Component]): Unit = { val next_rev = next.map(component => component.name -> component.rev).toMap def is_unchanged(components: List[Component]): Boolean = components.forall(component => next_rev.get(component.name).contains(component.rev) def is_changed(component_names: List[String]): Boolean = !is_unchanged(current.filter(component => component_names.contains(component.name)) def is_current(job: Job): Boolean = is_unchanged(job.components) synchronized_database("add_tasks") { for { ci_job <- ci_jobs if ci_job.trigger == Build_CI.On_Commit if is_changed(Component.Isabelle :: ci_job.components) if !_state.pending.values.exists(_.kind == ci_job.name) if !_state.running.values.filter(_.kind == ci_job.name).exists(is_current) } _state = _state.add_pending(CI_Build.task(ci_job)) } } def loop_body(state: Poller.State): Poller.State = if (!state.next.is_finished) state else { state.next.join_result match { case Exn.Exn(exn) => echo_error_message("Could not reach repository: " + exn.getMessage) Poller.State(state.current, poll) case Exn.Res(next) => if (state.current != next) { echo("Found new revisions: " + next) add_tasks(state.current, next) } Poller.State(next, poll) } } } class Timer( ci_jobs: List[Build_CI.Job], store: Store, progress: Progress ) extends Loop_Process[Date]("Timer", store, progress) { override def delay = options.seconds("build_manager_timer_delay") private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tas for (ci_job <- ci_jobs) ci_job.trigger match { 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) case _ => } } def init: Date = Date.now() def loop_body(previous: Date): Date = { val now = Date.now() add_tasks(previous, now) now } } /* web server */ object Web_Server { val Id = new Properties.String(Markup.ID) object Page { val HOME = Path.basic("home") val OVERVIEW = Path.basic("overview") val BUILD = Path.basic("build") val DIFF = Path.basic("diff") } def paths(store: Store): Web_App.Paths = Web_App.Paths(store.address, Path.current, serve_frontend = true, landing = Page.HOME) object API { val BUILD_CANCEL = Path.explode("api/build/cancel") } object Cache { def empty: Cache = new Cache() } class Cache private(keep: Time = Time.minutes(1)) { private var cached: Map[Report, (Time, Report.Data)] = Map.empty def update(): Unit = synchronized { cached = for { (report, (time, _)) <- cached if time + keep > Time.now() } yield report -> (time, report.read) } def lookup(report: Report): Report.Data = synchronized { cached.get(report) match { case Some((_, data)) => cached += report -> (Time.now(), data) case None => cached += report -> (Time.now(), report.read) } cached(report)._2 } } } class Web_Server( port: Int, store: Store, build_hosts: List[Build_Cluster.Host], progress: Progress ) extends Loop_Process[Unit]("Web_Server", store, progress) { import Web_App.* import Web_Server.* val paths = Web_Server.paths(store) val cache = Cache.empty enum Model { case Error extends Model case Cancelled extends Model case Home(state: State) extends Model case Overview(kind: String, state: State) extends Model case Details(build: Build, state: State, public: Boolean = true) extends Model case Diff(build: Build) extends Model } object View { import HTML.* import More_HTML.* def render_if(cond: Boolean, body: XML.Body): XML.Body = if (cond) body else Nil def page_link(path: Path, s: String, props: Properties.T = Nil): XML.Elem = link(paths.frontend_url(path, props).toString, text(s)) + ("target" -> "_parent") def link_build(name: String, id: Long): XML.Elem = page_link(Page.BUILD, "#" + id, Markup.Name(name)) private def render_page(name: String)(body: => XML.Body): XML.Body = More_HTML.header(List(nav(List(page_link(Page.HOME, "home"))))) :: main(chapter(name) :: body ::: Nil) :: Nil private def summary(start: Date): XML.Body = text(" running since " + Build_Log.print_date(start)) private def summary(status: Status, start: Date, end: Option[Date]): XML.Body = text(" (" + status.toString + if_proper(end, " in " + (end.get - start).message_hms) + ") on " + Build_Log.print_date(start)) def render_home(state: State): XML.Body = render_page("Dashboard") { def render_kind(kind: String): XML.Elem = { val running = state.get_running(kind).sortBy(_.id).reverse val finished = state.get_finished(kind).sortBy(_.id).reverse def render_previous(finished: List[Result]): XML.Body = { val (failed, rest) = finished.span(_.status != Status.ok) val first_failed = failed.lastOption.map(result => par( text("first failure: ") ::: link_build(result.name, result.id) :: summary(result.status, result.start_date, result.end_date))) val last_success = rest.headOption.map(result => par( text("last success: ") ::: link_build(result.name, result.id) :: summary(result.status, result.start_date, result.end_date))) first_failed.toList ::: last_success.toList } def render_job(job: Job): XML.Body = par(link_build(job.name, job.id) :: summary(job.start_date)) :: render_if( finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name, render_previous(finished)) def render_result(result: Result): XML.Body = par( link_build(result.name, result.id) :: summary(result.status, result.start_date, result.end_date)) :: render_if(result.status != Status.ok && result.kind != User_Build.name, render_previous(finished.tail)) fieldset( XML.elem("legend", List(page_link(Page.OVERVIEW, kind, Markup.Kind(kind)))) :: (if (running.nonEmpty) render_job(running.head) else if (finished.nonEmpty) render_result(finished.head) else Nil)) } val running = state.running.values.toList val idle = (build_hosts.map(_.hostname).toSet -- running.flatMap(_.hostnames).toSet). def render_rows(hostnames: List[String], body: XML.Body): XML.Body = hostnames match { case Nil => Nil case hostname :: Nil => List(tr(List(td(text(hostname)), td(body)))) case hostname :: hostnames1 => tr(List(td(text(hostname)), td.apply(rowspan(hostnames.length), body))) :: hostnames1.map(hostname => tr(List(td(text(hostname))))) } def render_job(job: Job): XML.Body = render_rows(job.hostnames, page_link(Page.BUILD, job.name, Markup.Name(job.name)) :: summary(job.start_date)) par(text("Queue: " + state.pending.size + " tasks waiting")) :: table(tr(List(th(text("Host")), th(text("Activity")))) :: running.sortBy(_.name).flatMap(render_job) ::: idle.sorted.map(List(_)).flatMap(render_rows(_, text("idle")))) :: section("Builds") :: par(text("Total: " + state.num_builds + " builds")) :: state.kinds.sorted.map(render_kind) } def render_overview(kind: String, state: State): XML.Body = render_page("Overview: " + kind + " job ") { def render_job(job: Job): XML.Body = List(par(link_build(job.name, job.id) :: summary(job.start_date))) def render_result(result: Result): XML.Body = List(par( link_build(result.name, result.id) :: summary(result.status, result.start_date, result.end_date))) itemize( state.get_running(kind).sortBy(_.id).reverse.map(render_job) ::: state.get_finished(kind).sortBy(_.id).reverse.map(render_result)) :: Nil } private val ID = Params.key(Markup.ID) def render_details(build: Build, state: State, public: Boolean): XML.Body = render_page("Build: " + build.name) { def render_cancel(uuid: UUID.T): XML.Body = render_if(!public, List( submit_form("", List(hidden(ID, uuid.toString), api_button(paths.api_route(API.BUILD_CANCEL), "cancel build"))))) def render_rev(components: List[Component], data: Report.Data): XML.Body = { val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1) val s = components.mkString(", ") if (!components.map(_.name).exists(hg_info.toSet)) text("Components: " + s) else text("Components: ") :+ page_link(Page.DIFF, s, Markup.Name(build.name)) } def waiting_for(host: Build_Cluster.Host): XML.Body = build_hosts.find(_.hostname == host.hostname) match { case None => break ::: text(quote(host.hostname) + " is not a build host") case Some(host) => val active = state.running.values.filter(_.hostnames.contains(host.hostname)) if (active.isEmpty) Nil else break ::: text(host.hostname + " is busy with " + active.map(_.name).mkString(" and ")) } def waiting(task: Task): XML.Body = { val num_before = state.pending.values.count(_ > task) if (num_before > 0) text("Waiting for " + num_before + " tasks to complete") else Exn.capture(task.build_hosts) match { case Exn.Res(hosts) => text("Hosts not ready:") ::: hosts.flatMap(waiting_for) case _ => text("Unkown host spec") } } def started(user: Option[String], date: Date): String = "Started" + if_proper(user, " by " + user.get) + " on " + Build_Log.print_date(date) build match { case task: Task => par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) :: par(text("Components: " + task.components.mkString(", "))) :: par(List(bold(waiting(task)))) :: render_cancel(task.uuid) case job: Job => val report_data = cache.lookup(store.report(job.kind, job.id)) par(text(started(job.user, job.start_date))) :: par( if (job.cancelled) text("Cancelling ...") else text("Running ...") ::: render_cancel(job.uuid)) :: par(render_rev(job.components, report_data)) :: par(List(source(report_data.build_log))) :: Nil case result: Result => val report_data = cache.lookup(store.report(result.kind, result.id)) par(text(started(result.user, result.start_date) + if_proper(result.end_date, ", took " + (result.end_date.get - result.start_date).message_hms))) :: par(text("Status: " + result.status)) :: par(render_rev(result.components, report_data)) :: par(List(source(report_data.build_log))) :: Nil } } def render_diff(build: Build): XML.Body = render_page("Diff: " + build.name) { def colored(s: String): XML.Body = { val Colored = "([^\u001b]*)\u001b\\[([0-9;]+)m(.*)\u001b\\[0m([^\u001b]*)".r val colors = List("black", "maroon", "green", "olive", "navy", "purple", "teal", "silver") val lines = split_lines(s).map { case Colored(pre, code, s, post) => val codes = space_explode(';', code.stripSuffix(";1")).map(Value.Int.parse) val fg = codes match { case 0 :: i :: Nil => colors.unapply(i - 30) case _ => None } val sp = span(if (code.endsWith(";1")) List(bold(text(s))) else text(s)) val sp1 = fg.map(color => sp + ("style" -> ("color:" + color))).getOrElse(sp) List(span(text(pre)), sp1, span(text(post))) case line => text(Library.strip_ansi_color(line)) } List(source(Library.separate(nl, lines).flatten)) } 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 = data.component_logs.toMap.get(component.name).toList.flatMap(colored) ::: data.component_diffs.toMap.get(component.name).toList.flatMap(colored) val header = if (infos.isEmpty) component.toString else component.name + ":" par(subsubsection(header) :: infos) }) build match { case job: Job => render_diff(cache.lookup(store.report(job.kind, job.id)), job.components) case result: Result => render_diff(cache.lookup(store.report(result.kind, result.id)), result.components) case _ => Nil } } def render_cancelled: XML.Body = render_page("Build cancelled")(List(page_link(Page.HOME, "Home"))) def parse_uuid(params: Params.Data): Option[UUID.T] = for { id <- params.get(ID) uuid <- UUID.unapply(id) } yield uuid } private val server = new Server[Model](paths, port, progress = progress) { /* control */ def overview: Some[Model.Home] = Some(Model.Home(_state)) def get_overview(props: Properties.T): Option[Model.Overview] = props match { case Markup.Kind(kind) => Some(Model.Overview(kind, _state)) case _ => None } def get_build(props: Properties.T): Option[Model.Details] = props match { case Markup.Name(name) => val state = _state state.get(name).map(Model.Details(_, state)) case Web_Server.Id(UUID(uuid)) => val state = _state state.get(uuid).map(Model.Details(_, state, public = false)) case _ => None } def get_diff(props: Properties.T): Option[Model.Diff] = props match { case Markup.Name(name) => _state.get(name).map(Model.Diff(_)) case _ => None } def cancel_build(params: Params.Data): Option[Model] = for { uuid <- View.parse_uuid(params) model <- synchronized_database("cancel_build") { _state.get(uuid).map { case task: Task => _state = _state.remove_pending(task.name) Model.Cancelled case job: Job => _state = _state.cancel_running(job.name) Model.Cancelled case result: Result => Model.Details(result, _state, public = false) } } } yield model def render(model: Model): XML.Body = HTML.title("Isabelle Build Manager") :: ( model match { case Model.Error => HTML.text("invalid request") case Model.Home(state) => View.render_home(state) case Model.Overview(kind, state) => View.render_overview(kind, state) case Model.Details(build, state, public) => View.render_details(build, state, public) case Model.Diff(build) => View.render_diff(build) case Model.Cancelled => View.render_cancelled }) val error_model: Model = Model.Error val endpoints = List( Get(Page.HOME, "home", _ => overview), Get(Page.OVERVIEW, "overview", get_overview), Get(Page.BUILD, "build", get_build), Get(Page.DIFF, "diff", get_diff), Post(API.BUILD_CANCEL, "cancel build", cancel_build)) val logo = Bytes.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_transparent-48 val head = List( HTML.title("Isabelle Build Manager"), 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 { --color-secondary: var(--color-tertiary); --color-secondary-hover: var(--color-tertiary-hover); } html { background-color: white; }""")) } override def close(): Unit = { server.stop() super.close() } def init: Unit = server.start() def loop_body(u: Unit): Unit = if (!progress.stopped) synchronized_database("iterate") { cache.update() } } /** context **/ case class Context(store: Store, task: Task, id: Long) { def name = Build.name(task.kind, id) def report: Report = store.report(task.kind, id) def task_dir: Path = store.task_dir(task) def isabelle_identifier: String = if (task.build_cluster) store.options.string("build_cluster_identifier") else store. def open_ssh(): SSH.System = { if (task.build_cluster) store.open_cluster_ssh() else Library.the_single(task.build_hosts).open_ssh(store.options) } } /** build process **/ object Build_Process { def open(context: Context): Build_Process = new Build_Process(context.open_ssh(), conte } class Build_Process(ssh: SSH.System, context: Context) { private val task = context.task private val progress = context.report.progress /* resources with cleanup operations */ private val _dir = ssh.tmp_dir() private val _isabelle = try { val rsync_context = Rsync.Context(ssh = ssh) val source = File.standard_path(context.task_dir) Rsync.exec(rsync_context, clean = true, args = List("--", Url.direct_path(source), rsync_context.target(_dir))).check Isabelle_System.rm_tree(context.task_dir) Other_Isabelle(_dir, context.isabelle_identifier, ssh, progress) } catch { case exn: Throwable => close(); throw exn } private val _process = try { val init_components = for { extra_component <- task.build_config.extra_components target = _dir + Sync.DIRS + Path.basic(extra_component.name) if Components.is_component_dir(target) } yield "init_component " + quote(target.absolute.implode) _isabelle.init( other_settings = _isabelle.init_components() ::: init_components ::: task.other_settin fresh = task.build_config.fresh_build, echo = true) val paths = Web_Server.paths(context.store) val job_url = paths.frontend_url(Web_Server.Page.BUILD, Markup.Name(context.name)) val cmd = task.build_config.command(job_url, task.build_hosts) progress.echo("isabelle" + cmd) val script = File.bash_path(Isabelle_Tool.exe(_isabelle.isabelle_home)) + cmd ssh.bash_process(_isabelle.bash_context(script), settings = false) } catch { case exn: Throwable => close(); throw exn } def cancel(): Unit = Option(_process).foreach(_.interrupt()) def terminate(): Unit = Option(_process).foreach(_.terminate()) def close(): Unit = { Option(_dir).foreach(ssh.rm_tree) Isabelle_System.rm_tree(context.task_dir) ssh.close() } /* execution */ def run(): Process_Result = { val process_result = _process.result(progress_stdout = progress.echo(_), progress_stderr = progress.echo(_ close() process_result } } /** build manager store **/ case class Store(options: Options) { val base_dir = Path.explode(options.string("build_manager_dir")) val address = { Url(proper_string(options.string("build_manager_address")) getOrElse "https://" + options.string("build_manager_ssh_host")) } val pending = base_dir + Path.basic("pending") def task_dir(task: Task) = pending + Path.basic(task.uuid.toString) def sync_permissions(dir: Path, ssh: SSH.System = SSH.Local): Unit = { ssh.execute("chmod -R g+rwx " + File.bash_path(dir)) ssh.execute("chown -R :" + unix_group + " " + File.bash_path(dir)) } def init_dirs(): Unit = List(pending, finished).foreach(dir => sync_permissions(Isabelle_System.make_directo val unix_group: String = options.string("build_manager_group") def open_database(server: SSH.Server = SSH.no_server): PostgreSQL.Database = PostgreSQL.open_database_server(options, server = server, user = options.string("build_manager_database_user"), password = options.string("build_manager_database_password"), database = options.string("build_manager_database_name"), host = options.string("build_manager_database_host"), port = options.int("build_manager_database_port"), ssh_host = options.string("build_manager_database_ssh_host"), ssh_port = options.int("build_manager_database_ssh_port"), ssh_user = options.string("build_manager_database_ssh_user")) /* server */ val identifier = options.string("build_manager_identifier") val finished = base_dir + Path.basic("finished") def report(kind: String, id: Long): Report = Report(kind, id, finished + Path.make(List(kind, id.toString))) def open_cluster_ssh(): SSH.Session = SSH.open_session(options, host = options.string("build_manager_cluster_ssh_host"), port = options.int("build_manager_cluster_ssh_port"), user = options.string("build_manager_cluster_ssh_user")) /* client */ def open_ssh(): SSH.Session = SSH.open_session(options, host = options.string("build_manager_ssh_host"), port = options.int("build_manager_ssh_port"), user = options.string("build_manager_ssh_user")) def open_postgresql_server(): SSH.Server = PostgreSQL.open_server(options, host = options.string("build_manager_database_host"), port = options.int("build_manager_database_port"), ssh_host = options.string("build_manager_ssh_host"), ssh_port = options.int("build_manager_ssh_port"), ssh_user = options.string("build_manager_ssh_user")) } /** build manager server **/ /* build manager */ def build_manager( build_hosts: List[Build_Cluster.Host], options: Options, port: Int, sync_dirs: List[Sync.Dir] = Nil, progress: Progress = new Progress ): Unit = { val store = Store(options) val isabelle_repository = Mercurial.self_repository() val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")).map(Build_ progress.echo_if(ci_jobs.nonEmpty, "Managing ci jobs: " + commas_quote(ci_jobs.map( using(store.open_database())(db => Build_Manager.private_data.transaction_lock(db, create = true, label = "Build_Manager.build_manager") { store.init_dirs() }) val processes = List( new Runner(store, build_hosts, isabelle_repository, sync_dirs, progress), new Poller(ci_jobs, store, isabelle_repository, sync_dirs, progress), new Timer(ci_jobs, store, progress), new Web_Server(port, store, build_hosts, progress)) val threads = processes.map(Isabelle_Thread.create(_)) POSIX_Interrupt.handler { progress.stop() processes.foreach(_.interrupt()) } { threads.foreach(_.start()) threads.foreach(_.join()) } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_manager", "run build manager", Scala_Project { args => var afp_root: Option[Path] = None val dirs = new mutable.ListBuffer[Path] val build_hosts = new mutable.ListBuffer[Build_Cluster.Host] var options = Options.init() var port = 0 val getopts = Getopts(""" Usage: isabelle build_manager [OPTIONS] Options are: -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -D DIR include extra component in given directory -H HOSTS host specifications for all available hosts of the form NAMES:PARAMETERS (separated by commas) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p PORT explicit web server port Run Isabelle build manager. """, --> -------------------- --> maximum size reached --> -------------------- ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.43Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28