can't find "libleanshared_1.dll" to execute lean executable

Stream: lean4

[Zhong TengXun]

lake exe can run the program while directly run the exe in .lake\build\bin cannot, which shows something like the title.

[Sebastian Ullrich]

Dynamic linking is not the standard build type of Lean, nor is running the executables directly. If you want both for e.g. deployment, you'll need to copy the required DLLs from the toolchain's bin folder to the executable location.

[Zhong TengXun]

thanks