diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index edece6a267..cf62222012 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -434,6 +434,10 @@ def eprint [ToString α] (s : α) : IO Unit := do
 def eprintln [ToString α] (s : α) : IO Unit :=
   eprint <| toString s |>.push '\n'
 
+@[export lean_io_eprint]
+private def eprintAux (s : String) : IO Unit :=
+  eprint s
+
 @[export lean_io_eprintln]
 private def eprintlnAux (s : String) : IO Unit :=
   eprintln s
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index e23ccc6f37..4b38761ebe 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -275,7 +275,7 @@ value unbox_t(object * o, type t) {
 }
 
 /** \pre Very simple debug output of arbitrary values, should be extended. */
-void print_value(std::ostream & ios, value const & v, type t) {
+void print_value(tout & ios, value const & v, type t) {
     if (t == type::Float) {
         ios << v.m_float;
     } else if (type_is_scalar(t)) {
@@ -292,6 +292,10 @@ void print_value(std::ostream & ios, value const & v, type t) {
     }
 }
 
+void print_value(tout const & ios, value const & v, type t) {
+  return print_value(const_cast<tout &>(ios), v, t);
+}
+
 void * lookup_symbol_in_cur_exe(char const * sym) {
 #ifdef LEAN_WINDOWS
     HMODULE hmods[128];  // 128 modules should be enough for everyone
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index ed1d2c9cdc..b173513388 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -122,8 +122,16 @@ scope_trace_env::~scope_trace_env() {
     get_disabled_trace_classes().resize(m_disable_sz);
 }
 
-std::ostream & tout() {
-    return std::cerr;
+extern "C" obj_res lean_io_eprint(obj_arg s, obj_arg w);
+static void io_eprint(obj_arg s) {
+    object * r = lean_io_eprint(s, lean_io_mk_world());
+    if (!lean_io_result_is_ok(r))
+        lean_io_result_show_error(r);
+    lean_dec(r);
+}
+
+tout::~tout() {
+    io_eprint(mk_string(m_out.str()));
 }
 
 std::ostream & operator<<(std::ostream & ios, tclass const & c) {
diff --git a/src/library/trace.h b/src/library/trace.h
index 17adeb83ee..3eae4a7af9 100644
--- a/src/library/trace.h
+++ b/src/library/trace.h
@@ -32,7 +32,18 @@ public:
 
 struct tclass { name m_cls; tclass(name const & c):m_cls(c) {} };
 
-std::ostream & tout();
+struct tout {
+    sstream m_out;
+    ~tout();
+};
+
+template <typename T>
+tout & operator<<(tout const & out, T const & t) {
+    tout & out_mut = const_cast<tout &>(out);
+    out_mut.m_out << t;
+    return out_mut;
+}
+
 std::ostream & operator<<(std::ostream & ios, tclass const &);
 
 #define lean_trace(CName, CODE) {               \