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

chore: log cumulative #eval execution time

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

9
src/frontends/lean/builtin_cmds.cpp
View file

@ -388,12 +388,9 @@ static environment eval_cmd(parser & p) {
object_ref r;
try {
if (p.profiling()) {
timeit timer(out.get_text_stream().get_stream(), "eval time");
r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
} else {
r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
}
time_task t("#eval execution",
message_builder(environment(), get_global_ios(), "foo", pos_info(), message_severity::INFORMATION));
r = object_ref(ir::run_boxed(new_env, fn_name, args.size(), &args[0]));
} catch (exception & ex) {
std::cout.rdbuf(saved_cout);
out.report();