feat(library/time_task): print cumulative times on --profile

doc/changes.md

@@ -133,6 +133,8 @@ master branch (aka work in progress branch)
   value of a superclass. This change eliminates the need for most `..` source specifiers
   in instance declarations.
 
+* The `--profile` flag will now print cumulative profiling times at the end of execution
+
 *Changes*
 
 * Command `variable [io.interface]` is not needed anymore to use the `io` monad.

src/frontends/lean/definition_cmds.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <vector>
+#include "library/time_task.h"
 #include "library/profiling.h"
 #include "library/library_task_builder.h"
 #include "library/sorry.h"
@@ -179,17 +180,8 @@ static void finalize_definition(elaborator & elab, buffer<expr> const & params,
 
 static certified_declaration check(parser & p, environment const & env, name const & c_name, declaration const & d, pos_info const & pos) {
     try {
-        if (p.profiling()) {
-            xtimeit timer(get_profiling_threshold(p.get_options()), [&](second_duration duration) {
-                    auto msg = p.mk_message(pos, INFORMATION);
-                    msg.get_text_stream().get_stream()
-                        << "type checking time of " << c_name << " took " << display_profiling_time{duration} << "\n";
-                    msg.report();
-                });
-            return ::lean::check(env, d);
-        } else {
-            return ::lean::check(env, d);
-        }
+        time_task _("type checking", p.mk_message(pos, INFORMATION), p.get_options(), c_name);
+        return ::lean::check(env, d);
     } catch (kernel_exception & ex) {
         unsigned i = get_pp_indent(p.get_options());
         auto pp_fn = ::lean::mk_pp_ctx(env, p.get_options(), metavar_context(), local_context());
@@ -226,6 +218,7 @@ static bool check_noncomputable(bool ignore_noncomputable, environment const & e
 static environment compile_decl(parser & p, environment const & env,
                                 name const & c_name, name const & c_real_name, pos_info const & pos) {
     try {
+        time_task _("compilation", p.mk_message(message_severity::INFORMATION), p.get_options(), c_real_name);
         return vm_compile(env, env.get(c_real_name));
     } catch (exception & ex) {
         // FIXME(gabriel): use position from exception
@@ -531,6 +524,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
                                                      bool is_example, bool is_instance, bool is_meta, bool is_abbrev) {
     parser::local_scope scope1(p);
     auto header_pos = p.pos();
+    time_task _("parsing", p.mk_message(header_pos, INFORMATION), p.get_options());
     declaration_name_scope scope2;
     expr fn = parse_single_header(p, scope2, lp_names, params, is_example, is_instance);
     expr val;
@@ -600,17 +594,8 @@ static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind
 }
 
 static expr_pair elaborate_definition(parser & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
-    if (p.profiling()) {
-        xtimeit timer(get_profiling_threshold(p.get_options()), [&](second_duration duration) {
-                auto msg = p.mk_message(pos, INFORMATION);
-                msg.get_text_stream().get_stream()
-                    << "elaboration of " << fn << " took " << display_profiling_time{duration} << "\n";
-                msg.report();
-            });
-        return elaborate_definition_core(elab, kind, fn, val);
-    } else {
-        return elaborate_definition_core(elab, kind, fn, val);
-    }
+    time_task _("elaboration", p.mk_message(pos, INFORMATION), p.get_options(), mlocal_pp_name(fn));
+    return elaborate_definition_core(elab, kind, fn, val);
 }
 
 static void finalize_theorem_type(elaborator & elab, buffer<expr> const & params, expr & type,
@@ -669,15 +654,9 @@ static expr elaborate_proof(
         elaborator elab(decl_env, opts, get_namespace(decl_env) + mlocal_pp_name(fn), mctx, lctx, recover_from_errors);
 
         expr val, type;
-        if (get_profiler(opts)) {
-            xtimeit timer(get_profiling_threshold(opts), [&](second_duration duration) {
-                auto msg = message_builder(decl_env, get_global_ios(), file_name, header_pos, INFORMATION);
-                msg.get_text_stream().get_stream()
-                        << "elaboration of " << mlocal_pp_name(fn) << " took " << display_profiling_time{duration} << "\n";
-                msg.report();
-            });
-            std::tie(val, type) = elab.elaborate_with_type(val0, mk_as_is(mlocal_type(fn)));
-        } else {
+        {
+            time_task _("elaboration", message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, INFORMATION),
+                        opts, mlocal_pp_name(fn));
             std::tie(val, type) = elab.elaborate_with_type(val0, mk_as_is(mlocal_type(fn)));
         }
 
@@ -839,6 +818,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
             finalize_definition(elab, new_params, type, val, lp_names, meta.m_modifiers.m_is_meta);
             env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, prv_name, type, some_expr(val), {}, meta, is_abbrev, header_pos);
         }
+        time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), p.get_options(), c_name);
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;
         if (is_rfl) new_env = mark_rfl_lemma(new_env, c_real_name);

src/library/CMakeLists.txt

@@ -20,4 +20,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   eval_helper.cpp
   messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
   documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp
-  pipe.cpp handle.cpp profiling.cpp)
+  pipe.cpp handle.cpp profiling.cpp time_task.cpp)

src/library/init_module.cpp

@@ -52,6 +52,7 @@ Author: Leonardo de Moura
 #include "library/check.h"
 #include "library/parray.h"
 #include "library/profiling.h"
+#include "library/time_task.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -115,9 +116,11 @@ void initialize_library_module() {
     initialize_check();
     initialize_congr_lemma();
     initialize_parray();
+    initialize_time_task();
 }
 
 void finalize_library_module() {
+    finalize_time_task();
     finalize_parray();
     finalize_congr_lemma();
     finalize_check();

src/library/message_builder.h

@@ -13,7 +13,7 @@ Author: Gabriel Ebner
 
 namespace lean {
 
-/** Buider for a message object.  Automatically reports the message on destruction. */
+/** Builder for a message object. */
 class message_builder {
     std::shared_ptr<abstract_type_context> m_tc;
     std::string                            m_file_name;

src/library/time_task.cpp

@@ -0,0 +1,39 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+
+#include <map>
+#include "library/time_task.h"
+
+namespace lean {
+
+static std::map<std::string, second_duration> * g_cum_times;
+static mutex * g_cum_times_mutex;
+
+void report_profiling_time(std::string const & category, second_duration time) {
+    lock_guard<mutex> _(*g_cum_times_mutex);
+    (*g_cum_times)[category] += time;
+}
+
+void display_cumulative_profiling_times(std::ostream & out) {
+    if (g_cum_times->empty())
+        return;
+    out << "cumulative profiling times:\n";
+    for (auto const & p : *g_cum_times)
+        out << "\t" << p.first << " " << display_profiling_time{p.second} << "\n";
+}
+
+void initialize_time_task() {
+    g_cum_times_mutex = new mutex;
+    g_cum_times = new std::map<std::string, second_duration>;
+}
+
+void finalize_time_task() {
+    delete g_cum_times;
+    delete g_cum_times_mutex;
+}
+}
+

src/library/time_task.h

@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#pragma once
+#include <string>
+#include "library/message_builder.h"
+#include "library/profiling.h"
+#include "util/timeit.h"
+
+namespace lean {
+void report_profiling_time(std::string const & category, second_duration time);
+void display_cumulative_profiling_times(std::ostream & out);
+
+/** Measure time of some task and report it for the final cumulative profile. */
+class time_task {
+    std::string     m_category;
+    optional<xtimeit> m_timeit;
+public:
+    time_task(std::string const & category, message_builder builder, options const & opts, name decl = name()):
+            m_category(category) {
+        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());
+    }
+};
+
+void initialize_time_task();
+void finalize_time_task();
+}

src/library/vm/interaction_state_imp.h

@@ -12,6 +12,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include "library/profiling.h"
 #include "library/constants.h"
 #include "library/message_builder.h"
+#include "library/time_task.h"
 #include "library/vm/interaction_state.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
@@ -222,7 +223,16 @@ environment interaction_monad<State>::evaluator::compile(name const & interactio
     }
     try {
         bool optimize_bytecode = false;
-        return vm_compile(new_env, new_env.get(interaction_name), optimize_bytecode);
+        if (provider) {
+            auto out = message_builder(environment(), get_global_ios(),
+                                       get_pos_info_provider()->get_file_name(),
+                                       get_pos_info_provider()->get_pos_info_or_some(interaction),
+                                       INFORMATION);
+            time_task _("elaboration: tactic compilation", out, m_opts);
+            return vm_compile(new_env, new_env.get(interaction_name), optimize_bytecode);
+        } else {
+            return vm_compile(new_env, new_env.get(interaction_name), optimize_bytecode);
+        }
     } catch (exception & ex) {
         throw formatted_exception(some(interaction), format(ex.what()));
     }
@@ -263,7 +273,7 @@ vm_obj interaction_monad<State>::evaluator::operator()(expr const & interaction,
                                    get_pos_info_provider()->get_pos_info_or_some(interaction),
                                    INFORMATION);
         out.set_caption("tactic profile data");
-        if (prof.get_snapshots().display("tactic", m_opts, out.get_text_stream().get_stream()))
+        if (prof.get_snapshots().display("elaboration: tactic", m_opts, out.get_text_stream().get_stream()))
             out.report();
     }
 

src/library/vm/vm.cpp

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/profiling.h"
 #include "library/util.h"
+#include "library/time_task.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_option.h"
@@ -3554,6 +3555,7 @@ void vm_state::profiler::snapshots::display(std::ostream & out) const {
 }
 
 bool vm_state::profiler::snapshots::display(std::string const &what, options const &opts, std::ostream &out) const {
+    report_profiling_time(what + " execution", m_total_time);
     if (m_total_time >= get_profiling_threshold(opts)) {
         out << what << " execution took " << display_profiling_time{m_total_time} << "\n";
         display(out);

src/shell/lean.cpp

@@ -39,6 +39,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/export.h"
 #include "library/message_builder.h"
+#include "library/time_task.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/dependencies.h"
@@ -743,6 +744,8 @@ int main(int argc, char ** argv) {
             }
         }
 
+        display_cumulative_profiling_times(std::cerr);
+
         // if (!mods.empty() && export_native_objects) {
         //     // this code is now broken
         //     env = lean::set_native_module_path(env, lean::name(native_output));

src/util/timeit.h

@@ -54,12 +54,16 @@ public:
     xtimeit(xtimeit const &) = delete;
     xtimeit(xtimeit &&) = default;
     ~xtimeit() {
-        auto end = std::chrono::steady_clock::now();
-        auto diff = second_duration(end - m_start);
+        auto diff = get_elapsed();
         if (diff >= m_threshold && m_fn) {
             m_fn(diff);
         }
     }
+
+    second_duration get_elapsed() const {
+        auto end = std::chrono::steady_clock::now();
+        return second_duration(end - m_start);
+    }
 };
 
 }