feat(library/module_mgr): profile .olean serialization/deserialization

src/frontends/lean/definition_cmds.cpp

@@ -189,7 +189,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);
+        time_task _("compilation", p.mk_message(message_severity::INFORMATION), c_real_name);
         return vm_compile(env, env.get(c_real_name));
     } catch (exception & ex) {
         // FIXME(gabriel): use position from exception
@@ -308,7 +308,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());
+    time_task _("parsing", p.mk_message(header_pos, INFORMATION));
     declaration_name_scope scope2;
     expr fn = parse_single_header(p, scope2, lp_names, params, is_example, is_instance);
     expr val;
@@ -380,7 +380,7 @@ 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) {
-    time_task _("elaboration", p.mk_message(pos, INFORMATION), p.get_options(), local_pp_name_p(fn));
+    time_task _("elaboration", p.mk_message(pos, INFORMATION), local_pp_name_p(fn));
     return elaborate_definition_core(elab, kind, fn, val);
 }
 
@@ -438,7 +438,7 @@ static expr elaborate_proof(
         expr val, type;
         {
             time_task _("elaboration", message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, INFORMATION),
-                        opts, local_pp_name_p(fn));
+                        local_pp_name_p(fn));
             std::tie(val, type) = elab.elaborate_with_type(val0, mk_as_is(local_type_p(fn)));
         }
 
@@ -581,7 +581,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
             finalize_definition(elab, new_params, type, val, lp_names);
             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);
+        time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), c_name);
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;
         new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);

src/library/module.cpp

@@ -24,6 +24,7 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include "library/noncomputable.h"
 #include "library/constants.h"
 #include "library/module_mgr.h"
+#include "library/time_task.h"
 
 /*
 Missing features: non monotonic modifications in .olean files
@@ -219,6 +220,8 @@ bool is_candidate_olean_file(std::string const & file_name) {
 
 olean_data parse_olean(std::istream & in, std::string const & file_name, bool check_hash) {
     std::vector<module_name> imports;
+    time_task t(".olean deserialization",
+                message_builder(environment(), get_global_ios(), file_name, pos_info(), message_severity::INFORMATION));
 
     deserializer d1(in, optional<std::string>(file_name));
     std::string header, version;

src/library/module_mgr.cpp

@@ -13,6 +13,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich
 #include "util/file_lock.h"
 #include "library/module_mgr.h"
 #include "library/module.h"
+#include "library/time_task.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/parser.h"
 
@@ -57,6 +58,9 @@ static void compile_olean(search_path const & path, std::shared_ptr<module_info>
 
     auto olean_fn = olean_of_lean(find_file(path, mod->m_name, {".lean"}));
     lean_trace("import", tout() << "saving " << olean_fn << "\n";);
+    time_task t(".olean serialization",
+                message_builder(environment(), get_global_ios(), mod->m_filename, pos_info(),
+                                message_severity::INFORMATION));
     exclusive_file_lock output_lock(olean_fn);
     std::ofstream out(olean_fn, std::ios_base::binary);
     write_module(*mod->m_loaded_module, out);
@@ -130,7 +134,13 @@ void module_mgr::build_lean(std::shared_ptr<module_info> const & mod, name_set c
     }
 
     std::istringstream in(contents);
-    auto env = import_modules(m_initial_env, imports, mk_loader());
+    environment env;
+    {
+        time_task t("building env from imports",
+                    message_builder(environment(), get_global_ios(), mod->m_filename, pos_info(),
+                                    message_severity::INFORMATION));
+        env = import_modules(m_initial_env, imports, mk_loader());
+    }
     parser p(env, m_ios, in, mod->m_filename);
     p.parse_commands();
     mod->m_loaded_module = std::make_shared<loaded_module const>(export_module(p.env(), mod_name));

src/library/time_task.h

@@ -19,8 +19,9 @@ 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()):
+    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;

src/library/vm/interaction_state_imp.h

@@ -227,7 +227,7 @@ environment interaction_monad<State>::evaluator::compile(name const & interactio
                                        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);
+            time_task _("elaboration: tactic compilation", out);
             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);