# HG changeset patch # User Fabian Huch # 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 }