# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702633685 -3600
# Node ID e9a788a757757ddc8198ebb71f7994d1d7001af8
# Parent  9deadc9d8872cd73d1e09262bbdd4f2f742c6ce8
use single-threaded session build as benchmark (using ZF-Constructible);

diff -r 9deadc9d8872 -r e9a788a75775 src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Thu Dec 14 13:14:25 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Fri Dec 15 10:48:05 2023 +0100
@@ -8,6 +8,9 @@
 
 
 object Benchmark {
+  /* ZF-Constructible as representative benchmark session with short build time and requirements */
+
+  val benchmark_session = "ZF-Constructible"
 
   def benchmark_command(
     host: Build_Cluster.Host,
@@ -19,28 +22,79 @@
       Options.Spec.bash_strings(options, bg = true)
   }
 
+  def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = {
+    val res =
+      Build.build(
+        options.string("build_engine") = Build.Default_Engine().name,
+        selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)),
+        progress = progress, build_heap = true)
+    if (!res.ok) error("Failed building requirements")
+  }
+
   def benchmark(options: Options, progress: Progress = new Progress()): Unit = {
     val hostname = options.string("build_hostname")
     val store = Store(options)
 
     using(store.open_server()) { server =>
-      val db = store.open_build_database(path = Host.private_data.database, server = server)
+      using_optional(store.maybe_open_database_server(server = server)) { database_server =>
+        val db = store.open_build_database(path = Host.private_data.database, server = server)
+
+        benchmark_requirements(options, progress)
+
+        progress.echo("Starting benchmark...")
+        val selection = Sessions.Selection(sessions = List(benchmark_session))
+        val full_sessions = Sessions.load_structure(options.int("threads") = 1)
+
+        val build_context =
+          Build.Context(store, new Build.Default_Engine,
+            Sessions.deps(full_sessions.selection(selection)).check_errors)
 
-      progress.echo("Starting benchmark...")
-      val start = Time.now()
+        val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
+        val session = sessions(benchmark_session)
+
+        val heaps = session.ancestors.map(store.output_heap)
+        ML_Heap.restore(database_server, heaps, cache = store.cache.compress)
 
-      // TODO proper benchmark
-      def fib(n: Long): Long = if (n < 2) 1 else fib(n - 2) + fib(n - 1)
-      val result = fib(42)
+        def get_shasum(session_name: String): SHA1.Shasum = {
+          val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
+
+          val input_shasum =
+            if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum()
+            else SHA1.flat_shasum(ancestor_shasums)
 
-      val stop = Time.now()
-      val timing = stop - start
+          store.check_output(
+            database_server, session_name,
+            session_options = build_context.sessions_structure(session_name).options,
+            sources_shasum = sessions(session_name).sources_shasum,
+            input_shasum = input_shasum,
+            fresh_build = false,
+            store_heap = false)._2
+        }
+
+        val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
+        val background = deps.background(benchmark_session)
+        val input_shasum = get_shasum(benchmark_session)
+        val node_info = Host.Node_Info(hostname, None, Nil)
+
+        val local_build_context =
+          build_context.copy(store = Store(options.bool("build_database_server") = false))
 
-      val score = Time.seconds(100).ms.toDouble / (1 + timing.ms)
-      progress.echo(
-        "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
+        val build =
+          Build_Job.start_session(local_build_context, session, progress, No_Logger, server,
+            background, session.sources_shasum, input_shasum, node_info, false)
 
-      Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+        val timing =
+          build.join match {
+            case Some(result) if result.process_result.ok => result.process_result.timing
+            case _ => error("Failed to build benchmark session")
+          }
+
+        val score = Time.seconds(1000).ms.toDouble / (1 + timing.elapsed.ms)
+        progress.echo(
+          "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score))
+
+        Host.write_info(db, Host.Info.gather(hostname, score = Some(score)))
+      }
     }
   }