diff --git a/README.md b/README.md index 1574dd0ef8..d4626287d5 100644 --- a/README.md +++ b/README.md @@ -31,9 +31,6 @@ Requirements - [GMP (GNU multiprecision library)](http://gmplib.org/) - [MPFR (GNU MPFR Library)](http://www.mpfr.org/) - (optional) [gperftools](https://code.google.com/p/gperftools/) -- (optional) [Boost](http://www.boost.org) (version >= 1.54), we can - build Lean using boost::thread instead of std::thread. When using - Boost, Lean can modify the thread stack size. Installing required packages at -------------------------------- diff --git a/doc/make/msys2.md b/doc/make/msys2.md index f98eb72e98..e50570e3b3 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.md @@ -33,22 +33,3 @@ mkdir build && cd build cmake ../src -G Ninja -D CMAKE_BUILD_TYPE=Release ninja ``` - -## Build Lean using Boost - -To install Boost in the [msys2] shell, use the following command: - -```bash -pacman -S mingw-w64-x86_64-boost -``` - -In the [msys2] shell, execute the following commands. - -```bash -cd /c/ -git clone https://github.com/leanprover/lean -cd lean -mkdir build && cd build -cmake -D CMAKE_CXX_COMPILER=g++.exe -D BOOST=ON -G Ninja ../src -ninja -``` diff --git a/doc/make/split-stack.md b/doc/make/split-stack.md index e39b400bc4..4ce4d25220 100644 --- a/doc/make/split-stack.md +++ b/doc/make/split-stack.md @@ -11,7 +11,7 @@ the program. In principle, it is possible to build a program that uses split-stacks with libraries that do not. However, it did not work in our experiments. To be able to compile Lean with split-stacks, we also have to compile -GMP, MPFR and Lua using split-stacks. +GMP, MPFR using split-stacks. We also had to use the [gold linker](). @@ -23,7 +23,7 @@ can install it by executing sudo apt-get install binutils-gold -Before we compiled GMP, MPFR, Lua, and Lean, we created an alias +Before we compiled GMP, MPFR, and Lean, we created an alias alias ld=ld.gold @@ -62,25 +62,6 @@ Make sure MPFR does not produce any warning/error message. Then, build and insta We should have the file `libmpfr.a` at `$HOME/tools/split-stack/lib`. -Compiling Lua using split-stacks --------------------------------- - -Download Lua from [http://www.lua.org/](http://www.lua.org/); uncompress the Lua tar-ball at `$HOME/tools`. -Then, modify the following line in the file `src/Makefile` in the Lua directory. - - CFLAGS= -O2 -Wall -DLUA_COMPAT_ALL $(SYSCFLAGS) $(MYCFLAGS) - -We should include the option `-fsplit-stack` - - CFLAGS= -O2 -fsplit-stack -Wall -DLUA_COMPAT_ALL $(SYSCFLAGS) $(MYCFLAGS) - -Then, build and install using - - make linux - make linux install INSTALL_TOP=$HOME/tools/split-stack - -We should have the file `liblua.a` at `$HOME/tools/split-stack/lib`. - Compiling Lean using split-stacks -------------------------------- @@ -90,7 +71,7 @@ Go to the Lean directory, and create the folder `build/release` Configure Lean using - cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D LUA_LIBRARIES=$HOME/tools/split-stack/lib/liblua.a -D LUA_INCLUDE_DIR=$HOME/tool/split-stack/include -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a -D MPFR_LIBRARIES=$HOME/tools/split-stack/lib/libmpfr.a ../../src + cmake -D CMAKE_BUILD_TYPE=Release -D CMAKE_CXX_COMPILER=g++ -D TCMALLOC=OFF -D GMP_INCLUDE_DIR=$HOME/tools/split-stack/include -D GMP_LIBRARIES=$HOME/tools/split-stack/lib/libgmp.a -D MPFR_LIBRARIES=$HOME/tools/split-stack/lib/libmpfr.a ../../src Remark: if you have ninja build tool installed in your system, you can also provide `-G Ninja` diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md index bf8e8d5a50..22dab16541 100644 --- a/doc/make/ubuntu-12.04-detailed.md +++ b/doc/make/ubuntu-12.04-detailed.md @@ -25,10 +25,6 @@ Preparing working environment on Ubuntu 12.04 sudo apt-get install doxygen sudo apt-get install kcachegrind - sudo add-apt-repository --yes ppa:boost-latest/ppa - sudo apt-get install libboost1.54-dev - sudo apt-get install libboost-thread1.54-dev - ### Fork Lean on github : https://github.com/leanprover/lean ### Create a projects directory @@ -49,14 +45,6 @@ Preparing working environment on Ubuntu 12.04 cmake -D CMAKE_BUILD_TYPE=Debug ../../src make -### Build Lean using Boost - - cd lean - mkdir -p build/release - cd build/release - cmake -D CMAKE_BUILD_TYPE=Release -D BOOST=ON ../../src - make - ### If you are using Emacs, here are some basic configurations (custom-set-variables diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6445689d31..d098ac2755 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -27,7 +27,6 @@ set(CMAKE_COLOR_MAKEFILE ON) enable_testing() option(MULTI_THREAD "MULTI_THREAD" ON) -option(BOOST "BOOST" OFF) option(STATIC "STATIC" OFF) option(SPLIT_STACK "SPLIT_STACK" OFF) option(READLINE "READLINE" OFF) @@ -194,19 +193,6 @@ else() message(FATAL_ERROR "Your C++ compiler does not support C++11.") endif () -# BOOST -if (BOOST AND MULTI_THREAD) - find_package(Boost 1.54 COMPONENTS system thread atomic chrono REQUIRED) - message(STATUS "Boost library will be used to implement multi-threading support") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_BOOST") - include_directories(${Boost_INCLUDE_DIRS}) - set(EXTRA_LIBS ${EXTRA_LIBS} ${Boost_LIBRARIES}) - if (("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - # Hide warnings when using Boost and g++ on OSX - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-local-typedefs -Wno-deprecated-declarations") - endif() -endif() - if (${EMSCRIPTEN}) include(ExternalProject) set(gmp_install_prefix ${CMAKE_CURRENT_BINARY_DIR}/gmp-root) @@ -360,7 +346,7 @@ set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(init) set(LEAN_OBJS ${LEAN_OBJS} $) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}") -if(MULTI_THREAD AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")) AND (NOT BOOST)) +if(MULTI_THREAD AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin"))) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") endif() set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")