diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 597fa6a46..f0692c469 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/test.h"
 #include "util/exception.h"
-#include "util/trace.h"
 #include "util/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/environment.h"
diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index cb2a0b4e0..e4ba200bd 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -40,9 +40,6 @@ add_test(splay_tree "${CMAKE_CURRENT_BINARY_DIR}/splay_tree")
 add_executable(splay_map splay_map.cpp $<TARGET_OBJECTS:util>)
 target_link_libraries(splay_map ${EXTRA_LIBS})
 add_test(splay_map "${CMAKE_CURRENT_BINARY_DIR}/splay_map")
-add_executable(trace trace.cpp $<TARGET_OBJECTS:util>)
-target_link_libraries(trace ${EXTRA_LIBS})
-add_test(trace "${CMAKE_CURRENT_BINARY_DIR}/trace")
 add_executable(exception exception.cpp $<TARGET_OBJECTS:util>)
 target_link_libraries(exception ${EXTRA_LIBS})
 add_test(exception "${CMAKE_CURRENT_BINARY_DIR}/exception")
diff --git a/src/tests/util/interval/double_interval.cpp b/src/tests/util/interval/double_interval.cpp
index 0f6381f7c..4facee167 100644
--- a/src/tests/util/interval/double_interval.cpp
+++ b/src/tests/util/interval/double_interval.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #include "util/test.h"
-#include "util/trace.h"
 #include "util/numerics/double.h"
 #include "util/interval/interval.h"
 #include "tests/util/interval/check.h"
