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