michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(*): remove old tracing framework

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-08 09:06:10 -08:00
parent ab91f8dd5f
commit a2ef818ff3
13 changed files with 1 additions and 120 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/tests/kernel/environment.cpp
View file

@ -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"

3
src/tests/util/CMakeLists.txt
View file

@ -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")

2
src/tests/util/interval/double_interval.cpp
View file

@ -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();

2
src/tests/util/interval/float_interval.cpp
View file

@ -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();

2
src/tests/util/interval/interval.cpp
View file

@ -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();

2
src/tests/util/interval/mpfp_interval.cpp
View file

@ -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();

18
src/tests/util/trace.cpp
View file

@ -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;
}

2
src/util/CMakeLists.txt
View file

@ -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

3
src/util/init_module.cpp
View file

@ -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();
}
}

3
src/util/interval/interval.cpp
View file

@ -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;

1
src/util/name.cpp
View file

@ -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"

49
src/util/trace.cpp
View file

@ -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();
}
}

33
src/util/trace.h
View file

@ -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();
}