@@ -1031,7 +1030,6 @@ static void double_interval_trans() {
 }
 
 int main() {
-    enable_trace("numerics");
     double_interval_arith();
     double_interval_inf1();
     double_interval_inf2();
diff --git a/src/tests/util/interval/float_interval.cpp b/src/tests/util/interval/float_interval.cpp
index a3b0c00b8..f2237d9ed 100644
--- a/src/tests/util/interval/float_interval.cpp
+++ b/src/tests/util/interval/float_interval.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #include "util/test.h"
-#include "util/trace.h"
 #include "util/numerics/float.h"
 #include "util/interval/interval.h"
 #include "tests/util/interval/check.h"
@@ -1031,7 +1030,6 @@ static void float_interval_trans() {
 }
 
 int main() {
-    enable_trace("numerics");
     float_interval_arith();
     float_interval_inf1();
     float_interval_inf2();
diff --git a/src/tests/util/interval/interval.cpp b/src/tests/util/interval/interval.cpp
index 9dbeb1861..2ba6d7486 100644
--- a/src/tests/util/interval/interval.cpp
+++ b/src/tests/util/interval/interval.cpp
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include <vector>
 #include <algorithm>
 #include "util/test.h"
-#include "util/trace.h"
 #include "util/numerics/double.h"
 #include "util/numerics/mpq.h"
 #include "util/numerics/mpfp.h"
@@ -160,7 +159,6 @@ static void tst3() {
 }
 
 int main() {
-    enable_trace("numerics");
     tst1();
     tst2();
     tst3();
diff --git a/src/tests/util/interval/mpfp_interval.cpp b/src/tests/util/interval/mpfp_interval.cpp
index a2fa2446d..2c4f59b62 100644
--- a/src/tests/util/interval/mpfp_interval.cpp
+++ b/src/tests/util/interval/mpfp_interval.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #include "util/test.h"
-#include "util/trace.h"
 #include "util/numerics/mpfp.h"
 #include "util/interval/interval.h"
 #include "tests/util/interval/check.h"
@@ -1031,7 +1030,6 @@ static void mpfp_interval_trans() {
 }
 
 int main() {
-    enable_trace("numerics");
     mpfp_interval_arith();
     mpfp_interval_inf1();
     mpfp_interval_inf2();
diff --git a/src/tests/util/trace.cpp b/src/tests/util/trace.cpp
deleted file mode 100644
index 445733050..000000000
--- a/src/tests/util/trace.cpp
+++ /dev/null
@@ -1,18 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/test.h"
-#include "util/trace.h"
-using namespace lean;
-
-int main() {
-    lean_assert(!is_trace_enabled("name"));
-    enable_trace("name");
-    lean_assert(is_trace_enabled("name"));
-    disable_trace("name");
-    lean_assert(!is_trace_enabled("name"));
-    return has_violations() ? 1 : 0;
-}
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 57f8f3e22..bbe47d625 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(util OBJECT trace.cpp debug.cpp name.cpp name_set.cpp
+add_library(util OBJECT debug.cpp name.cpp name_set.cpp
   name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp
   bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp
   realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp
index dad4fd4c6..4fc0df7b0 100644
--- a/src/util/init_module.cpp
+++ b/src/util/init_module.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "util/ascii.h"
 #include "util/debug.h"
-#include "util/trace.h"
 #include "util/serializer.h"
 #include "util/thread_script_state.h"
 #include "util/script_state.h"
@@ -19,7 +18,6 @@ Author: Leonardo de Moura
 namespace lean {
 void initialize_util_module() {
     initialize_debug();
-    initialize_trace();
     initialize_serializer();
     initialize_thread();
     initialize_ascii();
@@ -38,7 +36,6 @@ void finalize_util_module() {
     finalize_ascii();
     finalize_thread();
     finalize_serializer();
-    finalize_trace();
     finalize_debug();
 }
 }
diff --git a/src/util/interval/interval.cpp b/src/util/interval/interval.cpp
index 6fc5000fd..b812d0f6b 100644
--- a/src/util/interval/interval.cpp
+++ b/src/util/interval/interval.cpp
@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include <mpfr.h>
 #include <utility>
 #include <algorithm>
-#include "util/trace.h"
 #include "util/numerics/mpz.h"
 #include "util/interval/interval.h"
 
@@ -284,12 +283,10 @@ interval<T> & interval<T>::sub(interval<T> const & o, interval_deps & deps) {
         T new_l_val;
         T new_u_val;
         xnumeral_kind new_l_kind, new_u_kind;
-        lean_trace("numerics", tout << "this: " << *this << " o: " << o << "\n";);
         round_to_minus_inf();
         lean::sub(new_l_val, new_l_kind, m_lower, lower_kind(), o.m_upper, o.upper_kind());
         round_to_plus_inf();
         lean::sub(new_u_val, new_u_kind, m_upper, upper_kind(), o.m_lower, o.lower_kind());
-        lean_trace("numerics", tout << "new: " << new_l_val << " " << new_u_val << "\n";);
         swap(new_l_val, m_lower);
         swap(new_u_val, m_upper);
         m_lower_inf = new_l_kind == XN_MINUS_INFINITY;
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 938e92d5e..8c393cb07 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "util/buffer.h"
 #include "util/memory_pool.h"
 #include "util/hash.h"
-#include "util/trace.h"
 #include "util/ascii.h"
 #include "util/utf8.h"
 #include "util/object_serializer.h"
diff --git a/src/util/trace.cpp b/src/util/trace.cpp
deleted file mode 100644
index 79471bd91..000000000
--- a/src/util/trace.cpp
+++ /dev/null
@@ -1,49 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-
-#include <set>
-#include <string>
-#include <memory>
-#include "util/trace.h"
-
-#ifndef LEAN_TRACE_OUT
-#define LEAN_TRACE_OUT ".lean_trace"
-#endif
-
-namespace lean {
-
-#ifdef LEAN_TRACE
-std::ofstream tout(LEAN_TRACE_OUT);
-mutex         trace_mutex;
-#endif
-
-static std::set<std::string> * g_enabled_trace_tags = nullptr;
-
-void initialize_trace() {
-    // lazy initialization
-}
-
-void finalize_trace() {
-    delete g_enabled_trace_tags;
-}
-
-void enable_trace(char const * tag) {
-    if (!g_enabled_trace_tags)
-        g_enabled_trace_tags = new std::set<std::string>();
-    g_enabled_trace_tags->insert(tag);
-}
-
-void disable_trace(char const * tag) {
-    if (g_enabled_trace_tags)
-        g_enabled_trace_tags->erase(tag);
-}
-
-bool is_trace_enabled(char const * tag) {
-    return g_enabled_trace_tags && g_enabled_trace_tags->find(tag) != g_enabled_trace_tags->end();
-}
-
-}
diff --git a/src/util/trace.h b/src/util/trace.h
deleted file mode 100644
index 11a942563..000000000
--- a/src/util/trace.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-
-#ifdef LEAN_TRACE
-#include "util/thread.h"
-#include <fstream>
-namespace lean {
-extern std::ofstream tout;
-extern mutex         trace_mutex;
-}
-#define TRACE_CODE(CODE) { lock_guard<mutex> _lean_trace_lock_(lean::trace_mutex); CODE }
-#else
-#define TRACE_CODE(CODE)
-#endif
-
-#define lean_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); })
-
-#define lean_simple_trace(TAG, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG)) { CODE lean::tout.flush(); })
-
-#define lean_cond_trace(TAG, COND, CODE) TRACE_CODE(if (lean::is_trace_enabled(TAG) && (COND)) { lean::tout << "-------- [" << TAG << "] " << __FUNCTION__ << " " << __FILE__ << ":" << __LINE__ << " ---------\n"; CODE lean::tout << "------------------------------------------------\n"; lean::tout.flush(); })
-
-namespace lean {
-void enable_trace(char const * tag);
-void disable_trace(char const * tag);
-bool is_trace_enabled(char const * tag);
-void initialize_trace();
-void finalize_trace();
-}