chore(src/CMakeLists): remove support for optional Boost

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

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
-```

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](<http://en.wikipedia.org/wiki/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`
 

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

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} $<TARGET_OBJECTS:smt2_frontend>)
 add_subdirectory(init)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:init>)
 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")