From c9bebb7411b58feff60793309e8fc808a198610b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 31 Oct 2018 09:19:27 +0100
Subject: [PATCH] feat(library/time_task): do not report inclusive times

---
 src/library/time_task.cpp | 28 ++++++++++++++++++++++++++++
 src/library/time_task.h   | 21 +++------------------
 2 files changed, 31 insertions(+), 18 deletions(-)

diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp
index 09c76a777c..5745e17802 100644
--- a/src/library/time_task.cpp
+++ b/src/library/time_task.cpp
@@ -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);
+    }
+}
 }
diff --git a/src/library/time_task.h b/src/library/time_task.h
index 2643f7bf55..a43d62c98d 100644
--- a/src/library/time_task.h
+++ b/src/library/time_task.h
@@ -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();