error loading library Aesop-Nanos.dll

Stream: lean4

[Sky Wilshaw]

I'm trying to get started again with porting now that I'm back on my windows machine but I'm having real trouble getting aesop to build. I keep getting errors like this when viewing files in mathlib4 that depend on aesop:

`c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lake.exe print-paths Init Mathlib.Data.Rat.Defs Mathlib.Algebra.Order.Ring.Defs` failed:

stderr:
warning: manifest out of date: package directory changed, use `lake update` to update
warning: wanted prebuilt release, but release repository and tag was not known
info: Building Aesop.Constants
info: Building Aesop.Tracing
info: Building Aesop.Util.Basic
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Util\Basic.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Util\Basic.olean -i .\./lake-packages\aesop\build\lib\Aesop\Util\Basic.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Util\Basic.c --load-dynlib=Aesop-Nanos.dll --load-dynlib=Std-Classes-BEq.dll --load-dynlib=Std-Lean-Delaborator.dll --load-dynlib=Std-Tactic-CoeExt.dll --load-dynlib=Std-Util-LibraryNote.dll --load-dynlib=Std-Classes-Cast.dll --load-dynlib=Std-Classes-Dvd.dll --load-dynlib=Std-Tactic-Unreachable.dll --load-dynlib=Std-Linter-UnreachableTactic.dll --load-dynlib=Std-Lean-TagAttribute.dll --load-dynlib=Std-Lean-AttributeExtra.dll --load-dynlib=Std-Linter-UnnecessarySeqFocus.dll --load-dynlib=Std-Linter.dll --load-dynlib=Std-Tactic-OpenPrivate.dll --load-dynlib=Std-Tactic-NoMatch.dll --load-dynlib=Std-Tactic-GuardExpr.dll --load-dynlib=Std-Tactic-ByCases.dll --load-dynlib=Std-Tactic-SeqFocus.dll --load-dynlib=Std-Tactic-TryThis.dll --load-dynlib=Std-Tactic-ShowTerm.dll --load-dynlib=Std-Lean-Parser.dll --load-dynlib=Std-Tactic-SimpTrace.dll --load-dynlib=Std-Lean-Meta-Basic.dll --load-dynlib=Std-Lean-Tactic.dll --load-dynlib=Std-Tactic-Basic.dll --load-dynlib=Std-Util-TermUnsafe.dll --load-dynlib=Std-Lean-NameMapAttribute.dll --load-dynlib=Std-Tactic-Lint-Basic.dll --load-dynlib=Std-Data-List-Init-Lemmas.dll --load-dynlib=Std-Data-Array-Init-Basic.dll --load-dynlib=Std-Data-Array-Basic.dll --load-dynlib=Std-Tactic-Lint-Misc.dll --load-dynlib=Std-Logic.dll --load-dynlib=Std-Classes-LawfulMonad.dll --load-dynlib=Std-Lean-Meta-LCtx.dll --load-dynlib=Std-Tactic-Simpa.dll --load-dynlib=Std-Classes-Order.dll --load-dynlib=Std-Util-ExtendedBinder.dll --load-dynlib=Std-Classes-SetNotation.dll --load-dynlib=Std-Control-ForInStep-Basic.dll --load-dynlib=Std-Control-ForInStep-Lemmas.dll --load-dynlib=Std-Control-ForInStep.dll --load-dynlib=Std-Tactic-HaveI.dll --load-dynlib=Std-Data-Array-Init-Lemmas.dll --load-dynlib=Std-Data-Nat-Basic.dll --load-dynlib=Std-Data-Nat-Lemmas.dll --load-dynlib=Std-Data-Option-Init-Lemmas.dll --load-dynlib=Std-Data-List-Basic.dll --load-dynlib=Std-Data-Option-Basic.dll --load-dynlib=Std-Tactic-RCases.dll --load-dynlib=Std-Lean-Command.dll --load-dynlib=Std-Tactic-Ext-Attr.dll --load-dynlib=Std-Data-Option-Lemmas.dll --load-dynlib=Std-Tactic-Ext.dll --load-dynlib=Std-Data-List-Lemmas.dll --load-dynlib=Std-Data-Array-Lemmas.dll --load-dynlib=Std-Data-AssocList.dll --load-dynlib=Std-Data-BinomialHeap.dll --load-dynlib=Std-Data-Char.dll --load-dynlib=Std-Data-DList.dll --load-dynlib=Std-Data-Fin-Lemmas.dll --load-dynlib=Std-Data-HashMap-Basic.dll --load-dynlib=Std-Data-HashMap-WF.dll --load-dynlib=Std-Data-HashMap.dll --load-dynlib=Std-Data-Int-Basic.dll --load-dynlib=Std-Tactic-NormCast-Ext.dll --load-dynlib=Std-Tactic-NormCast-Lemmas.dll --load-dynlib=Std-Data-Int-Lemmas.dll --load-dynlib=Std-Data-Int-DivMod.dll --load-dynlib=Std-Data-Nat-Gcd.dll --load-dynlib=Std-Data-PairingHeap.dll --load-dynlib=Std-Data-RBMap-Basic.dll --load-dynlib=Std-Data-RBMap-WF.dll --load-dynlib=Std-Data-RBMap.dll --load-dynlib=Std-Data-RBMap-Alter.dll --load-dynlib=Std-Data-RBMap-Lemmas.dll --load-dynlib=Std-Data-Rat-Basic.dll --load-dynlib=Std-Data-Rat-Lemmas.dll --load-dynlib=Std-Data-Rat.dll --load-dynlib=Std-Data-String.dll --load-dynlib=Std-Lean-Expr.dll --load-dynlib=Std-Lean-Meta-AssertHypotheses.dll --load-dynlib=Std-Lean-Meta-Clear.dll --load-dynlib=Std-Lean-Meta-Inaccessible.dll --load-dynlib=Std-Lean-Meta-InstantiateMVars.dll --load-dynlib=Std-Lean-MonadBacktrack.dll --load-dynlib=Std-Lean-Meta-SavedState.dll --load-dynlib=Std-Lean-Meta-UnusedNames.dll --load-dynlib=Std-Tactic-Congr.dll --load-dynlib=Std-Tactic-Lint-Simp.dll --load-dynlib=Std-Tactic-Lint-TypeClass.dll --load-dynlib=Std-Tactic-Lint-Frontend.dll --load-dynlib=Std-Tactic-Lint.dll --load-dynlib=Std-Tactic-SqueezeScope.dll --load-dynlib=Std.dll --load-dynlib=Aesop-Util-UnionFind.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Nanos.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Constants.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Constants.olean -i .\./lake-packages\aesop\build\lib\Aesop\Constants.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Constants.c --load-dynlib=Aesop-Percent.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Percent.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Tracing.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Tracing.olean -i .\./lake-packages\aesop\build\lib\Aesop\Tracing.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Tracing.c --load-dynlib=Aesop-Tracing-Init.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Tracing-Init.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505

