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.