forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
profiling.cpp
46 lines (36 loc) · 1.43 KB
/
profiling.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
/*
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Gabriel Ebner
*/
#include "library/profiling.h"
#include "util/option_declarations.h"
#ifndef LEAN_DEFAULT_PROFILER
#define LEAN_DEFAULT_PROFILER false
#endif
#ifndef LEAN_DEFAULT_PROFILER_THRESHOLD
#define LEAN_DEFAULT_PROFILER_THRESHOLD 100
#endif
namespace lean {
static name * g_profiler = nullptr;
static name * g_profiler_threshold = nullptr;
bool get_profiler(options const & opts) {
return opts.get_bool(*g_profiler, LEAN_DEFAULT_PROFILER);
}
prof_clock::duration get_profiling_threshold(options const & opts) {
return prof_clock::duration(std::chrono::milliseconds(opts.get_unsigned(*g_profiler_threshold, LEAN_DEFAULT_PROFILER_THRESHOLD)));
}
void initialize_profiling() {
g_profiler = new name{"profiler"};
mark_persistent(g_profiler->raw());
g_profiler_threshold = new name{"profiler", "threshold"};
mark_persistent(g_profiler_threshold->raw());
register_bool_option(*g_profiler, LEAN_DEFAULT_PROFILER, "(profiler) profile tactics and vm_eval command");
register_unsigned_option(*g_profiler_threshold, LEAN_DEFAULT_PROFILER_THRESHOLD,
"(profiler) threshold in milliseconds, profiling times under threshold will not be reported");
}
void finalize_profiling() {
delete g_profiler;
delete g_profiler_threshold;
}
}