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 <leonardo@microsoft.com>

.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=DEBUG   TCMALLOC=OFF MULTI_THREAD=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 MULTI_THREAD=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 MULTI_THREAD=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=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:

src/tests/kernel/threads.cpp

@@ -51,7 +51,7 @@ static void tst1() {
     a = f(a, a);
     std::vector<thread> 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); }));
     }

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

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),

src/tests/util/lazy_list.cpp

@@ -94,7 +94,7 @@ static void tst1() {
     display(orelse(lazy_list<int>(), 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

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;

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<int> v(1024);
     if (v.size() != 1024) {