Zulip Chat Archive

Stream: mathlib4

Topic: error while loading shared libraries


Kevin Buzzard (Oct 24 2022 at 20:20):

I just pulled mathlib4 master and typed lake build and I got

/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2022-10-20/bin/lake: error while loading shared libraries: libleanshared.so: cannot open shared object file: No such file or directory

What did I do wrong? :-(

Kevin Buzzard (Oct 24 2022 at 20:35):

fixed it by nuking the toolchain (I might have triggered two downloads of the toolchain simultaneously, one on the command line and one in VS Code)


Last updated: Dec 20 2023 at 11:08 UTC