From f73051c6741168f1d847cb0ac71ff8c07158c0a0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Sep 2015 10:40:41 -0700 Subject: [PATCH] fix(CMakeLists.txt): do not generate DLL when using cross-compilation It is not clear why it doesn't work. This is not a big because we do not use cross-compilation anymore to generate the official Lean for Windows. We use MSys2 instead. --- src/CMakeLists.txt | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f71ec8c20..1dbd62f59 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -375,8 +375,13 @@ if ((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Windows")) set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all") endif() add_subdirectory(api) -add_library(leanshared SHARED shared/init.cpp $ ${LEAN_OBJS}) -target_link_libraries(leanshared ${EXTRA_LIBS}) +# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux). +# For some strange reason, it contains a copy of pthread_equal. +# Remark: this problem does not happen when we generate the DLL using msys2 on Windows. +if (NOT("${CROSS_COMPILE}" MATCHES "ON")) + add_library(leanshared SHARED shared/init.cpp $ ${LEAN_OBJS}) + target_link_libraries(leanshared ${EXTRA_LIBS}) +endif() add_subdirectory(shell) add_subdirectory(emacs) @@ -389,7 +394,11 @@ add_subdirectory(tests/library) add_subdirectory(tests/library/blast) add_subdirectory(tests/frontends/lean) add_subdirectory(tests/shell) -add_subdirectory(tests/shared) +# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux). +# For some strange reason, it contains a copy of pthread_equal. +if (NOT("${CROSS_COMPILE}" MATCHES "ON")) + add_subdirectory(tests/shared) +endif() # Include style check if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))