# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1711035355 -3600
# Node ID 8fe1ed4b5705f36aebd8edcde2b7ee7689fda2b5
# Parent  5eb90c1ce653cdf1c47b9b93383dafe8ae6f6108
option for benchmark session;

diff -r 5eb90c1ce653 -r 8fe1ed4b5705 etc/options
--- a/etc/options	Thu Mar 21 13:05:49 2024 +0100
+++ b/etc/options	Thu Mar 21 16:35:55 2024 +0100
@@ -219,6 +219,9 @@
 option build_cluster_identifier : string = "build_cluster"
   -- "ISABELLE_IDENTIFIER for remote build cluster sessions"
 
+option build_benchmark_session : string = "FOLP-ex"
+  -- "representative benchmark session with short build time and requirements"
+
 option build_schedule : string = ""
   -- "path to pre-computed schedule"
 
diff -r 5eb90c1ce653 -r 8fe1ed4b5705 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Thu Mar 21 13:05:49 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Thu Mar 21 16:35:55 2024 +0100
@@ -13,26 +13,28 @@
 object Build_Benchmark {
   /* benchmark */
 
-  // representative benchmark session with short build time and requirements
-  val benchmark_session = "FOLP-ex"
+  def benchmark_session(options: Options) = options.string("build_benchmark_session")
 
   def benchmark_command(
+    options: Options,
     host: Build_Cluster.Host,
     ssh: SSH.System = SSH.Local,
     isabelle_home: Path = Path.current,
   ): String = {
     val benchmark_options =
-      List(Options.Spec.eq("build_hostname", host.name), Options.Spec("build_database_server"))
+      List(
+        Options.Spec.eq("build_hostname", host.name),
+        Options.Spec("build_database_server"),
+        options.spec("build_benchmark_session"))
     ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_benchmark" +
       Options.Spec.bash_strings(benchmark_options ::: host.options, bg = true)
   }
 
   def benchmark_requirements(options: Options, progress: Progress = new Progress): Unit = {
-    val res =
-      Build.build(
-        options.string.update("build_engine", Build.Engine.Default.name),
-        selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)),
-        progress = progress, build_heap = true)
+    val options1 = options.string.update("build_engine", Build.Engine.Default.name)
+    val selection =
+      Sessions.Selection(requirements = true, sessions = List(benchmark_session(options)))
+    val res = Build.build(options1, selection = selection, progress = progress, build_heap = true)
     if (!res.ok) error("Failed building requirements")
   }
 
@@ -45,14 +47,15 @@
         val db = store.open_build_database(path = Host.private_data.database, server = server)
 
         progress.echo("Starting benchmark ...")
-        val selection = Sessions.Selection(sessions = List(benchmark_session))
+        val benchmark_session_name = benchmark_session(options)
+        val selection = Sessions.Selection(sessions = List(benchmark_session_name))
         val full_sessions = Sessions.load_structure(options + "threads=1")
 
         val build_deps = Sessions.deps(full_sessions.selection(selection)).check_errors
         val build_context = Build.Context(store, build_deps, jobs = 1)
 
         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
-        val session = sessions(benchmark_session)
+        val session = sessions(benchmark_session_name)
 
         val hierachy = session.ancestors.map(store.output_session(_, store_heap = true))
         for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
@@ -79,8 +82,8 @@
         }
 
         val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
-        val background = deps.background(benchmark_session)
-        val input_shasum = get_shasum(benchmark_session)
+        val background = deps.background(benchmark_session_name)
+        val input_shasum = get_shasum(benchmark_session_name)
         val node_info = Host.Node_Info(hostname, None, Nil)
 
         val local_build_context = build_context.copy(store = Store(local_options))
diff -r 5eb90c1ce653 -r 8fe1ed4b5705 src/Pure/Build/build_cluster.scala
--- a/src/Pure/Build/build_cluster.scala	Thu Mar 21 13:05:49 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala	Thu Mar 21 16:35:55 2024 +0100
@@ -196,7 +196,8 @@
 
     def benchmark(): Unit = {
       val script =
-        Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = built_cluster_isabelle_home)
+        Build_Benchmark.benchmark_command(options, host, ssh = ssh,
+          isabelle_home = built_cluster_isabelle_home)
       build_cluster_isabelle.bash(script).check
     }