author | wenzelm |
Thu, 15 Feb 2024 12:18:25 +0100 | |
changeset 79617 | cdb51c7225ad |
parent 79602 | 9ba800f12785 |
child 79618 | 50376abd132d |
permissions | -rw-r--r-- |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
1 |
/* Title: Pure/System/benchmark.scala |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Fabian Huch, TU Muenchen |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
3 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
4 |
Host platform benchmarks for performance estimation. |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
5 |
*/ |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
6 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
7 |
package isabelle |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
8 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
9 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
10 |
object Benchmark { |
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
11 |
/* ZF-Constructible as representative benchmark session with short build time and requirements */ |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
12 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
13 |
val benchmark_session = "ZF-Constructible" |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
14 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
15 |
def benchmark_command( |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
16 |
host: Build_Cluster.Host, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
17 |
ssh: SSH.System = SSH.Local, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
18 |
isabelle_home: Path = Path.current, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
19 |
): String = { |
78916 | 20 |
val options = Options.Spec.eq("build_hostname", host.name) :: host.options |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
21 |
ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" + |
78915
90756ad4d8d7
more accurate treatment of surrounding whitespace;
wenzelm
parents:
78908
diff
changeset
|
22 |
Options.Spec.bash_strings(options, bg = true) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
23 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
24 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
25 |
def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = { |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
26 |
val res = |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
27 |
Build.build( |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
28 |
options.string("build_engine") = Build.Default_Engine().name, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
29 |
selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)), |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
30 |
progress = progress, build_heap = true) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
31 |
if (!res.ok) error("Failed building requirements") |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
32 |
} |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
33 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
34 |
def benchmark(options: Options, progress: Progress = new Progress()): Unit = { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
35 |
val hostname = options.string("build_hostname") |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
36 |
val store = Store(options) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
37 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
38 |
using(store.open_server()) { server => |
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
39 |
using_optional(store.maybe_open_database_server(server = server)) { database_server => |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
40 |
val db = store.open_build_database(path = Host.private_data.database, server = server) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
41 |
|
79617 | 42 |
progress.echo("Starting benchmark ...") |
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
43 |
val selection = Sessions.Selection(sessions = List(benchmark_session)) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
44 |
val full_sessions = Sessions.load_structure(options.int("threads") = 1) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
45 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
46 |
val build_context = |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
47 |
Build.Context(store, new Build.Default_Engine, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
48 |
Sessions.deps(full_sessions.selection(selection)).check_errors) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
49 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
50 |
val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
51 |
val session = sessions(benchmark_session) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
52 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
53 |
val heaps = session.ancestors.map(store.output_heap) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
54 |
ML_Heap.restore(database_server, heaps, cache = store.cache.compress) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
55 |
|
79295
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
56 |
val local_options = |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
57 |
options |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
58 |
.bool.update("build_database_server", false) |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
59 |
.bool.update("build_database", false) |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
60 |
|
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
61 |
benchmark_requirements(local_options, progress) |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
62 |
ML_Heap.restore(database_server, heaps, cache = store.cache.compress) |
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
63 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
64 |
def get_shasum(session_name: String): SHA1.Shasum = { |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
65 |
val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
66 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
67 |
val input_shasum = |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
68 |
if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum() |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
69 |
else SHA1.flat_shasum(ancestor_shasums) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
70 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
71 |
store.check_output( |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
72 |
database_server, session_name, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
73 |
session_options = build_context.sessions_structure(session_name).options, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
74 |
sources_shasum = sessions(session_name).sources_shasum, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
75 |
input_shasum = input_shasum, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
76 |
fresh_build = false, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
77 |
store_heap = false)._2 |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
78 |
} |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
79 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
80 |
val deps = Sessions.deps(full_sessions.selection(selection)).check_errors |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
81 |
val background = deps.background(benchmark_session) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
82 |
val input_shasum = get_shasum(benchmark_session) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
83 |
val node_info = Host.Node_Info(hostname, None, Nil) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
84 |
|
79295
123651f3ec5d
restore benchmark requirement heaps properly;
Fabian Huch <huch@in.tum.de>
parents:
79291
diff
changeset
|
85 |
val local_build_context = build_context.copy(store = Store(local_options)) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
86 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
87 |
val build = |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
88 |
Build_Job.start_session(local_build_context, session, progress, No_Logger, server, |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
89 |
background, session.sources_shasum, input_shasum, node_info, false) |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
90 |
|
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
91 |
val timing = |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
92 |
build.join match { |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
93 |
case Some(result) if result.process_result.ok => result.process_result.timing |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
94 |
case _ => error("Failed to build benchmark session") |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
95 |
} |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
96 |
|
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
97 |
val score = Time.seconds(1000).ms.toDouble / (1 + timing.elapsed.ms) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
98 |
progress.echo( |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
99 |
"Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score)) |
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
100 |
|
79602 | 101 |
Host.write_info(db, Host.Info.init(hostname = hostname, score = Some(score))) |
79291
e9a788a75775
use single-threaded session build as benchmark (using ZF-Constructible);
Fabian Huch <huch@in.tum.de>
parents:
78916
diff
changeset
|
102 |
} |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
103 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
104 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
105 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
106 |
val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark", |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
107 |
Scala_Project.here, |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
108 |
{ args => |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
109 |
var options = Options.init() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
110 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
111 |
val getopts = Getopts(""" |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
112 |
Usage: isabelle benchmark [OPTIONS] |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
113 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
114 |
Options are: |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
115 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
116 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
117 |
Run a system benchmark. |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
118 |
""", |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
119 |
"o:" -> (arg => options = options + arg)) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
120 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
121 |
val more_args = getopts(args) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
122 |
if (more_args.nonEmpty) getopts.usage() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
123 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
124 |
val progress = new Console_Progress() |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
125 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
126 |
benchmark(options, progress = progress) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
127 |
}) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
diff
changeset
|
128 |
} |