--- a/etc/build.props Thu Feb 15 12:42:00 2024 +0100
+++ b/etc/build.props Thu Feb 15 12:48:25 2024 +0100
@@ -51,6 +51,7 @@
src/Pure/Admin/isabelle_cronjob.scala \
src/Pure/Build/browser_info.scala \
src/Pure/Build/build.scala \
+ src/Pure/Build/build_benchmark.scala \
src/Pure/Build/build_cluster.scala \
src/Pure/Build/build_job.scala \
src/Pure/Build/build_process.scala \
@@ -168,7 +169,6 @@
src/Pure/PIDE/yxml.scala \
src/Pure/ROOT.scala \
src/Pure/System/bash.scala \
- src/Pure/System/benchmark.scala \
src/Pure/System/classpath.scala \
src/Pure/System/command_line.scala \
src/Pure/System/components.scala \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Build/build_benchmark.scala Thu Feb 15 12:48:25 2024 +0100
@@ -0,0 +1,128 @@
+/* Title: Pure/System/build_benchmark.scala
+ Author: Fabian Huch, TU Muenchen
+
+Host platform benchmarks for performance estimation.
+*/
+
+package isabelle
+
+
+object Build_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")) + " build_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("build_benchmark", "run benchmark for build process",
+ Scala_Project.here,
+ { args =>
+ var options = Options.init()
+
+ val getopts = Getopts("""
+Usage: isabelle build_benchmark [OPTIONS]
+
+ Options are:
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+
+ Run benchmark for build process.
+""",
+ "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
--- a/src/Pure/Build/build_cluster.scala Thu Feb 15 12:42:00 2024 +0100
+++ b/src/Pure/Build/build_cluster.scala Thu Feb 15 12:48:25 2024 +0100
@@ -185,7 +185,7 @@
def benchmark(): Unit = {
val script =
- Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home)
+ Build_Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home)
remote_isabelle.bash(script).check
}
--- a/src/Pure/Build/build_schedule.scala Thu Feb 15 12:42:00 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Feb 15 12:48:25 2024 +0100
@@ -1035,11 +1035,11 @@
}
override def run(): Build.Results = {
- Benchmark.benchmark_requirements(build_options)
+ Build_Benchmark.benchmark_requirements(build_options)
if (build_context.jobs > 0) {
val benchmark_options = build_options.string.update("build_hostname", hostname)
- Benchmark.benchmark(benchmark_options, progress)
+ Build_Benchmark.benchmark(benchmark_options, progress)
}
_build_cluster.benchmark()
--- 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
--- a/src/Pure/System/isabelle_tool.scala Thu Feb 15 12:42:00 2024 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Feb 15 12:48:25 2024 +0100
@@ -120,11 +120,11 @@
class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
class Tools extends Isabelle_Scala_Tools(
- Benchmark.isabelle_tool,
Build.isabelle_tool1,
Build.isabelle_tool2,
Build.isabelle_tool3,
Build.isabelle_tool4,
+ Build_Benchmark.isabelle_tool,
Build_Schedule.isabelle_tool,
CI_Build.isabelle_tool,
Doc.isabelle_tool,