Zulip Chat Archive

Stream: lean4

Topic: Installing lean4 via nix on arm mac


Andre Knispel (Sep 19 2022 at 11:49):

I've been following the steps of the nix setup guide, but I keep getting the following error message once I try to run any nix command in the setup package:
error: getting status of '/nix/store/0ccnxa25whszw7mgbgyzdm4nqc0zwnm8-source/lean': No such file or directory

I'm relatively proficient with nix itself, but I don't know all that much about flakes, only that I've been having issues with other flakes that used eachDefaultSystem before, since it doesn't include aarch64-darwin. I've tried many different things, including trying to inspect the derivation with nix show-derivation and setting my system to x86_64-darwin in some ways locally for the lean shell, but I always just get this error message, without any extra information of where it's coming from.

Any ideas on what I could be doing to fix this, that don't involve setting my system to x86_64 globally?

Sebastian Ullrich (Sep 19 2022 at 11:54):

Mmh, I haven't seen this error before. But you should usually get more context using --show-trace

Andre Knispel (Sep 19 2022 at 12:03):

Good point, usually nix reminds me of that but it didn't this time. But it actually also doesn't print anything else

Andre Knispel (Sep 19 2022 at 12:05):

I get the feeling that this is a very early failure, since I poked it in many ways and I couldn't get any other information out of it

Andre Knispel (Sep 19 2022 at 12:11):

In fact, even derivations that don't exist just give that error message. For example if I run nix build .#abc


Last updated: Dec 20 2023 at 11:08 UTC