Error loading library 126 when building

Stream: lean4

[Yicheng Qian]

I'm having problem when compiling lean code.
After cloning the latest version of https://github.com/abentkamp/duper, I ran lake build in the folder and lean raised an error

libc++abi: terminating <...>lean::exception: error loading library Duper-Util-Misc.dll: 126
error: external command `<...\lean.exe>` exited with code 3221226505

What should I do to make it work?
The complete error message:

stderr:
info: Building Duper.Clause
error: > LEAN_PATH=.\lean_packages\std\build\lib;.\build\lib <...>\lean.exe .\.\.\Duper\Clause.lean -R .\.\. -o .\build\lib\Duper\Clause.olean -i .\build\lib\Duper\Clause.ilean -c .\build\ir\Duper\Clause.c --load-dynlib=Duper-Util-Misc.dll --load-dynlib=Duper-Expr.dll --load-dynlib=Duper-Order.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Duper-Util-Misc.dll: 126
error: external command `c:\Users\yiche\.elan\toolchains\leanprover--lean4---nightly-2022-11-19\bin\lean.exe` exited with code 3221226505

[Yicheng Qian]

Ah. I've tried WSL, and it compiled successfully. However I just can't get it to compile on Windows.

[Sebastian Ullrich]

@Mac 126 is ERROR_MOD_NOT_FOUND, so the PATH may not be correctly set up. Unfortunately, the error message doesn't tell us whether the mentioned DLL or any of its dependencies was not found.

[Mac]

@Sebastian Ullrich Yeah the problem is that augmented PATH environment variable does not properly forward to the worker processes on Windows. This is a relatively recent phenomenon that I think may be related to the changes in lean4#1759. However, I have a fix in the works which should solve this regardless. This plan is deploy it with the v4.1.0 release by the end of the month.

[Utensil Song]

This is an old thread, but the closest I can find that's like the errors I'm facing. I'm trying to make FFI to a third-party library work on Windows CI (which already works on Mac and Ubuntu CI) with this lakefile, the library .a and .dll compiled, linked successfully, the FFI .dll compiled and linked successfully, but I have this final error 126:

✔ [6/17] Built GinacLean/libginac_ffi
✖ [7/17] Building Ginac.Symbol
trace: .> LEAN_PATH=.\.\.lake\build\lib PATH c:\Users\runneradmin\.elan\toolchains\leanprover--lean4---v4.8.0\bin\lean.exe --load-dynlib=.\.\.lake\build\lib\cln.dll --load-dynlib=.\.\.lake\build\lib\ginac.dll .\.\lean\.\Ginac\Symbol.lean -R .\.\lean\. -o .\.\.lake\build\lib\Ginac\Symbol.olean -i .\.\.lake\build\lib\Ginac\Symbol.ilean -c .\.\.lake\build\ir\Ginac\Symbol.c --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library .\.\.lake\build\lib\ginac.dll: 126
error: Lean exited with code 3221226505
Some builds logged failures:
- Ginac.Symbol
error: build failed

I can confirm that the DLL with that name is right at that relative path, as I've made sure it's there for the previous linking steps. According to this thread, this could be some environment variable issues, also as indicated by the empty PATH before the lean.exe. But previous issues are supposed to be fixed, and I can't figure out what I can do to help the situation from the lakefile.

@Mac Malone Do you have some idea? Thanks!

[Utensil Song]

Well, lake env lake build to the rescue again. CI green. :joy: