max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: improve precision of compilation time profiling

Browse source
This commit is contained in:
Sebastian Ullrich 2020-04-23 16:23:52 +02:00
parent 24f22f7643
commit ec9f4b579d
2 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/definition_cmds.cpp
View file

@ -132,7 +132,6 @@ static void finalize_definition(elaborator & elab, buffer<expr> 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

4
src/library/compiler/compiler.cpp
View file

@ -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); };