Running lake build gives a similar error:

error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Constants.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Constants.olean -i .\./lake-packages\aesop\build\lib\Aesop\Constants.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Constants.c --load-dynlib=Aesop-Percent.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Percent.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505

[Mario Carneiro]

update your lean-toolchain to match mathlib/aesop

[Sky Wilshaw]

Ah, I'm not on master so perhaps the toolchain in this branch is old.

[Mario Carneiro]

you should also try deleting the lake-packages directory, it might be using incompatible build data

[Sky Wilshaw]

I'd also run lake clean, presumably it does the same thing. Currently waiting for it to try building with the lean-toolchain from master, hopefully this works...

[Sky Wilshaw]

Unfortunately this still doesn't work. This error is from CategoryTheory.NatIso (just because it uses aesop) on current master, after a lake clean:

`c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lake.exe print-paths Init Mathlib.CategoryTheory.Functor.Category Mathlib.CategoryTheory.Iso` failed:

stderr:
warning: manifest out of date: package directory changed, use `lake update` to update
warning: wanted prebuilt release, but release repository and tag was not known
info: Building Aesop.Constants
info: Building Aesop.Tracing
info: Building Mathlib.Combinatorics.Quiver.Basic
info: Linking Std.Data.HashMap
info: Linking Std
info: Linking Aesop.Util.UnionFind
info: Building Aesop.Util.Basic
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Tracing.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Tracing.olean -i .\./lake-packages\aesop\build\lib\Aesop\Tracing.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Tracing.c --load-dynlib=Aesop-Tracing-Init.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Tracing-Init.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Constants.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Constants.olean -i .\./lake-packages\aesop\build\lib\Aesop\Constants.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Constants.c --load-dynlib=Aesop-Percent.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Percent.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505
error: > LEAN_PATH=.\build\lib;.\./lake-packages\Qq\build\lib;.\./lake-packages\aesop\build\lib;.\./lake-packages\std\build\lib PATH c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe .\./lake-packages\aesop\.\.\Aesop\Util\Basic.lean -R .\./lake-packages\aesop\.\. -o .\./lake-packages\aesop\build\lib\Aesop\Util\Basic.olean -i .\./lake-packages\aesop\build\lib\Aesop\Util\Basic.ilean -c .\./lake-packages\aesop\build\ir\Aesop\Util\Basic.c --load-dynlib=Aesop-Nanos.dll --load-dynlib=Std-Classes-BEq.dll --load-dynlib=Std-Lean-Delaborator.dll --load-dynlib=Std-Tactic-CoeExt.dll --load-dynlib=Std-Util-LibraryNote.dll --load-dynlib=Std-Classes-Cast.dll --load-dynlib=Std-Classes-Dvd.dll --load-dynlib=Std-Tactic-Unreachable.dll --load-dynlib=Std-Linter-UnreachableTactic.dll --load-dynlib=Std-Lean-TagAttribute.dll --load-dynlib=Std-Lean-AttributeExtra.dll --load-dynlib=Std-Linter-UnnecessarySeqFocus.dll --load-dynlib=Std-Linter.dll --load-dynlib=Std-Tactic-OpenPrivate.dll --load-dynlib=Std-Tactic-NoMatch.dll --load-dynlib=Std-Tactic-GuardExpr.dll --load-dynlib=Std-Tactic-ByCases.dll --load-dynlib=Std-Tactic-SeqFocus.dll --load-dynlib=Std-Tactic-TryThis.dll --load-dynlib=Std-Tactic-ShowTerm.dll --load-dynlib=Std-Lean-Parser.dll --load-dynlib=Std-Tactic-SimpTrace.dll --load-dynlib=Std-Lean-Meta-Basic.dll --load-dynlib=Std-Lean-Tactic.dll --load-dynlib=Std-Tactic-Basic.dll --load-dynlib=Std-Util-TermUnsafe.dll --load-dynlib=Std-Lean-NameMapAttribute.dll --load-dynlib=Std-Tactic-Lint-Basic.dll --load-dynlib=Std-Data-List-Init-Lemmas.dll --load-dynlib=Std-Data-Array-Init-Basic.dll --load-dynlib=Std-Data-Array-Basic.dll --load-dynlib=Std-Tactic-Lint-Misc.dll --load-dynlib=Std-Logic.dll --load-dynlib=Std-Classes-LawfulMonad.dll --load-dynlib=Std-Lean-Meta-LCtx.dll --load-dynlib=Std-Tactic-Simpa.dll --load-dynlib=Std-Classes-Order.dll --load-dynlib=Std-Util-ExtendedBinder.dll --load-dynlib=Std-Classes-SetNotation.dll --load-dynlib=Std-Control-ForInStep-Basic.dll --load-dynlib=Std-Control-ForInStep-Lemmas.dll --load-dynlib=Std-Control-ForInStep.dll --load-dynlib=Std-Tactic-HaveI.dll --load-dynlib=Std-Data-Array-Init-Lemmas.dll --load-dynlib=Std-Data-Nat-Basic.dll --load-dynlib=Std-Data-Nat-Lemmas.dll --load-dynlib=Std-Data-Option-Init-Lemmas.dll --load-dynlib=Std-Data-List-Basic.dll --load-dynlib=Std-Data-Option-Basic.dll --load-dynlib=Std-Tactic-RCases.dll --load-dynlib=Std-Lean-Command.dll --load-dynlib=Std-Tactic-Ext-Attr.dll --load-dynlib=Std-Data-Option-Lemmas.dll --load-dynlib=Std-Tactic-Ext.dll --load-dynlib=Std-Data-List-Lemmas.dll --load-dynlib=Std-Data-Array-Lemmas.dll --load-dynlib=Std-Data-AssocList.dll --load-dynlib=Std-Data-BinomialHeap.dll --load-dynlib=Std-Data-Char.dll --load-dynlib=Std-Data-DList.dll --load-dynlib=Std-Data-Fin-Lemmas.dll --load-dynlib=Std-Data-HashMap-Basic.dll --load-dynlib=Std-Data-HashMap-WF.dll --load-dynlib=Std-Data-HashMap.dll --load-dynlib=Std-Data-Int-Basic.dll --load-dynlib=Std-Tactic-NormCast-Ext.dll --load-dynlib=Std-Tactic-NormCast-Lemmas.dll --load-dynlib=Std-Data-Int-Lemmas.dll --load-dynlib=Std-Data-Int-DivMod.dll --load-dynlib=Std-Data-Nat-Gcd.dll --load-dynlib=Std-Data-PairingHeap.dll --load-dynlib=Std-Data-RBMap-Basic.dll --load-dynlib=Std-Data-RBMap-WF.dll --load-dynlib=Std-Data-RBMap.dll --load-dynlib=Std-Data-RBMap-Alter.dll --load-dynlib=Std-Data-RBMap-Lemmas.dll --load-dynlib=Std-Data-Rat-Basic.dll --load-dynlib=Std-Data-Rat-Lemmas.dll --load-dynlib=Std-Data-Rat.dll --load-dynlib=Std-Data-String.dll --load-dynlib=Std-Lean-Expr.dll --load-dynlib=Std-Lean-Meta-AssertHypotheses.dll --load-dynlib=Std-Lean-Meta-Clear.dll --load-dynlib=Std-Lean-Meta-Inaccessible.dll --load-dynlib=Std-Lean-Meta-InstantiateMVars.dll --load-dynlib=Std-Lean-MonadBacktrack.dll --load-dynlib=Std-Lean-Meta-SavedState.dll --load-dynlib=Std-Lean-Meta-UnusedNames.dll --load-dynlib=Std-Tactic-Congr.dll --load-dynlib=Std-Tactic-Lint-Simp.dll --load-dynlib=Std-Tactic-Lint-TypeClass.dll --load-dynlib=Std-Tactic-Lint-Frontend.dll --load-dynlib=Std-Tactic-Lint.dll --load-dynlib=Std-Tactic-SqueezeScope.dll --load-dynlib=Std.dll --load-dynlib=Aesop-Util-UnionFind.dll
error: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library Aesop-Nanos.dll: 126
error: external command `c:\Users\skywi\.elan\toolchains\leanprover--lean4---nightly-2022-12-13\bin\lean.exe` exited with code 3221226505

