perf: optimize negative time_task

leanprover · Feb 9, 2023 · 84d0252 · 84d0252
1 parent c06c99f
commit 84d0252
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 16 deletions.
diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp
@@ -43,17 +43,22 @@ void finalize_time_task() {
 
 time_task::time_task(std::string const & category, options const & opts, name decl) :
         m_category(category) {
-    if (get_profiler(opts)) {
+    if (!m_category.size()) {
+        // exclude given block from surrounding task, if any
+        if (g_current_time_task) {
+            m_timeit = optional<xtimeit>([](second_duration _) {});
+            m_parent_task = g_current_time_task;
+            g_current_time_task = this;
+        }
+    } else if (get_profiler(opts)) {
         m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable {
-            if (m_category.size()) {
-                sstream ss;
-                ss << m_category;
-                if (decl)
-                    ss << " of " << decl;
-                ss << " took " << display_profiling_time{duration} << "\n";
-                // output atomically, like IO.print
-                tout() << ss.str();
-            }
+            sstream ss;
+            ss << m_category;
+            if (decl)
+                ss << " of " << decl;
+            ss << " took " << display_profiling_time{duration} << "\n";
+            // output atomically, like IO.print
+            tout() << ss.str();
         });
         m_parent_task = g_current_time_task;
         g_current_time_task = this;

diff --git a/src/util/timeit.h b/src/util/timeit.h
@@ -22,19 +22,19 @@ std::ostream & operator<<(std::ostream & out, display_profiling_time const & tim
 /** \brief Low tech timer. */
 class timeit {
     second_duration m_threshold;
-    std::chrono::steady_clock::time_point m_start;
+    std::chrono::system_clock::time_point m_start;
     std::ostream & m_out;
     std::string    m_msg;
 public:
     timeit(std::ostream & out, char const * msg, second_duration threshold):
         m_threshold(threshold), m_out(out), m_msg(msg) {
-        m_start = std::chrono::steady_clock::now();
+        m_start = std::chrono::system_clock::now();
     }
     timeit(std::ostream & out, char const * msg, double threshold):
         timeit(out, msg, second_duration(threshold)) {}
     timeit(std::ostream & out, char const * msg) : timeit(out, msg, second_duration(0)) {}
     ~timeit() {
-        auto end = std::chrono::steady_clock::now();
+        auto end = std::chrono::system_clock::now();
         auto diff = second_duration(end - m_start);
         if (diff >= m_threshold) {
             m_out << m_msg << " " << display_profiling_time{diff} << "\n";
@@ -46,12 +46,12 @@ class timeit {
 class xtimeit {
     second_duration m_threshold;
     second_duration m_excluded {0};
-    std::chrono::steady_clock::time_point m_start;
+    std::chrono::system_clock::time_point m_start;
     std::function<void(second_duration)> m_fn; // NOLINT
 public:
     xtimeit(second_duration threshold, std::function<void(second_duration)> const & fn): // NOLINT
         m_threshold(threshold), m_fn(fn) {
-        m_start = std::chrono::steady_clock::now();
+        m_start = std::chrono::system_clock::now();
     }
     xtimeit(std::function<void(second_duration)> const & fn) : xtimeit(second_duration(0), fn) {} // NOLINT
     xtimeit(xtimeit const &) = delete;
@@ -64,7 +64,7 @@ class xtimeit {
     }
 
     second_duration get_elapsed_inclusive() const {
-        auto end = std::chrono::steady_clock::now();
+        auto end = std::chrono::system_clock::now();
         return second_duration(end - m_start);
     }