From 55d09a39b431d2f2ba948ba1cd76388a9c68a221 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 6 Jul 2024 11:43:09 +0200 Subject: [PATCH] fix: move Std from libleanshared to much smaller libInit_shared (#4661) Fixes the Windows build. As libLean is by far the biggest component, there is no need for a separate libStd_shared for now. ``` $ find build/release/stage1/lib/lean -name '*.a' -exec bash -c 'echo -n "{} " ; nm {} | grep " T " | wc -l' \; build/release/stage1/lib/lean/libleanrt.a 497 build/release/stage1/lib/lean/libleancpp.a 1320 build/release/stage1/lib/lean/libInit.a 7476 build/release/stage1/lib/lean/libStd.a 1696 build/release/stage1/lib/lean/libLean.a 64339 build/release/stage1/lib/lean/libLake.a 5722 ``` --- src/CMakeLists.txt | 4 ++-- src/stdlib.make.in | 4 ++-- stage0/src/CMakeLists.txt | 4 ++-- stage0/src/stdlib.make.in | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d61af9c449..ce38bcf3bd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -510,13 +510,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) # set up libInit_shared only on Windows; see also stdlib.make.in if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a") + set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") + set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") else() set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") endif() diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 063cbe714f..959bca8240 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -51,7 +51,7 @@ ${LIB}/temp/empty.c: # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt # we specify the precise file names here to avoid rebuilds -${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c +${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${LIB}/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c ifeq "${INIT_SHARED_LINKER_FLAGS}" "" # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} @@ -64,7 +64,7 @@ endif Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} -${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libStd.a.export ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a +${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f $@ diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index d61af9c449..ce38bcf3bd 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -510,13 +510,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib) # set up libInit_shared only on Windows; see also stdlib.make.in if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a") + set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a") endif() if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libStd.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows") - set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libStd.a.export ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") + set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a") else() set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lStd -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}") endif() diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in index 063cbe714f..959bca8240 100644 --- a/stage0/src/stdlib.make.in +++ b/stage0/src/stdlib.make.in @@ -51,7 +51,7 @@ ${LIB}/temp/empty.c: # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt # we specify the precise file names here to avoid rebuilds -${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c +${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${LIB}/temp/libStd.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c ifeq "${INIT_SHARED_LINKER_FLAGS}" "" # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} @@ -64,7 +64,7 @@ endif Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} -${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libStd.a.export ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a +${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f $@