max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/time_task): do not report inclusive times

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-31 09:19:27 +01:00
parent 8c27f0aac6
commit c9bebb7411
2 changed files with 31 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/library/time_task.cpp
View file

@ -12,6 +12,7 @@ namespace lean {
static std::map<std::string, second_duration> * g_cum_times;
static mutex * g_cum_times_mutex;
LEAN_THREAD_PTR(time_task, g_current_time_task);
void report_profiling_time(std::string const & category, second_duration time) {
lock_guard<mutex> _(*g_cum_times_mutex);
@ -35,4 +36,31 @@ void finalize_time_task() {
delete g_cum_times;
delete g_cum_times_mutex;
}
time_task::time_task(std::string const & category, message_builder builder, name decl) :
m_category(category) {
auto const & opts = builder.get_text_stream().get_options();
if (get_profiler(opts)) {
m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable {
builder.get_text_stream().get_stream() << m_category;
if (decl)
builder.get_text_stream().get_stream() << " of " << decl;
builder.get_text_stream().get_stream() << " took " << display_profiling_time{duration} << "\n";
builder.report();
});
m_parent_task = g_current_time_task;
g_current_time_task = this;
}
}
time_task::~time_task() {
if (m_timeit) {
g_current_time_task = m_parent_task;
auto time = m_timeit->get_elapsed();
report_profiling_time(m_category, time);
if (m_parent_task)
// do not report inclusive times
report_profiling_time(m_parent_task->m_category, -time);
}
}
}

21
src/library/time_task.h
View file

@ -18,25 +18,10 @@ void display_cumulative_profiling_times(std::ostream & out);
class time_task {
std::string m_category;
optional<xtimeit> m_timeit;
time_task * m_parent_task;
public:
time_task(std::string const & category, message_builder builder, name decl = name()) :
m_category(category) {
auto const & opts = builder.get_text_stream().get_options();
if (get_profiler(opts)) {
m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable {
builder.get_text_stream().get_stream() << m_category;
if (decl)
builder.get_text_stream().get_stream() << " of " << decl;
builder.get_text_stream().get_stream() << " took " << display_profiling_time{duration} << "\n";
builder.report();
});
}
}
~time_task() {
if (m_timeit)
report_profiling_time(m_category, m_timeit->get_elapsed());
}
time_task(std::string const & category, message_builder builder, name decl = name());
~time_task();
};
void initialize_time_task();