From 425bebe99ecb69bf0859dee5eb08f440d4e99fcb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 26 Aug 2025 18:01:57 +0200 Subject: [PATCH] chore: further split `libleanshared` on Windows to avoid symbol limit (#10136) Co-authored-by: Markus Himmel --- src/CMakeLists.txt | 8 ++++--- src/lake/examples/reverse-ffi/Makefile | 4 ++-- src/lean.mk.in | 2 +- src/stdlib.make.in | 31 ++++++++++++++++++------- stage0/src/CMakeLists.txt | Bin 39267 -> 39484 bytes stage0/src/stdlib.make.in | Bin 9413 -> 11084 bytes tests/compiler/foreign/Makefile | 2 +- 7 files changed, 31 insertions(+), 16 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 697bd78dd3..b9c33905bc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -469,6 +469,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib") + string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib") string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib") string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib") string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean") @@ -502,7 +503,7 @@ endif() # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH. if(${CMAKE_SYSTEM_NAME} MATCHES "Windows") # import libraries created by the stdlib.make targets - string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared") + string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared") elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") # The second flag is necessary to even *load* dylibs without resolved symbols, as can happen # if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even @@ -589,7 +590,7 @@ endif() add_subdirectory(initialize) add_subdirectory(shell) -# to be included in `leanshared` but not the smaller `leanshared_1` (as it would pull +# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull # in the world) add_library(leaninitialize STATIC $) set_target_properties(leaninitialize PROPERTIES @@ -714,6 +715,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") ) add_custom_target(leanshared ALL DEPENDS Init_shared leancpp + COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ) @@ -734,7 +736,7 @@ else() COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared VERBATIM) - string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared") endif() if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") diff --git a/src/lake/examples/reverse-ffi/Makefile b/src/lake/examples/reverse-ffi/Makefile index 67e4d53832..63e367cf9d 100644 --- a/src/lake/examples/reverse-ffi/Makefile +++ b/src/lake/examples/reverse-ffi/Makefile @@ -23,7 +23,7 @@ endif $(OUT_DIR)/main: main.c lake | $(OUT_DIR) # Add library paths for Lake package and for Lean itself - cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lInit_shared -lleanshared_1 -lleanshared $(LINK_FLAGS) + cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS) run: $(OUT_DIR)/main ifeq ($(OS),Windows_NT) @@ -55,7 +55,7 @@ endif $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR) cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR) - cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lInit_shared -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL) + cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL) run-local: $(OUT_DIR)/main-local $(OUT_DIR)/main-local diff --git a/src/lean.mk.in b/src/lean.mk.in index 4c979f1331..131a73a48a 100644 --- a/src/lean.mk.in +++ b/src/lean.mk.in @@ -145,7 +145,7 @@ $(LIB_OUT)/$(STATIC_LIB_NAME).export: $(addsuffix .export,$(NAT_OBJS)) | $(LIB_O $(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O")) # "T"hin archive seems necessary to preserve paths so that we can distinguish # between object files with the same file name when manipulating the archive for - # `libleanshared_1` + # `libleanshared_*` @$(LEAN_AR) rcsT $@ @$@.in @rm -f $@.in else diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 920ca6397d..6e4d97af09 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -97,23 +97,36 @@ ifeq "${CMAKE_SYSTEM_NAME}" "Windows" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} @rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} -# "half-way point" DLL to avoid symbol limit -# include Lean.Meta.WHNF and leancpp except for `initialize.cpp` + @rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} +# initial DLL to avoid symbol limit: include leancpp except for `initialize.cpp` "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} \ - ${LIB}/temp/Lean/Meta/WHNF.*o.export -Wl,--start-group ${LIB}/lean/libLean.a.export -Wl,--whole-archive ${LIB}/temp/libleancpp_1.a -Wl,--no-whole-archive -Wl,--end-group -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared_1.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} -Wl,-Map=${LIB}/temp/libleanshared_1.map + -Wl,--start-group ${LIB}/lean/libLean.a.export -Wl,--whole-archive ${LIB}/temp/libleancpp_1.a -Wl,--no-whole-archive -Wl,--end-group -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared_1.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} -Wl,-Map=${LIB}/temp/libleanshared_1.map + echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: " + nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l # now delete included symbols from libLean.a cp ${LIB}/lean/libLean.a.export ${LIB}/lean/diff.a sed -En 's/.*\s(\S*\.o\.export):.*/\1/p' ${LIB}/temp/libleanshared_1.map > ${LIB}/temp/diff.a.in # can't use bundled llvm-ar before LLVM 16, https://github.com/llvm/llvm-project/issues/55023 ar dP ${LIB}/lean/diff.a @${LIB}/temp/diff.a.in - "${CMAKE_AR}" tP ${LIB}/lean/diff.a -# now include Lean and the diff library in `leanshared` + #"${CMAKE_AR}" tP ${LIB}/lean/diff.a +# now again up to `Lean.Meta` + "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} \ + ${LIB}/lean/../temp/Lean/Meta.*o.export ${LIB}/lean/diff.a -Wl,--no-whole-archive -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared_2.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} -Wl,-Map=${LIB}/temp/libleanshared_2.map + echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: " + nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l + sed -En 's/.*\s(\S*\.o\.export):.*/\1/p' ${LIB}/temp/libleanshared_2.map > ${LIB}/temp/diff.a.in + ar dP ${LIB}/lean/diff.a @${LIB}/temp/diff.a.in + #"${CMAKE_AR}" tP ${LIB}/lean/diff.a +# now include `Lean` and the diff library in `leanshared` "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ - -Wl,--whole-archive ${LIB}/lean/diff.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a -Wl,--no-whole-archive -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} + -Wl,--whole-archive ${LIB}/lean/diff.a ${LIB}/temp/libleanshell.a ${LIB}/temp/libleaninitialize.a -Wl,--no-whole-archive -lleanshared_2 -lleanshared_1 -lInit_shared -Wl,--out-implib,${LIB}/lean/libleanshared.dll.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} + echo -n "${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} symbols: " + nm ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} --extern-only | wc -l rm ${LIB}/lean/diff.a else # 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 ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/empty.c ${LEANSHARED_1_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} + "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/empty.c ${LEANSHARED_2_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} ifeq "${CMAKE_SYSTEM_NAME}" "Darwin" "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ ${LIB}/temp/Lean.*o.export -Wl,-force_load,${LIB}/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS} ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} @@ -125,12 +138,12 @@ endif leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} -${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a.export ${LIB}/lean/libLake.a.export +${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a.export ${LIB}/lean/libLake.a.export @echo "[ ] Building $@" # on Windows, must remove file before writing a new one (since the old one may be in use) @rm -f ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX} "${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ \ - ${LAKESHARED_LINKER_FLAGS} -lleanshared -lleanshared_1 -lInit_shared ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} + ${LAKESHARED_LINKER_FLAGS} -lleanshared -lleanshared_2 -lleanshared_1 -lInit_shared ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS} libLake_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX} @@ -142,7 +155,7 @@ ${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX}: ${LIB}/temp/LakeMain.*o. lake: ${CMAKE_BINARY_DIR}/bin/lake${CMAKE_EXECUTABLE_SUFFIX} -${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libleanmain.a +${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX} ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libleanmain.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 697bd78dd3fe5ba703b661f467e397416853fcf2..b9c33905bc6fec642be6b29e693aae8a0437a7bb 100644 GIT binary patch delta 81 zcmaF7iD}OkrVXdU7>y=Ng=tKl6~+x@^@mGN3TBz?;U+#=J4_rX$hG-*mTn+&-v*c{?7PB{m8UvGuUJ|o% GhsqKL&lFq$ diff --git a/stage0/src/stdlib.make.in b/stage0/src/stdlib.make.in index 920ca6397d2a1bedd0415c05e4fc728b0d80afaa..6e4d97af09b30cb3718c59be22e690e81aa6c4d1 100644 GIT binary patch delta 490 zcmX@=c_wVbHNnYsf)nJN^=4F;-Cgv!(`1mN4x5m zWaeg;SOJwJ=aiy1y7{G$B_kJSYH~)tf^MFI(qu!$06vK7Vk-qDF3!B%$qyCO zCi6*Xi|Xp8R+OX`<>}_<+9+1m!#$v=z|pLgB0m$~5aiB;pE`KOrJJ*;&*G z?06$Ku!9pOuNJ)zl&TS%g%l=@ihkH_;hMZbQ69S;n?=N187E&9)q#3_gQE6iR|!#| z+3%$6HqVqe#SCO_P*mJ(D#OhLwoz_#fSe#ybh4?;;>ivYtdnB}*f&2?e9Qy@7MPs* delta 183 zcmX>TcGPpjH9=2h1*MF{oHX6?#7c#N{LH)(B?T8BABB>9g~YP_%oK&<%G{*<9EF_B z+{_X#WrfVVg~Ys+$x%W}C(DYn%a)|(7U+ZI^+EFb zAbCBle7)3)g8ZVA&Hsd~7&o(v1~X2M7So!1K$3$6q;&E*$@`P{NcC(MmT6|(Tqt*n dd2_eYUB<~Z;sTr7RRozQcPo`{j@5Y21OOP`K+OOE diff --git a/tests/compiler/foreign/Makefile b/tests/compiler/foreign/Makefile index 9509698cdc..37099b60fa 100644 --- a/tests/compiler/foreign/Makefile +++ b/tests/compiler/foreign/Makefile @@ -27,7 +27,7 @@ $(BIN_OUT)/testcpp.so: $(CPP_OBJS) | $(BIN_OUT) $(CXX) -shared -o $@ $^ `leanc -shared --print-ldflags` $(BIN_OUT)/test: $(LIB_OUT)/libMain.a $(CPP_OBJS) | $(BIN_OUT) - $(CXX) -o $@ $^ `leanc -shared --print-ldflags` -lInit_shared -lleanshared_1 -lleanshared $(TEST_SHARED_LINK_FLAGS) + $(CXX) -o $@ $^ `leanc -shared --print-ldflags` -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(TEST_SHARED_LINK_FLAGS) run_test: $(BIN_OUT)/test $^