Zulip Chat Archive

Stream: lean4

Topic: Issue with lake

Adam Topaz (Apr 17 2023 at 17:46):

I am running into some issues with lake. Here's what I have done (in my home folder):

  1. lake new Playground math
  2. cd Playground
  3. lake --version

The output is

/home/adam/.elan/toolchains/leanprover--lean4---nightly-2023-04-11/bin/lake: error while loading shared libraries: libc++.so.1: cannot open shared object file: No such file or directory

Adam Topaz (Apr 17 2023 at 17:46):

Is it just me or can someone reproduce?

Adam Topaz (Apr 17 2023 at 17:47):

I get the same behavior if the first step is replaced with lake new Playground

Henrik Böving (Apr 17 2023 at 17:47):

Works for me, do you have libc++.so.1 on your system?

Henrik Böving (Apr 17 2023 at 17:48):

The package that ships it should be called something like libcxx

Adam Topaz (Apr 17 2023 at 17:48):

I assume so, since I never had this issue before. I'm on nixos and I have no clue how to check whether I actually have it.

Henrik Böving (Apr 17 2023 at 17:49):

Hmmm, idk if NixOS has a mechanism for that but i guess you can always jus locate libc++.so.1

Gabriel Ebner (Apr 17 2023 at 17:51):

You've probably updated nixos after elan downloaded the 4/11 binaries. It should be enough to elan uninstall leanprover/lean4:nightly-2023-04-11 and then it should work again.

Adam Topaz (Apr 17 2023 at 17:53):

That worked. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC