17 val options = Options.Spec.eq("build_hostname", host.name) :: host.options |
20 val options = Options.Spec.eq("build_hostname", host.name) :: host.options |
18 ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" + |
21 ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " benchmark" + |
19 Options.Spec.bash_strings(options, bg = true) |
22 Options.Spec.bash_strings(options, bg = true) |
20 } |
23 } |
21 |
24 |
|
25 def benchmark_requirements(options: Options, progress: Progress = new Progress()): Unit = { |
|
26 val res = |
|
27 Build.build( |
|
28 options.string("build_engine") = Build.Default_Engine().name, |
|
29 selection = Sessions.Selection(requirements = true, sessions = List(benchmark_session)), |
|
30 progress = progress, build_heap = true) |
|
31 if (!res.ok) error("Failed building requirements") |
|
32 } |
|
33 |
22 def benchmark(options: Options, progress: Progress = new Progress()): Unit = { |
34 def benchmark(options: Options, progress: Progress = new Progress()): Unit = { |
23 val hostname = options.string("build_hostname") |
35 val hostname = options.string("build_hostname") |
24 val store = Store(options) |
36 val store = Store(options) |
25 |
37 |
26 using(store.open_server()) { server => |
38 using(store.open_server()) { server => |
27 val db = store.open_build_database(path = Host.private_data.database, server = server) |
39 using_optional(store.maybe_open_database_server(server = server)) { database_server => |
|
40 val db = store.open_build_database(path = Host.private_data.database, server = server) |
28 |
41 |
29 progress.echo("Starting benchmark...") |
42 benchmark_requirements(options, progress) |
30 val start = Time.now() |
|
31 |
43 |
32 // TODO proper benchmark |
44 progress.echo("Starting benchmark...") |
33 def fib(n: Long): Long = if (n < 2) 1 else fib(n - 2) + fib(n - 1) |
45 val selection = Sessions.Selection(sessions = List(benchmark_session)) |
34 val result = fib(42) |
46 val full_sessions = Sessions.load_structure(options.int("threads") = 1) |
35 |
47 |
36 val stop = Time.now() |
48 val build_context = |
37 val timing = stop - start |
49 Build.Context(store, new Build.Default_Engine, |
|
50 Sessions.deps(full_sessions.selection(selection)).check_errors) |
38 |
51 |
39 val score = Time.seconds(100).ms.toDouble / (1 + timing.ms) |
52 val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress) |
40 progress.echo( |
53 val session = sessions(benchmark_session) |
41 "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score)) |
|
42 |
54 |
43 Host.write_info(db, Host.Info.gather(hostname, score = Some(score))) |
55 val heaps = session.ancestors.map(store.output_heap) |
|
56 ML_Heap.restore(database_server, heaps, cache = store.cache.compress) |
|
57 |
|
58 def get_shasum(session_name: String): SHA1.Shasum = { |
|
59 val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum) |
|
60 |
|
61 val input_shasum = |
|
62 if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum() |
|
63 else SHA1.flat_shasum(ancestor_shasums) |
|
64 |
|
65 store.check_output( |
|
66 database_server, session_name, |
|
67 session_options = build_context.sessions_structure(session_name).options, |
|
68 sources_shasum = sessions(session_name).sources_shasum, |
|
69 input_shasum = input_shasum, |
|
70 fresh_build = false, |
|
71 store_heap = false)._2 |
|
72 } |
|
73 |
|
74 val deps = Sessions.deps(full_sessions.selection(selection)).check_errors |
|
75 val background = deps.background(benchmark_session) |
|
76 val input_shasum = get_shasum(benchmark_session) |
|
77 val node_info = Host.Node_Info(hostname, None, Nil) |
|
78 |
|
79 val local_build_context = |
|
80 build_context.copy(store = Store(options.bool("build_database_server") = false)) |
|
81 |
|
82 val build = |
|
83 Build_Job.start_session(local_build_context, session, progress, No_Logger, server, |
|
84 background, session.sources_shasum, input_shasum, node_info, false) |
|
85 |
|
86 val timing = |
|
87 build.join match { |
|
88 case Some(result) if result.process_result.ok => result.process_result.timing |
|
89 case _ => error("Failed to build benchmark session") |
|
90 } |
|
91 |
|
92 val score = Time.seconds(1000).ms.toDouble / (1 + timing.elapsed.ms) |
|
93 progress.echo( |
|
94 "Finished benchmark in " + timing.message + ". Score: " + String.format("%.2f", score)) |
|
95 |
|
96 Host.write_info(db, Host.Info.gather(hostname, score = Some(score))) |
|
97 } |
44 } |
98 } |
45 } |
99 } |
46 |
100 |
47 val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark", |
101 val isabelle_tool = Isabelle_Tool("benchmark", "run system benchmark", |
48 Scala_Project.here, |
102 Scala_Project.here, |