[Jannis Limperg]

Someone reported a similar issue in JLimperg/aesop#33. No idea what causes it I'm afraid.

[Sebastian Ullrich]

Also, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Error.20loading.20library.20126.20when.20building

[Sky Wilshaw]

Ah, that's unfortunate. I may be unable to contribute until this bug gets fixed, I'm pretty much stuck working on Windows for now.

[Gabriel Ebner]

Maybe we should disable precompiled modules in aesop for now? (That is, until the bug is fixed.)

[Jannis Limperg]

Gabriel Ebner said:

Maybe we should disable precompiled modules in aesop for now? (That is, until the bug is fixed.)

Good idea, done.

[Sky Wilshaw]

Thank you, I'm now able to compile mathlib!

[Arthur Paulino]

Is this being tracked somewhere? I'd like to follow it :eyes:
I've been hit by this issue when importing a different package

[Sebastian Ullrich]

Please open a Lake issue, I don't there is one yet

[Arthur Paulino]

https://github.com/leanprover/lake/issues/146

[Mac]

So I was debugging this issue and found some interesting behavior. Passing the library name to --load-dynlib and augmenting the environment library path works to build modules every EXCEPT from within the Lean server for some reason (at least on Windows). I even verified the environment path from lake print-paths on the terminal and lake print-paths in the server are the same and it still did not work.

