diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 08a53a989f..686d196ca6 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -132,7 +132,6 @@ static void finalize_definition(elaborator & elab, buffer const & params, 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), c_real_name); return compile(env, p.get_options(), c_real_name); } catch (exception & ex) { // FIXME(gabriel): use position from exception diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index f506e411ad..1a7ccf28c9 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/max_sharing.h" #include "library/trace.h" #include "library/sorry.h" +#include "library/time_task.h" #include "library/compiler/util.h" #include "library/compiler/lcnf.h" #include "library/compiler/find_jp.h" @@ -184,6 +185,9 @@ environment compile(environment const & env, options const & opts, names cs) { if (has_synthetic_sorry(cinfo)) return env; } + time_task t("compilation", + message_builder(environment(), get_global_ios(), "foo", pos_info(), message_severity::INFORMATION)); + comp_decls ds = to_comp_decls(env, cs); csimp_cfg cfg(opts); auto simp = [&](environment const & env, expr const & e) { return csimp(env, e, cfg); };