Skip to content

Commit

Permalink
fix: rm new shared libs before build for Windows (#5541)
Browse files Browse the repository at this point in the history
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`.
  • Loading branch information
tydeu authored Oct 2, 2024
1 parent 9322d8d commit 952c086
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/stdlib.make.in
Original file line number Diff line number Diff line change
Expand Up @@ -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`
Expand Down Expand Up @@ -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}

Expand Down

0 comments on commit 952c086

Please sign in to comment.