Zulip Chat Archive
Stream: mathlib4
Topic: problems installing lean4/mathlib4
Alex Kontorovich (Jan 04 2023 at 20:43):
Can someone please help with this error message?
alexkontorovich@alexs-mbp-3 mathlib4 % lake exe cache get
dyld[78814]: Library not loaded: @rpath/libleanshared.dylib
Referenced from: <4C4C44B5-5555-3144-A1EE-735D621B0ED9> /Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/bin/lake
Reason: tried: '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/lean/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/lean/libleanshared.dylib' (no such file), '/System/Volumes/Preboot/Cryptexes/OS@rpath/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/lean/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/libleanshared.dylib' (no such file), '/Users/alexkontorovich/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib/lean/libleanshared.dylib' (no such file), '/usr/local/lib/libleanshared.dylib' (no such file), '/usr/lib/libleanshared.dylib' (no such file, not in dyld cache)
zsh: abort lake exe cache get
Last updated: Dec 20 2023 at 11:08 UTC