# HG changeset patch # User Fabian Huch # Date 1719474076 -7200 # Node ID 4b10ae56ed01c73fb23a299eb301e8584d7bd539 # Parent 7dcc5df65affc9f56a37f31184bfb481606b22e5 add Isabelle settings to managed tasks and ci jobs; diff -r 7dcc5df65aff -r 4b10ae56ed01 src/Pure/Build/build_ci.scala --- a/src/Pure/Build/build_ci.scala Wed Jun 26 19:55:56 2024 +0200 +++ b/src/Pure/Build/build_ci.scala Thu Jun 27 09:41:16 2024 +0200 @@ -112,6 +112,7 @@ build_prefs: List[Options.Spec] = Nil, hook: Hook = none, extra_components: List[String] = Nil, + other_settings: List[String] = Nil, trigger: Trigger = On_Commit ) { override def toString: String = name diff -r 7dcc5df65aff -r 4b10ae56ed01 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Wed Jun 26 19:55:56 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jun 27 09:41:16 2024 +0200 @@ -106,6 +106,7 @@ sealed case class Task( build_config: Build_Config, hosts_spec: String, + other_settings: List[String] = Nil, uuid: UUID.T = UUID.random(), submit_date: Date = Date.now(), priority: Priority = Priority.normal, @@ -318,6 +319,7 @@ val kind = SQL.Column.string("kind") val build_cluster = SQL.Column.bool("build_cluster") val hosts_spec = SQL.Column.string("hosts_spec") + 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") @@ -340,10 +342,10 @@ val verbose = SQL.Column.bool("verbose") val table = - make_table(List(kind, build_cluster, hosts_spec, uuid, submit_date, priority, isabelle_rev, - components, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, - fresh_build, presentation, verbose), + make_table(List(kind, build_cluster, hosts_spec, other_settings, uuid, submit_date, + priority, isabelle_rev, components, 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") } @@ -353,6 +355,7 @@ val kind = res.string(Pending.kind) val build_cluster = res.bool(Pending.build_cluster) val hosts_spec = res.string(Pending.hosts_spec) + 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)) @@ -384,8 +387,8 @@ clean_build, export_files, fresh_build, presentation, verbose) } - val task = - Task(build_config, hosts_spec, UUID.make(uuid), submit_date, priority, isabelle_rev) + val task = Task(build_config, hosts_spec, other_settings, UUID.make(uuid), submit_date, + priority, isabelle_rev) task.name -> task }) @@ -408,11 +411,12 @@ stmt.string(1) = task.kind stmt.bool(2) = task.build_cluster stmt.string(3) = task.hosts_spec - stmt.string(4) = task.uuid.toString - stmt.date(5) = task.submit_date - stmt.string(6) = task.priority.toString - stmt.string(7) = task.isabelle_rev - stmt.string(8) = task.components.mkString(",") + stmt.string(4) = cat_lines(task.other_settings) + stmt.string(5) = task.uuid.toString + stmt.date(6) = task.submit_date + stmt.string(7) = task.priority.toString + stmt.string(8) = task.isabelle_rev + stmt.string(9) = task.components.mkString(",") def get[A](f: User_Build => A): Option[A] = task.build_config match { @@ -420,20 +424,20 @@ case _ => None } - stmt.string(9) = get(user_build => user_build.prefs.map(_.print).mkString(",")) - stmt.bool(10) = get(_.requirements) - stmt.bool(11) = get(_.all_sessions) - stmt.string(12) = get(_.base_sessions.mkString(",")) - stmt.string(13) = get(_.exclude_session_groups.mkString(",")) - stmt.string(14) = get(_.exclude_sessions.mkString(",")) - stmt.string(15) = get(_.session_groups.mkString(",")) - stmt.string(16) = get(_.sessions.mkString(",")) - stmt.bool(17) = get(_.build_heap) - stmt.bool(18) = get(_.clean_build) - stmt.bool(19) = get(_.export_files) - stmt.bool(20) = get(_.fresh_build) - stmt.bool(21) = get(_.presentation) - stmt.bool(22) = get(_.verbose) + stmt.string(10) = get(user_build => user_build.prefs.map(_.print).mkString(",")) + stmt.bool(11) = get(_.requirements) + stmt.bool(12) = get(_.all_sessions) + stmt.string(13) = get(_.base_sessions.mkString(",")) + stmt.string(14) = get(_.exclude_session_groups.mkString(",")) + stmt.string(15) = get(_.exclude_sessions.mkString(",")) + stmt.string(16) = get(_.session_groups.mkString(",")) + stmt.string(17) = get(_.sessions.mkString(",")) + stmt.bool(18) = get(_.build_heap) + stmt.bool(19) = get(_.clean_build) + stmt.bool(20) = get(_.export_files) + stmt.bool(21) = get(_.fresh_build) + stmt.bool(22) = get(_.presentation) + stmt.bool(23) = get(_.verbose) }) } @@ -885,8 +889,8 @@ if isabelle_updated || ci_job.components.exists(updated_components.contains) if !_state.pending.values.exists(_.kind == ci_job.name) } { - val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, priority = Priority.low, - isabelle_rev = "default") + val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, ci_job.other_settings, + priority = Priority.low, isabelle_rev = "default") _state = _state.add_pending(task) } } @@ -1257,7 +1261,7 @@ } yield "init_component " + quote(target.absolute.implode) _isabelle.init( - other_settings = _isabelle.init_components() ::: init_components, + other_settings = _isabelle.init_components() ::: init_components ::: task.other_settings, fresh = task.build_config.fresh_build, echo = true) val paths = Web_Server.paths(context.store) @@ -1530,7 +1534,7 @@ val build_config = User_Build(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, uuid, Date.now(), Priority.high) + val task = Task(build_config, hosts_spec, uuid = uuid, priority = Priority.high) val dir = store.task_dir(task)