# HG changeset patch # User wenzelm # Date 1707997705 -3600 # Node ID 3914bca631b93f603e6fd91ff4a3dac765c09a6f # Parent 50ec6a68d36fdb8ea31d50c1b4d8710d680022e3 clarified directories; clarified names; diff -r 50ec6a68d36f -r 3914bca631b9 etc/build.props --- 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 \ diff -r 50ec6a68d36f -r 3914bca631b9 src/Pure/Build/build_benchmark.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 diff -r 50ec6a68d36f -r 3914bca631b9 src/Pure/Build/build_cluster.scala --- 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 } diff -r 50ec6a68d36f -r 3914bca631b9 src/Pure/Build/build_schedule.scala --- 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() diff -r 50ec6a68d36f -r 3914bca631b9 src/Pure/System/benchmark.scala --- 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 diff -r 50ec6a68d36f -r 3914bca631b9 src/Pure/System/isabelle_tool.scala --- 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,