fix(library/trace): use null output channel when trace environment is not set

This is important when multiple threads are being used, and the trace
environment is not set for a child thread

src/library/trace.cpp

@@ -20,7 +20,8 @@ LEAN_THREAD_PTR(io_state,    g_ios);
 LEAN_THREAD_VALUE(unsigned,  g_depth, 0);
 
 void register_trace_class(name const & n) {
-    register_option(name("trace") + n, BoolOption, "false", "(trace) enable/disable tracing for the given module and submodules");
+    register_option(name("trace") + n, BoolOption, "false",
+                    "(trace) enable/disable tracing for the given module and submodules");
     g_trace_classes->insert(n);
 }
 
@@ -118,11 +119,21 @@ scope_trace_init_bool_option::~scope_trace_init_bool_option() {
     }
 }
 
+struct silent_ios_helper {
+    std::shared_ptr<output_channel> m_out;
+    io_state                        m_ios;
+    silent_ios_helper():
+        m_out(new null_output_channel()),
+        m_ios(get_dummy_ios(), m_out, m_out) {}
+};
+
+MK_THREAD_LOCAL_GET_DEF(silent_ios_helper, get_silent_ios_helper);
+
 io_state_stream tout() {
     if (g_env) {
         return diagnostic(*g_env, *g_ios);
     } else {
-        return diagnostic(get_dummy_env(), get_dummy_ios());
+        return diagnostic(get_dummy_env(), get_silent_ios_helper().m_ios);
     }
 }
 

src/util/CMakeLists.txt

@@ -4,4 +4,5 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp
   realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
   lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp
   serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp
-  init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp)
+  init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp
+  null_ostream.cpp)

src/util/null_ostream.cpp

@@ -0,0 +1,22 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <fstream>
+#include "util/thread.h"
+#include "util/null_ostream.h"
+
+namespace lean {
+int null_streambuf::overflow(int c) {
+    setp(m_buffer, m_buffer+sizeof(m_buffer));
+    return (c == std::ifstream::traits_type::eof()) ? '\0' : c;
+}
+
+MK_THREAD_LOCAL_GET_DEF(null_streambuf, get_null_streambuf);
+
+null_streambuf * null_ostream::rdbuf() const {
+    return &get_null_streambuf();
+}
+}

src/util/null_ostream.h

@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <iostream>
+
+#define LEAN_NULL_AUX_BUFFER_SIZE 64
+
+namespace lean {
+class null_streambuf : public std::streambuf {
+    char                m_buffer[LEAN_NULL_AUX_BUFFER_SIZE];
+protected:
+    virtual int overflow(int c) override;
+};
+
+class null_ostream : public std::ostream {
+public:
+    null_streambuf * rdbuf() const;
+};
+}

src/util/output_channel.h

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include <fstream>
 #include <sstream>
 #include <string>
-
+#include "util/null_ostream.h"
 namespace lean {
 /**
     \brief Wrapper for std::ostream.
@@ -52,6 +52,13 @@ public:
     virtual std::ostream & get_stream() { return m_out; }
     std::string str() const { return m_out.str(); }
 };
+class null_output_channel : public output_channel {
+    null_ostream m_out;
+public:
+    null_output_channel() {}
+    virtual ~null_output_channel() {}
+    virtual std::ostream & get_stream() { return m_out; }
+};
 template<typename T>
 output_channel & operator<<(output_channel & out, T const & v) {
     out.get_stream() << v;