From 7b28419260b18d8eb36abd2cf283fb8a286dd2c7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 18:23:22 -0700 Subject: [PATCH] chore(*): disable multi thread support for OSX, remove the !defined(APPLE) directives We should re-enable multi thread support for OSX as soon as the bug in clang is fixed. Signed-off-by: Leonardo de Moura --- .travis.osx.yml | 15 ++++++++++----- src/tests/kernel/threads.cpp | 2 +- src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/tactic/tactic.cpp | 2 +- src/tests/util/lazy_list.cpp | 2 +- src/tests/util/rb_tree.cpp | 4 ++-- src/tests/util/thread.cpp | 2 +- 7 files changed, 17 insertions(+), 12 deletions(-) diff --git a/.travis.osx.yml b/.travis.osx.yml index 17b5c60f9..b165ba431 100644 --- a/.travis.osx.yml +++ b/.travis.osx.yml @@ -4,15 +4,20 @@ env: # DROPBOX_KEY=[secure] - secure: "W8vou0KRJOOboZXP9q+D/9Wl6LlBeVS2T85MHWPz7EwCMQbJq5xWnGzYLE6FmC0iILcZkXyP63vqoYMFo5MJaEQeALGx2RuIiW7XgrD+7Bn4Vfsp6BLT7K9/AJETGGTQnLs8oZJJCXHGtzbc8EPFIZd/ZPPrve4jhEE5ZNhXnRc=" matrix: - - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=DEBUG TCMALLOC=OFF PUSH_TO_CDASH=TRUE LUA=51 - - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF PUSH_TO_CDASH=TRUE LUA=51 UPLOAD=osx PACKAGE=TRUE - - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF PUSH_TO_CDASH=TRUE LUA=52 - - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF PUSH_TO_CDASH=TRUE LUA=JIT + - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=DEBUG TCMALLOC=OFF MULTI_THREAD=OFF PUSH_TO_CDASH=TRUE LUA=51 + - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF MULTI_THREAD=OFF PUSH_TO_CDASH=TRUE LUA=51 UPLOAD=osx PACKAGE=TRUE + - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF MULTI_THREAD=OFF PUSH_TO_CDASH=TRUE LUA=52 + - CMAKE_CXX_COMPILER=g++ CMAKE_BUILD_TYPE=RELEASE TCMALLOC=OFF MULTI_THREAD=OFF PUSH_TO_CDASH=TRUE LUA=JIT # Turn off tcmalloc on OSX due to segmentation fault. # Soonho filed a bug report for this: # https://code.google.com/p/gperftools/issues/detail?id=573&thanks=573&ts=1379701793 +# Turn off Thread on OSX due to segmantation fault. +# This is due to a bug in clang C++11 on OSX. +# Soonho has reported the issue to the clang developers. +# It is a known bug. + before_script: - mkdir -p build - cd build @@ -20,7 +25,7 @@ before_script: - export CPLUS_INCLUDE_PATH - LIBRARY_PATH=/usr/local/lib:/usr/local/lib/gcc/x86_64-apple-darwin12.5.0/4.8.1/ - export LIBRARY_PATH -- cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTCMALLOC=${TCMALLOC} -DCMAKE_CXX_COMPILER=/usr/local/bin/${CMAKE_CXX_COMPILER} ../src -G Ninja +- cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DTCMALLOC=${TCMALLOC} -DMULTI_THREAD=${MULTI_THREAD} -DCMAKE_CXX_COMPILER=/usr/local/bin/${CMAKE_CXX_COMPILER} ../src -G Ninja - cd .. # Remark: diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 9976cc9b7..072d7770f 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -51,7 +51,7 @@ static void tst1() { a = f(a, a); std::vector ts; - #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) + #if defined(LEAN_MULTI_THREAD) for (unsigned i = 0; i < 8; i++) { ts.push_back(thread([&](){ save_stack_info(); mk(a); })); } diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 39ab91554..86d9a65af 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -228,7 +228,7 @@ static expr mk_big(unsigned depth) { } static void tst12() { -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env; init_test_frontend(env); diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 03b1bc67a..e8370d6fd 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -68,7 +68,7 @@ static void tst1() { check_failure(now_tactic(), env, io, ctx, q); std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q).get_proof() << "\n"; -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) check_failure(try_for(loop_tactic(), 100), env, io, ctx, q); std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s).get_proof() << "\n"; check_failure(try_for(orelse(try_for(loop_tactic(), 10000), diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp index 5367bdb9d..4ddca2087 100644 --- a/src/tests/util/lazy_list.cpp +++ b/src/tests/util/lazy_list.cpp @@ -94,7 +94,7 @@ static void tst1() { display(orelse(lazy_list(), take(10, seq(100)))); display(orelse(take(0, seq(1)), take(10, seq(100)))); display(orelse(filter(take(100, seq(1)), [](int i) { return i < 0; }), take(10, seq(1000)))); -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) display(timeout(append(append(take(10, seq(1)), loop()), seq(100)), 5)); display(take(10, par(seq(1), loop()))); #endif diff --git a/src/tests/util/rb_tree.cpp b/src/tests/util/rb_tree.cpp index 4ac97322b..93fd7d1ac 100644 --- a/src/tests/util/rb_tree.cpp +++ b/src/tests/util/rb_tree.cpp @@ -193,7 +193,7 @@ static void tst5() { #define DEFAULT_STEP 5 #endif -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) static void tst6() { int_rb_tree t; const unsigned SZ = DEFAULT_SZ; @@ -241,7 +241,7 @@ int main() { tst3(); tst4(); tst5(); -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) tst6(); #endif return has_violations() ? 1 : 0; diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 4d36087ab..f251e4e70 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" using namespace lean; -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) +#if defined(LEAN_MULTI_THREAD) void foo() { static LEAN_THREAD_LOCAL std::vector v(1024); if (v.size() != 1024) {