--- a/src/Pure/System/benchmark.scala Thu Feb 15 12:42:00 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-/* Title: Pure/System/benchmark.scala
- Author: Fabian Huch, TU Muenchen
-
-Host platform benchmarks for performance estimation.
-*/
-
-package isabelle
-
-
-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,
- ssh: SSH.System = SSH.Local,
- isabelle_home: Path = Path.current,
- ): String = {
- val options = Options.Spec.eq("build_hostname", host.name) :: host.options
- ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" +
- Options.Spec.bash_strings(options, bg = true)
- }
-
- def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = {
- val res =
- Build.build(
- options.string.update("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 =>
- using_optional(store.maybe_open_database_server(server = server)) { database_server =>
- 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 full_sessions = Sessions.load_structure(options.int.update("threads", 1))
-
- val build_context =
- Build.Context(store, new Build.Default_Engine,
- Sessions.deps(full_sessions.selection(selection)).check_errors)
-
- 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)
-
- val local_options =
- options
- .bool.update("build_database_server", false)
- .bool.update("build_database", false)
-
- benchmark_requirements(local_options, progress)
- ML_Heap.restore(database_server, heaps, cache = store.cache.compress)
-
- 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)
-
- 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(local_options))
-
- val build =
- Build_Job.start_session(local_build_context, session, progress, No_Logger, server,
- background, session.sources_shasum, input_shasum, node_info, false)
-
- 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.init(hostname = hostname, score = Some(score)))
- }
- }
- }
-
- val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark",
- Scala_Project.here,
- { args =>
- var options = Options.init()
-
- val getopts = Getopts("""
-Usage: isabelle benchmark [OPTIONS]
-
- Options are:
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-
- Run a system benchmark.
-""",
- "o:" -> (arg => options = options + arg))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- val progress = new Console_Progress()
-
- benchmark(options, progress = progress)
- })
-}
\ No newline at end of file