add Isabelle settings to managed tasks and ci jobs;
authorFabian Huch <huch@in.tum.de>
Thu, 27 Jun 2024 09:41:16 +0200
changeset 80414 4b10ae56ed01
parent 80413 7dcc5df65aff
child 80415 89c20f7f3b3b
add Isabelle settings to managed tasks and ci jobs;
src/Pure/Build/build_ci.scala
src/Pure/Build/build_manager.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
--- 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)