From 1221bdd3c7d5395baa451ce8fdd2c2f8a00cbc8f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 16 Dec 2021 14:51:50 +0100
Subject: [PATCH] fix: use redirected stderr for `timeit` & `allocprof`

---
 src/runtime/io.cpp   | 18 ++++++++++++------
 src/runtime/object.h |  1 +
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 198064cdca..44f31489c5 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -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 */
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 38613cf47c..b227ce9cb3 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -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