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

doc(cmake/osx10.8): add note regarding multi-thread support on OSX

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-07 12:43:27 -07:00
parent a42856c1d2
commit 60a1ac3192
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
doc/make/osx-10.8.md
View file

@ -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 Instructions for installing clang-3.3 (C++11 compatible) on OS X 10.8
brew install llvm --with-clang --with-asan 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.