From 8143b51c7ee66ef5b1751caa9e610bb0bdb99fad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Sep 2014 09:26:40 -0700
Subject: [PATCH] feat(build): add 'CROSS_COMPILE' cmake option

When CROSS_COMPILE=ON, the Lean standard library will not be compiled.
---
 .travis.windows.yml |  2 +-
 src/CMakeLists.txt  | 20 +++++++++++++-------
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/.travis.windows.yml b/.travis.windows.yml
index aafd3e3cb..e0b989b19 100644
--- a/.travis.windows.yml
+++ b/.travis.windows.yml
@@ -24,7 +24,7 @@ script:
   - mkdir -p build
   - LEAN_ROOT=`pwd`
   - 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
   - if [[ $CMAKE_BUILD_TYPE == RELEASE ]]; then
         BUILD_TYPE=Release;
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f78b81f11..c2a4778ff 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -24,6 +24,9 @@ option(JEMALLOC           "JEMALLOC"           OFF)
 # a version of Lean that does not report when 'sorry' is used.
 # This is useful for suppressing warning messages in the nightly builds.
 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
 include(CTest)
@@ -322,13 +325,16 @@ if(NOT DEFINED PROCESSOR_COUNT)
   endif()
 endif()
 
-# Only build libraries if we are NOT cross compiling
-add_custom_target(
-  standard_lib ALL
-  COMMAND python ${LEAN_SOURCE_DIR}/../bin/linja
-  DEPENDS ${CMAKE_BINARY_DIR}/shell/lean
-  WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library
-  )
+if("${CROSS_COMPILE}" MATCHES "ON")
+  message(STATUS "Lean standard library will not be compiled when using cross-compilation.")
+else()
+  add_custom_target(
+    standard_lib ALL
+    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
   WORKING_DIRECTORY ${LEAN_SOURCE_DIR}/../library