To fix this, I am providing the full library path to --load-dynlib. This does mean we are likely to run into command line length limit sooner though.

[Sebastian Ullrich]

I'm not sure what you mean by environment path. There is no shared object search path in print-paths, is there? It's just immediate file names.

[Mac]

@Sebastian Ullrich When Lake builds modules in print-paths it augments the environment of the lean command. One thing it does is add the directories of shared libraries (e.g. build.lib) tot the platform-specific shared library path environment variable (e.g., LD_LIBRARY_PATH on Linux, PATH on Windows). This allowed it to get away with using just load-dynlib=Mod-Name.so instead of load-dynlib=build/lib/Mod-Name.so. However, for some reason this does not work when run from the server (at least on Windows). It does work when print-paths is run directly from the command line though.

[Mac]

Another issue I just ran into is that Linux requires an augmented environment even if a full path is provided to --load-dynlib to load nested linked dynlibs (MacOS and Windows allow nested libraries to be preloaded to avoid this check). This is a problem for external libraries loaded by the server because we don't know the path of the library until the build completes and by thus we cannot ahead-of-time augment the Lean server's environment to include those paths.

[Sebastian Ullrich]

Mac said:

Sebastian Ullrich When Lake builds modules in print-paths it augments the environment of the lean command.

Are you thinking of lake env? There is no way for the current print-paths to affect the environment of the calling process, especially since changing the environment of a running process is Problematic anyway on certain platforms and thus not exposed in the IO API.

[Sebastian Ullrich]

However, for some reason this does not work when run from the server (at least on Windows).

Did you check that the worker process has the expected PATH? I suppose there's also Dependency Walker, but I don't know if that's convenient to use in this multi-process scenario.

[Sebastian Ullrich]

@Mac Time to release these fixes?

[Mac]

Sebastian Ullrich said:

There is no way for the current print-paths to affect the environment of the calling process, especially since changing the environment of a running process is Problematic anyway on certain platforms and thus not exposed in the IO API.

Ah, I did not realize setting environment variables from in a process was problematic on certain platforms. In that case, yeah my idea would not work.

Sebastian Ullrich said:

Did you check that the worker process has the expected PATH?

Yes. I did. The process does have the expected PATH? For one of the issues, this didn't even matter, because the problem was that the lean subprocess of Lake (to build the module) was the one that could not find dynlib. I even hard-code the process with the correct PATH and it still didn't work. So, I was stumped and went with the current solution.

Sebastian Ullrich said:

Mac Time to release these fixes?

Yeah, sorry. I meant too, but have making them, I got busy and never got around to making a PR. Here it is now: lean4#2070.