From a2ef818ff3fd48ff5a571c6637a15390907941ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 09:06:10 -0800 Subject: [PATCH] chore(*): remove old tracing framework --- src/tests/kernel/environment.cpp | 1 - src/tests/util/CMakeLists.txt | 3 -- src/tests/util/interval/double_interval.cpp | 2 - src/tests/util/interval/float_interval.cpp | 2 - src/tests/util/interval/interval.cpp | 2 - src/tests/util/interval/mpfp_interval.cpp | 2 - src/tests/util/trace.cpp | 18 -------- src/util/CMakeLists.txt | 2 +- src/util/init_module.cpp | 3 -- src/util/interval/interval.cpp | 3 -- src/util/name.cpp | 1 - src/util/trace.cpp | 49 --------------------- src/util/trace.h | 33 -------------- 13 files changed, 1 insertion(+), 120 deletions(-) delete mode 100644 src/tests/util/trace.cpp delete mode 100644 src/util/trace.cpp delete mode 100644 src/util/trace.h 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 #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_link_libraries(splay_map ${EXTRA_LIBS}) add_test(splay_map "${CMAKE_CURRENT_BINARY_DIR}/splay_map") -add_executable(trace trace.cpp $) -target_link_libraries(trace ${EXTRA_LIBS}) -add_test(trace "${CMAKE_CURRENT_BINARY_DIR}/trace") add_executable(exception exception.cpp $) 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 #include #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 #include #include -#include "util/trace.h" #include "util/numerics/mpz.h" #include "util/interval/interval.h" @@ -284,12 +283,10 @@ interval & interval::sub(interval 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 -#include -#include -#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 * 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(); - 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 -namespace lean { -extern std::ofstream tout; -extern mutex trace_mutex; -} -#define TRACE_CODE(CODE) { lock_guard _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(); -}