Profiler fixes

src/library/compiler/ir_interpreter.cpp

@@ -375,11 +375,11 @@ class interpreter {
 public:
     template<class T>
     static inline T with_interpreter(environment const & env, options const & opts, name const & fn, std::function<T(interpreter &)> const & f) {
+        time_task t("interpretation", opts, fn);
         if (g_interpreter && is_eqp(g_interpreter->m_env, env) && is_eqp(g_interpreter->m_opts, opts)) {
             return f(*g_interpreter);
         } else {
             // We changed threads or the closure was stored and called in a different context.
-            time_task t("interpretation", opts, fn);
             scope_trace_env scope_trace(env, opts);
             // the caches contain data from the Environment, so we cannot reuse them when changing it
             interpreter interp(env, opts);
@@ -514,6 +514,7 @@ class interpreter {
                 for (size_t i = 0; i < expr_ap_args(e).size(); i++) {
                     args[i] = eval_arg(expr_ap_args(e)[i]).m_obj;
                 }
+                time_task tt("", m_opts);
                 object * r = apply_n(var(expr_ap_fun(e)).m_obj, expr_ap_args(e).size(), args);
                 return r;
             }
@@ -851,6 +852,7 @@ class interpreter {
                 }
             }
             push_frame(e.m_decl, old_size);
+            time_task tt("", m_opts);
             object * o = curry(e.m_addr, args.size(), args2);
             type t = decl_type(e.m_decl);
             if (type_is_scalar(t)) {
@@ -980,6 +982,7 @@ class interpreter {
             }
         }
         if (n > 0) {
+            time_task tt("", m_opts);
             r = apply_n(r, n, args);
         }
         return r;
@@ -1030,6 +1033,7 @@ class interpreter {
             object * args[] = { io_mk_world() };
             object * r = call_boxed(init_decl, 1, args);
             if (io_result_is_ok(r)) {
+                time_task tt("", m_opts);
                 object * o = io_result_get_value(r);
                 mark_persistent(o);
                 dec_ref(r);

src/library/profiling.cpp

@@ -24,8 +24,8 @@ bool get_profiler(options const & opts) {
     return opts.get_bool(*g_profiler, LEAN_DEFAULT_PROFILER);
 }
 
-second_duration get_profiling_threshold(options const & opts) {
-    return second_duration(static_cast<double>(opts.get_unsigned(*g_profiler_threshold, LEAN_DEFAULT_PROFILER_THRESHOLD))/1000.0);
+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() {

src/library/profiling.h

@@ -10,10 +10,10 @@ Author: Gabriel Ebner
 
 namespace lean {
 
-using second_duration = std::chrono::duration<double>;
+using prof_clock = std::chrono::steady_clock;
 
 bool get_profiler(options const &);
-second_duration get_profiling_threshold(options const &);
+prof_clock::duration get_profiling_threshold(options const &);
 
 void initialize_profiling();
 void finalize_profiling();

src/library/time_task.cpp

@@ -43,8 +43,15 @@ void finalize_time_task() {
 
 time_task::time_task(std::string const & category, options const & opts, name decl) :
         m_category(category) {
-    if (get_profiler(opts)) {
-        m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](second_duration duration) mutable {
+    if (!m_category.size()) {
+        // ignore given block in timings of surrounding task, if any
+        if (g_current_time_task) {
+            m_timeit = optional<xtimeit>([](prof_clock::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), [=](prof_clock::duration duration) mutable {
             sstream ss;
             ss << m_category;
             if (decl)
@@ -61,10 +68,16 @@ time_task::time_task(std::string const & category, options const & opts, name de
 time_task::~time_task() {
     if (m_timeit) {
         g_current_time_task = m_parent_task;
-        report_profiling_time(m_category, m_timeit->get_elapsed());
-        if (m_parent_task && m_parent_task->m_timeit)
-            // report exclusive times
-            m_parent_task->m_timeit->exclude_duration(m_timeit->get_elapsed_inclusive());
+        if (m_category.size()) {
+            report_profiling_time(m_category, m_timeit->get_elapsed());
+            if (m_parent_task)
+                // report exclusive times
+                m_parent_task->m_timeit->exclude_duration(m_timeit->get_elapsed_inclusive());
+        } else {
+            if (m_parent_task) {
+                m_parent_task->m_timeit->ignore(*m_timeit);
+            }
+        }
     }
 }
 

src/util/timeit.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <iostream>
 #include <chrono>
+#include "library/profiling.h"
 
 namespace lean {
 using second_duration = std::chrono::duration<double>;
@@ -17,43 +18,18 @@ struct display_profiling_time {
     second_duration m_time;
 };
 
-std::ostream & operator<<(std::ostream & out, display_profiling_time const & time);
-
-/** \brief Low tech timer. */
-class timeit {
-    second_duration m_threshold;
-    std::chrono::steady_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();
-    }
-    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 diff = second_duration(end - m_start);
-        if (diff >= m_threshold) {
-            m_out << m_msg << " " << display_profiling_time{diff} << "\n";
-        }
-    }
-};
-
 /** \brief Low tech timer. */
 class xtimeit {
-    second_duration m_threshold;
-    second_duration m_excluded {0};
-    std::chrono::steady_clock::time_point m_start;
-    std::function<void(second_duration)> m_fn; // NOLINT
+    prof_clock::duration m_threshold;
+    prof_clock::duration m_excluded {0};
+    prof_clock::time_point m_start;
+    std::function<void(prof_clock::duration)> m_fn; // NOLINT
 public:
-    xtimeit(second_duration threshold, std::function<void(second_duration)> const & fn): // NOLINT
+    xtimeit(prof_clock::duration threshold, std::function<void(prof_clock::duration)> const & fn): // NOLINT
         m_threshold(threshold), m_fn(fn) {
-        m_start = std::chrono::steady_clock::now();
+        m_start = prof_clock::now();
     }
-    xtimeit(std::function<void(second_duration)> const & fn) : xtimeit(second_duration(0), fn) {} // NOLINT
+    xtimeit(std::function<void(prof_clock::duration)> const & fn) : xtimeit(prof_clock::duration(0), fn) {} // NOLINT
     xtimeit(xtimeit const &) = delete;
     xtimeit(xtimeit &&) = default;
     ~xtimeit() {
@@ -63,18 +39,31 @@ class xtimeit {
         }
     }
 
-    second_duration get_elapsed_inclusive() const {
-        auto end = std::chrono::steady_clock::now();
-        return second_duration(end - m_start);
+    prof_clock::duration get_elapsed_inclusive() const {
+        auto end = prof_clock::now();
+        return end - m_start;
     }
 
-    second_duration get_elapsed() const {
+    prof_clock::duration get_elapsed() const {
         return get_elapsed_inclusive() - m_excluded;
     }
 
-    void exclude_duration(second_duration d) {
+    void exclude_duration(prof_clock::duration d) {
         m_excluded += d;
     }
+
+    void ignore(xtimeit const & ignored) {
+        // propagate nested times as usual,
+        exclude_duration(ignored.m_excluded);
+        // but exclude this block's time from the directly surrounding task only by adjusting its start time
+        m_start += ignored.get_elapsed();
+        // For example, if elaboration calls an interpreted tactic (without its own category) that calls `simp`,
+        // we subtract the `simp` time from both surrounding categories as usual.
+        // However, if the tactic also spends some time in uncategorized native code,
+        // we subtract it from the interpretation category only by adjusting `m_start`,
+        // which effectively adds the time to the surrounding `elaboration` category instead.
+    }
 };
 
+std::ostream & operator<<(std::ostream & out, display_profiling_time const & time);
 }