max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: rm new shared libs before build for Windows (#5541)

Browse source 
On Windows, shared libraries must be removed before linking. Otherwise,
linking can fail with "Permission denied" when the libraries are in use.
This ensures such removal is done for the new `libLake_shared.dll` and
both parts of `libleanshared`.
This commit is contained in:
Mac Malone 2024-10-02 00:06:03 -04:00 • committed by GitHub
parent 9322d8d639
commit 952c086a92
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/stdlib.make.in
View file

@ -70,6 +70,7 @@ ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: $
@echo "[ ] Building $@"
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`
@ -104,6 +105,8 @@ Lake:
${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}/temp/libLean.a.export ${LIB}/temp/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}