From 60a1ac319224fd00aa82de93eba8941d68d83f5f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Jun 2014 12:43:27 -0700 Subject: [PATCH] doc(cmake/osx10.8): add note regarding multi-thread support on OSX Signed-off-by: Leonardo de Moura --- doc/make/osx-10.8.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/doc/make/osx-10.8.md b/doc/make/osx-10.8.md index 86bc3e93e..f1f9d9e15 100644 --- a/doc/make/osx-10.8.md +++ b/doc/make/osx-10.8.md @@ -16,3 +16,23 @@ Instructions for installing gcc-4.8 (C++11 compatible) on OS X 10.8 Instructions for installing clang-3.3 (C++11 compatible) on OS X 10.8 brew install llvm --with-clang --with-asan + +It seems there is a bug in the implementation of `thread_local` +storage specifier on clang++ and g++ on OSX. One possible +workaround is to disable multi threaded support in Lean, we just have to provide +the option + + -D MULTI_THREAD=OFF + +to `cmake` when creating Lean's makefiles. This option is simple, but +Lean is use only one core of your system. Another option is to +install Boost and provide the option + + -D BOOST=ON + +to `cmake`. This option forces Lean to use the Boost thread library +instead of the standard one. To install Boost, we should use the following command + + brew install boost --c++11 + +Note that, we have to say we want the C++11 compatible version.