nix: getting a cache hit

Stream: general

[James Sully]

Hi, I'm trying to build a trivial single .lean file executable using nix. I've copied the flake from here and tweaked the name.

I also poked around and found https://lean4.cachix.org. I added it as a substituter to my nix.conf, as well as the associated public key. However, when I nix build I'm still getting building lean-stage0 which I very much don't want to do on my laptop.

I was hoping the cache would have a pre-built copy of lean4 available. Is that the case? if so, is there something I have to do to get it, maybe specify the correct nixpkgs input?

[Mauricio Collares]

Can you paste the relevant section of nix.conf?

[Mauricio Collares]

Or just double-check the instructions at https://github.com/leanprover/lean4/blob/371fc8868af55eef20b63b9132cea60eb316c117/doc/setup/nix.md

[Mauricio Collares]

Oh, sorry, I missed lean4#3402

[James Sully]

Ah, thank you, and bummer