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

fix: use redirected stderr for timeit & allocprof

Browse source
This commit is contained in:
Sebastian Ullrich 2021-12-16 14:51:50 +01:00 • committed by Leonardo de Moura
parent 87e860f871
commit 1221bdd3c7
2 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/runtime/io.cpp
View file

@ -429,21 +429,27 @@ extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg
w = apply_1(fn, w);
auto end = std::chrono::steady_clock::now();
auto diff = std::chrono::duration<double>(end - start);
std::ostream & out = std::cerr; // TODO(Leo): replace?
sstream out;
out << std::setprecision(3);
if (diff < std::chrono::duration<double>(1)) {
out << string_cstr(msg) << " " << std::chrono::duration<double, std::milli>(diff).count() << "ms\n";
out << string_cstr(msg) << " " << std::chrono::duration<double, std::milli>(diff).count() << "ms";
} else {
out << string_cstr(msg) << " " << diff.count() << "s\n";
out << string_cstr(msg) << " " << diff.count() << "s";
}
io_eprintln(mk_string(out.str()));
return w;
}
/* allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α */
extern "C" LEAN_EXPORT obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) {
std::ostream & out = std::cerr; // TODO(Leo): replace?
allocprof prof(out, string_cstr(msg));
return apply_1(fn, w);
std::ostringstream out;
obj_res res;
{
allocprof prof(out, string_cstr(msg));
res = apply_1(fn, w);
}
io_eprintln(mk_string(out.str()));
return res;
}
/* getNumHeartbeats : BaseIO Nat */

1
src/runtime/object.h
View file

@ -476,6 +476,7 @@ inline b_obj_res io_result_get_value(b_obj_arg r) { return lean_io_result_get_va
inline b_obj_res io_result_get_error(b_obj_arg r) { return lean_io_result_get_error(r); }
inline void io_result_show_error(b_obj_arg r) { return lean_io_result_show_error(r); }
inline void io_mark_end_initialization() { return lean_io_mark_end_initialization(); }
void io_eprintln(obj_arg s);
// =======================================
// ST ref primitives