Zulip Chat Archive

Stream: general

Topic: lean4 on nixos

Johan Commelin (Sep 19 2022 at 10:32):

# version of lean that works
❯ ldd /home/jmc/.elan/toolchains/leanprover--lean4---nightly-2022-09-12/bin/lean
        linux-vdso.so.1 (0x00007ffc6d4d1000)
        libleanshared.so => /home/jmc/.elan/toolchains/leanprover--lean4---nightly-2022-09-12/bin/../lib/lean/libleanshared.so (0x00007f75c641c000)
        libdl.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libdl.so.2 (0x00007f75c6417000)
        libpthread.so.0 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libpthread.so.0 (0x00007f75c63f7000)
        libc.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libc.so.6 (0x00007f75c6222000)
        libm.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libm.so.6 (0x00007f75c60e1000)
        librt.so.1 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/librt.so.1 (0x00007f75c60d4000)
        /nix/store/bzd91shky9j9d43girrrj6vmqlw7x9m8-glibc-2.35-163/lib/ld-linux-x86-64.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib64/ld-linux-x86-64.so.2 (0x00007f75c9663000)

# version of lean that doesn't work
❯ ldd /home/jmc/.elan/toolchains/leanprover--lean4---nightly-2022-09-15/bin/lean
        linux-vdso.so.1 (0x00007ffc8a783000)
        libleanshared.so => /home/jmc/.elan/toolchains/leanprover--lean4---nightly-2022-09-15/bin/../lib/lean/libleanshared.so (0x00007f225c9c2000)
        libdl.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libdl.so.2 (0x00007f225c9bd000)
        libpthread.so.0 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libpthread.so.0 (0x00007f225c99d000)
        libc.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libc.so.6 (0x00007f225c7c8000)
        libm.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libm.so.6 (0x00007f225c687000)
        librt.so.1 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/librt.so.1 (0x00007f225c67a000)
        /lib64/ld-linux-x86-64.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib64/ld-linux-x86-64.so.2 (0x00007f225fc2a000)

Gabriel Ebner (Sep 19 2022 at 11:27):

The /lib64/ld-linux-x86-64.so.2 is very suspicious. Did you use a non-nixpkgs elan at one point?

Johan Commelin (Sep 19 2022 at 11:27):

Only via nix-env -e as you suggested earlier in this thread.

Gabriel Ebner (Sep 19 2022 at 11:28):

Hmm that should be fine.

Johan Commelin (Sep 19 2022 at 11:37):

@Gabriel Ebner So what can I try? I'm completely stumped.

Gabriel Ebner (Sep 19 2022 at 11:46):

Have you tried turning it off and on again? Does it work again if you do elan uninstall leanprover--lean4---nightly-2022-09-15?

Johan Commelin (Sep 19 2022 at 11:50):

Yeah, I tried that.

Johan Commelin (Sep 19 2022 at 11:50):

❯ elan uninstall leanprover/lean4:nightly-2022-09-15
info: uninstalling toolchain 'leanprover/lean4:nightly-2022-09-15'
info: toolchain 'leanprover/lean4:nightly-2022-09-15' uninstalled

❯ lean --version
info: downloading component 'lean'
137.3 MiB / 137.3 MiB (100 %)  20.7 MiB/s ETA:   0 s
info: installing component 'lean'
error: command failed: 'lean'
info: caused by: No such file or directory (os error 2)

❯ elan --version
elan 1.4.2 (4a1b1b918 2022-09-13)

Gabriel Ebner (Sep 19 2022 at 11:53):

which lean?

Gabriel Ebner (Sep 19 2022 at 11:54):

That doesn't look like a nixpkgs build.

Gabriel Ebner (Sep 19 2022 at 11:54):

This is how it should look like:

$ elan --version
elan 1.4.2 ( )

Johan Commelin (Sep 19 2022 at 11:54):

❯ which lean
/home/jmc/.elan/bin/lean

Gabriel Ebner (Sep 19 2022 at 11:55):

Okay, you've installed the official elan build. This was a bad idea.

rm -rf ~/.elan

Johan Commelin (Sep 19 2022 at 11:55):

Ooh, ok

Johan Commelin (Sep 19 2022 at 11:56):

❯ rm -rf ~/.elan

❯ lean --version
info: downloading component 'lean'
Total: 137.3 MiB Speed:   8.9 MiB/s
info: installing component 'lean'
Lean (version 4.0.0-nightly-2022-09-15, commit c1b7accd12f4, Release)

❯ elan --version
elan 1.4.2 ( )

Johan Commelin (Sep 19 2022 at 11:56):

Hooray! :octopus:

Last updated: Dec 20 2023 at 11:08 UTC