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

feat(build): add 'CROSS_COMPILE' cmake option

Browse source 
When CROSS_COMPILE=ON, the Lean standard library will not be compiled.
This commit is contained in:
Leonardo de Moura 2014-09-26 09:26:40 -07:00
parent f49a610995
commit 8143b51c7e
2 changed files with 14 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.travis.windows.yml
View file

@ -24,7 +24,7 @@ script:
- mkdir -p build - mkdir -p build
- LEAN_ROOT=`pwd` - LEAN_ROOT=`pwd`
- cd build - cd build
- cmake -DIGNORE_SORRY=ON -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} ../src -DTCMALLOC=OFF -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake - cmake -DCROSS_COMPILE=ON -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} ../src -DTCMALLOC=OFF -DCMAKE_TOOLCHAIN_FILE=/tmp/mxe/usr/x86_64-w64-mingw32/share/cmake/mxe-conf.cmake
- SITE=Windows@Travis - SITE=Windows@Travis
- if [[ $CMAKE_BUILD_TYPE == RELEASE ]]; then - if [[ $CMAKE_BUILD_TYPE == RELEASE ]]; then
BUILD_TYPE=Release; BUILD_TYPE=Release;

20
src/CMakeLists.txt
View file

@ -24,6 +24,9 @@ option(JEMALLOC "JEMALLOC" OFF)
# a version of Lean that does not report when 'sorry' is used. # a version of Lean that does not report when 'sorry' is used.
# This is useful for suppressing warning messages in the nightly builds. # This is useful for suppressing warning messages in the nightly builds.
option(IGNORE_SORRY "IGNORE_SORRY" OFF) option(IGNORE_SORRY "IGNORE_SORRY" OFF)
# When cross-compiling, we do not compile the standard library since
# the executable will not work on the host machine
option(CROSS_COMPILE "CROSS_COMPILE" OFF)
# Added for CTest # Added for CTest
include(CTest) include(CTest)
@ -322,13 +325,16 @@ if(NOT DEFINED PROCESSOR_COUNT)
endif() endif()
endif() endif()
# Only build libraries if we are NOT cross compiling if("${CROSS_COMPILE}" MATCHES "ON")
add_custom_target( message(STATUS "Lean standard library will not be compiled when using cross-compilation.")
standard_lib ALL else()
COMMAND python ${LEAN_SOURCE_DIR}/../bin/linja add_custom_target(
DEPENDS ${CMAKE_BINARY_DIR}/shell/lean standard_lib ALL
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library COMMAND python ${LEAN_SOURCE_DIR}/../bin/linja
) DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library
)
endif()
add_custom_target(clean-olean add_custom_target(clean-olean
WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library