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

fix: use correct shared library directory for Lake plugin on Windows (#13128)

Browse source 
This PR fixes the Windows dev build by using
`CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` instead of the hardcoded
`lib/lean` path for the Lake plugin. On Windows, DLLs must be placed
next to executables in `bin/`, but the plugin path was hardcoded to
`lib/lean`, causing stage0 DLLs to not be found.

The `CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY` variable was introduced
precisely for this purpose — it resolves to `bin` on Windows and
`lib/lean` elsewhere.

Closes #13126

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Kim Morrison 2026-04-01 03:33:58 +11:00 • committed by GitHub
parent 504e099c5d
commit 33c3604b87
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/lakefile.toml.in
View file

@ -77,7 +77,7 @@ globs = ["Lake.*"]
defaultFacets = ["static", "static.export"]
# Load the previous stage's lake native code into lake's build process in order to prevent ABI
# breakages from affecting bootstrapping.
moreLeanArgs = ["--plugin", "${PREV_STAGE}/lib/lean/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
moreLeanArgs = ["--plugin", "${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}"]
[[lean_lib]]
name = "LakeMain"