2013-07-18 09:12:07 -07:00
|
|
|
cmake_minimum_required(VERSION 2.8.7)
|
|
|
|
project(LEAN CXX)
|
|
|
|
set(LEAN_VERSION_MAJOR 0)
|
|
|
|
set(LEAN_VERSION_MINOR 1)
|
2013-07-16 22:11:48 -07:00
|
|
|
|
2013-07-18 09:12:07 -07:00
|
|
|
set(CMAKE_COLOR_MAKEFILE ON)
|
|
|
|
enable_testing()
|
2013-07-16 22:11:48 -07:00
|
|
|
|
2013-09-20 12:31:06 -07:00
|
|
|
option(TRACK_MEMORY_USAGE "TRACK_MEMORY_USAGE" ON)
|
2013-12-09 16:55:13 -08:00
|
|
|
option(MULTI_THREAD "MULTI_THREAD" ON)
|
|
|
|
option(BOOST "BOOST" OFF)
|
2013-12-09 18:02:04 -08:00
|
|
|
option(STATIC "STATIC" OFF)
|
2013-12-09 22:30:54 -08:00
|
|
|
option(SPLIT_STACK "SPLIT_STACK" OFF)
|
2013-12-21 18:57:15 -08:00
|
|
|
option(READLINE "READLINE" OFF)
|
2013-12-09 18:02:04 -08:00
|
|
|
|
2013-09-03 21:55:40 -07:00
|
|
|
# Added for CTest
|
2013-12-22 21:00:32 -08:00
|
|
|
include(CTest)
|
|
|
|
configure_file(${LEAN_SOURCE_DIR}/CTestCustom.cmake.in
|
2013-09-03 21:55:40 -07:00
|
|
|
${LEAN_BINARY_DIR}/CTestCustom.cmake @ONLY)
|
|
|
|
|
2013-08-10 14:15:13 -07:00
|
|
|
set(LEAN_EXTRA_LINKER_FLAGS "")
|
2013-09-03 10:26:12 -07:00
|
|
|
set(LEAN_EXTRA_CXX_FLAGS "")
|
2013-08-10 14:15:13 -07:00
|
|
|
|
2013-08-22 17:46:18 -07:00
|
|
|
# Windows does not support ulimit -s unlimited. So, we reserve a lot of stack space: 100Mb
|
|
|
|
if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
|
|
|
|
message(STATUS "Windows detected")
|
2013-12-01 12:42:32 -08:00
|
|
|
set(LEAN_WIN_STACK_SIZE "104857600")
|
|
|
|
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -Wl,--stack,${LEAN_WIN_STACK_SIZE}")
|
2013-09-03 10:26:12 -07:00
|
|
|
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_DEFAULT_PP_UNICODE=false")
|
2013-12-01 12:42:32 -08:00
|
|
|
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_WINDOWS -D LEAN_WIN_STACK_SIZE=${LEAN_WIN_STACK_SIZE}")
|
2013-11-18 09:52:47 -08:00
|
|
|
endif()
|
|
|
|
|
2013-12-09 14:56:48 -08:00
|
|
|
if("${MULTI_THREAD}" MATCHES "OFF")
|
|
|
|
message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
|
|
|
|
else()
|
|
|
|
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_MULTI_THREAD")
|
2013-10-25 11:50:35 -07:00
|
|
|
endif()
|
|
|
|
|
2013-12-09 18:02:04 -08:00
|
|
|
if("${STATIC}" MATCHES "ON")
|
|
|
|
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -static")
|
|
|
|
message(STATUS "Creating a static executable")
|
|
|
|
endif()
|
|
|
|
|
2013-08-05 17:58:54 -07:00
|
|
|
# Set Module Path
|
|
|
|
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/")
|
|
|
|
|
2013-07-16 22:11:48 -07:00
|
|
|
# Initialize CXXFLAGS.
|
2013-09-19 22:52:52 -07:00
|
|
|
set(CMAKE_CXX_FLAGS "-Wall -Wextra -std=c++11 ${LEAN_EXTRA_CXX_FLAGS}")
|
2013-07-18 11:10:15 -07:00
|
|
|
set(CMAKE_CXX_FLAGS_DEBUG "-g -DLEAN_DEBUG -DLEAN_TRACE")
|
2013-07-16 22:11:48 -07:00
|
|
|
set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG")
|
|
|
|
set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG")
|
|
|
|
set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
|
2013-09-26 20:22:40 -07:00
|
|
|
|
2013-12-09 22:30:54 -08:00
|
|
|
# SPLIT_STACK
|
|
|
|
if ("${SPLIT_STACK}" MATCHES "ON")
|
|
|
|
if ((${CMAKE_SYSTEM_NAME} MATCHES "Linux") AND ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fsplit-stack -D LEAN_USE_SPLIT_STACK")
|
|
|
|
message(STATUS "Using split-stacks")
|
|
|
|
else()
|
|
|
|
message(FATAL_ERROR "Split-stacks are only supported on Linux with g++")
|
|
|
|
endif()
|
|
|
|
endif()
|
|
|
|
|
2013-09-26 20:22:40 -07:00
|
|
|
# Test coverage
|
|
|
|
if("${TESTCOV}" MATCHES "ON")
|
2013-09-26 22:24:24 -07:00
|
|
|
include(CodeCoverage)
|
2013-09-26 20:22:40 -07:00
|
|
|
message(STATUS "Enable test-coverage")
|
2013-09-27 10:23:52 -07:00
|
|
|
set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0 -fprofile-arcs -ftest-coverage --coverage")
|
2013-09-26 22:24:24 -07:00
|
|
|
setup_target_for_coverage(cov ${LEAN_SOURCE_DIR}/../script/run_tests.sh coverage)
|
2013-09-26 20:22:40 -07:00
|
|
|
endif()
|
2013-07-16 22:11:48 -07:00
|
|
|
|
|
|
|
# Compiler-specific C++11 activation.
|
|
|
|
if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
|
|
|
|
execute_process(
|
|
|
|
COMMAND ${CMAKE_CXX_COMPILER} -dumpversion OUTPUT_VARIABLE GCC_VERSION)
|
|
|
|
if (NOT (GCC_VERSION VERSION_GREATER 4.8 OR GCC_VERSION VERSION_EQUAL 4.8))
|
|
|
|
message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.8 or greater.")
|
|
|
|
endif ()
|
|
|
|
elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
|
2013-08-13 00:29:18 -07:00
|
|
|
if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
|
2013-08-12 10:32:07 -07:00
|
|
|
# In OSX, clang requires "-stdlib=libc++" to support C++11
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++")
|
|
|
|
set(LEAN_EXTRA_LINKER_FLAGS "-stdlib=libc++")
|
2013-08-13 00:29:18 -07:00
|
|
|
endif ()
|
2013-07-16 22:11:48 -07:00
|
|
|
else ()
|
|
|
|
message(FATAL_ERROR "Your C++ compiler does not support C++11.")
|
|
|
|
endif ()
|
|
|
|
|
2013-12-09 16:55:13 -08:00
|
|
|
# BOOST
|
|
|
|
if (("${BOOST}" MATCHES "ON") AND ("${MULTI_THREAD}" MATCHES "ON"))
|
|
|
|
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")
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} -lboost_system -lboost_chrono -lboost_atomic -lboost_thread)
|
|
|
|
endif()
|
|
|
|
|
2013-08-05 17:58:54 -07:00
|
|
|
# MPFR
|
2013-08-05 19:16:52 -07:00
|
|
|
find_package(MPFR 3.1.0)
|
2013-10-25 23:35:06 -04:00
|
|
|
include_directories(${MPFR_INCLUDES})
|
2013-08-05 17:58:54 -07:00
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} ${MPFR_LIBRARIES})
|
|
|
|
|
2013-11-05 19:30:36 -05:00
|
|
|
# GMP
|
|
|
|
find_package(GMP 5.0.5)
|
|
|
|
include_directories(${GMP_INCLUDE_DIR})
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
|
|
|
|
|
2013-09-20 12:31:06 -07:00
|
|
|
# TRACK_MEMORY_USAGE
|
|
|
|
if("${TRACK_MEMORY_USAGE}" MATCHES "ON")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_TRACK_MEMORY")
|
|
|
|
endif()
|
|
|
|
|
2013-07-19 10:04:00 -07:00
|
|
|
# tcmalloc
|
2013-08-21 19:08:34 -07:00
|
|
|
option(TCMALLOC "TCMALLOC" ON)
|
|
|
|
if("${TCMALLOC}" MATCHES "ON")
|
2013-09-19 23:52:50 -07:00
|
|
|
find_package(Tcmalloc)
|
2013-07-20 14:19:36 -07:00
|
|
|
if(${TCMALLOC_FOUND})
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
|
2013-09-19 23:36:57 -07:00
|
|
|
message(STATUS "Using tcmalloc.")
|
2013-09-20 12:31:06 -07:00
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D HAS_TCMALLOC")
|
2013-09-19 23:36:57 -07:00
|
|
|
else()
|
|
|
|
message(WARNING "FAILED to find tcmalloc, using standard malloc.")
|
2013-07-20 14:19:36 -07:00
|
|
|
endif()
|
|
|
|
else()
|
2013-08-12 15:37:36 -07:00
|
|
|
message(STATUS "Using standard malloc.")
|
2013-07-18 15:10:31 -07:00
|
|
|
endif()
|
|
|
|
|
2013-08-21 19:08:34 -07:00
|
|
|
# Readline
|
|
|
|
if("${READLINE}" MATCHES "ON")
|
|
|
|
find_package(Readline)
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} ${READLINE_LIBRARY})
|
|
|
|
message(STATUS "Using GNU readline")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DLEAN_USE_READLINE")
|
|
|
|
endif()
|
|
|
|
|
2013-09-20 12:31:06 -07:00
|
|
|
# Check malloc_usable_size
|
|
|
|
if(NOT "${TCMALLOC_FOUND}" AND "${TRACK_MEMORY_USAGE}" MATCHES "ON")
|
|
|
|
find_package(MallocUsableSize)
|
2013-09-20 14:12:11 -07:00
|
|
|
if("${MUS_FOUND}" MATCHES "TRUE")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${MALLOC_DIR} -D HAS_MALLOC_USABLE_SIZE")
|
|
|
|
else()
|
2013-09-20 17:45:50 -07:00
|
|
|
find_package(MallocSize)
|
|
|
|
if("${MALLOCSIZE_FOUND}" MATCHES "TRUE")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${MALLOC_DIR} -D HAS_MALLOCSIZE")
|
|
|
|
else()
|
|
|
|
find_package(MSize)
|
|
|
|
if("${MSIZE_FOUND}" MATCHES "TRUE")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${MALLOC_DIR} -D HAS_MSIZE")
|
|
|
|
endif()
|
2013-09-20 14:12:11 -07:00
|
|
|
endif()
|
|
|
|
endif()
|
2013-09-20 12:31:06 -07:00
|
|
|
endif()
|
|
|
|
|
2013-12-25 16:18:51 -08:00
|
|
|
# Lua
|
2013-11-08 10:56:29 -08:00
|
|
|
find_package(Lua REQUIRED)
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} ${LUA_LIBRARIES})
|
2013-11-13 18:44:01 -08:00
|
|
|
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
|
|
|
|
# Lua static library for linux depends on dl.so
|
|
|
|
set(EXTRA_LIBS ${EXTRA_LIBS} -ldl)
|
|
|
|
endif()
|
2013-11-08 10:56:29 -08:00
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -I ${LUA_INCLUDE_DIR}")
|
|
|
|
if ("${HAS_LUA_NEWSTATE}$" MATCHES "TRUE")
|
|
|
|
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -D LEAN_USE_LUA_NEWSTATE")
|
|
|
|
endif()
|
2013-11-02 11:16:30 -07:00
|
|
|
|
2013-12-13 19:52:40 -05:00
|
|
|
IF(${CMAKE_SYSTEM_NAME} MATCHES "Darwin" AND ${LUA_FOUND} AND
|
|
|
|
"${LUA_INCLUDE_DIR}" MATCHES "jit")
|
|
|
|
# http://luajit.org/install.html
|
|
|
|
# If you're building a 64 bit application on OSX which links
|
|
|
|
# directly or indirectly against LuaJIT, you need to link your main
|
|
|
|
# executable with these flags:
|
|
|
|
set(LEAN_EXTRA_LINKER_FLAGS "${LEAN_EXTRA_LINKER_FLAGS} -pagezero_size 10000 -image_base 100000000")
|
|
|
|
ENDIF()
|
|
|
|
|
2013-12-25 16:18:51 -08:00
|
|
|
# CPack
|
|
|
|
set(CPACK_PACKAGE_NAME lean)
|
|
|
|
string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME)
|
|
|
|
set(CPACK_PACKAGE_FILE_NAME "lean-${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}-${LOWER_SYSTEM_NAME}")
|
|
|
|
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
|
|
|
|
SET(CPACK_GENERATOR TGZ)
|
|
|
|
else()
|
|
|
|
SET(CPACK_GENERATOR ZIP)
|
|
|
|
endif()
|
|
|
|
include(CPack)
|
|
|
|
|
|
|
|
# Examples
|
|
|
|
file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/../examples/lean/*.lean")
|
|
|
|
FOREACH(FILE ${LEANLIB})
|
|
|
|
install_files(/examples/lean FILES ${FILE})
|
|
|
|
ENDFOREACH(FILE)
|
2013-07-19 10:04:00 -07:00
|
|
|
|
2013-12-25 16:18:51 -08:00
|
|
|
include_directories(${LEAN_SOURCE_DIR})
|
2013-12-04 11:21:26 -08:00
|
|
|
|
2013-07-16 22:10:18 -07:00
|
|
|
add_subdirectory(util)
|
2013-08-10 14:15:13 -07:00
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} util)
|
2013-07-24 14:53:45 -07:00
|
|
|
add_subdirectory(util/numerics)
|
2013-08-10 14:15:13 -07:00
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} numerics)
|
2013-08-13 03:40:51 -07:00
|
|
|
add_subdirectory(util/sexpr)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} sexpr)
|
2013-09-17 14:10:53 -07:00
|
|
|
add_subdirectory(util/interval)
|
2013-08-10 14:15:13 -07:00
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} interval)
|
2013-07-22 04:03:46 -07:00
|
|
|
add_subdirectory(kernel)
|
2013-08-10 14:15:13 -07:00
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} kernel)
|
2013-08-22 10:26:52 -07:00
|
|
|
add_subdirectory(library)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} library)
|
2013-09-06 23:17:24 -07:00
|
|
|
add_subdirectory(library/arith)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} arithlib)
|
2013-09-13 09:06:46 -07:00
|
|
|
add_subdirectory(library/all)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} alllib)
|
2013-09-25 15:38:16 -07:00
|
|
|
add_subdirectory(library/rewriter)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} rewriter)
|
2013-10-03 15:02:07 -07:00
|
|
|
add_subdirectory(library/elaborator)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} elaborator)
|
2013-11-20 17:02:41 -08:00
|
|
|
add_subdirectory(library/tactic)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} tactic)
|
2013-11-07 13:56:04 -08:00
|
|
|
add_subdirectory(frontends/lean)
|
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
|
2013-11-26 19:30:01 -08:00
|
|
|
add_subdirectory(frontends/lua)
|
2013-11-26 19:15:49 -08:00
|
|
|
set(LEAN_LIBS ${LEAN_LIBS} leanlua)
|
2013-12-25 16:18:51 -08:00
|
|
|
add_subdirectory(extra)
|
2013-12-09 14:56:48 -08:00
|
|
|
if("${MULTI_THREAD}" MATCHES "ON")
|
|
|
|
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
|
|
|
|
else()
|
|
|
|
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
|
|
|
|
endif()
|
2013-08-17 20:37:10 -07:00
|
|
|
set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
|
2013-08-10 14:15:13 -07:00
|
|
|
set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
|
2013-07-16 22:10:18 -07:00
|
|
|
add_subdirectory(shell)
|
2013-12-22 21:00:32 -08:00
|
|
|
|
2013-07-19 19:12:55 -07:00
|
|
|
add_subdirectory(tests/util)
|
2013-07-24 14:53:45 -07:00
|
|
|
add_subdirectory(tests/util/numerics)
|
2013-10-21 18:17:34 -07:00
|
|
|
add_subdirectory(tests/util/interval)
|
2013-07-22 04:03:46 -07:00
|
|
|
add_subdirectory(tests/kernel)
|
2013-08-23 09:35:35 -07:00
|
|
|
add_subdirectory(tests/library)
|
2013-09-25 15:38:16 -07:00
|
|
|
add_subdirectory(tests/library/rewriter)
|
2013-11-20 17:02:41 -08:00
|
|
|
add_subdirectory(tests/library/tactic)
|
2013-10-14 08:16:23 -07:00
|
|
|
add_subdirectory(tests/library/elaborator)
|
2013-08-21 09:04:49 -07:00
|
|
|
add_subdirectory(tests/frontends/lean)
|
2013-09-13 19:15:38 -07:00
|
|
|
|
|
|
|
# Include style check
|
|
|
|
include(StyleCheck)
|
|
|
|
file(GLOB_RECURSE LEAN_SOURCES
|
2013-09-13 20:00:55 -07:00
|
|
|
${LEAN_SOURCE_DIR}
|
2013-09-16 16:23:20 -07:00
|
|
|
${LEAN_SOURCE_DIR}/[A-Za-z]*.cpp
|
|
|
|
${LEAN_SOURCE_DIR}/[A-Za-z]*.h)
|
2013-09-13 19:15:38 -07:00
|
|
|
add_style_check_target(style "${LEAN_SOURCES}")
|
2013-09-26 22:24:24 -07:00
|
|
|
add_test(NAME style_check COMMAND ${LEAN_SOURCE_DIR}/cmake/Modules/cpplint.py ${LEAN_SOURCES})
|