libStd.a file not found running `nix develop` through flake template

[noghartt]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

I have a Macbook M1 Pro, tried to install the Lean4 using the Nix template file, but follow this error below.

ld: warning: directory not found for option '-L/nix/store/5cm04cks3zf4aki08hxp0cp9s5nkhb7v-lean-bin-tools/lib/lean'
ld: file not found: /nix/store/3rnhnbmygslflmcyas6xadpma29pz5ny-Lean-lib/libStd.a
clang-11: error: linker command failed with exit code 1 (use -v to see invocation)

It happens after running the command nix develop and start to build all Lean4 packages.

Context

I tried to do a derivation on this package by myself to debug but couldn't find anything, any idea how to debug it on the right way?

Steps to Reproduce

1. Create a new Lean4 package using the Nix Flake template (nix flake new mypkg -t github:leanprover/lean4)
2. Access the package
3. Try to access the related nix shell running nix develop

Expected behavior:

Should be able to access the Nix shell

Actual behavior:

Be able to access Lean4's Nix shell and build the package

Versions

• Macbook M1 Pro (Sonoma 14.5)
• Nix v2.18.1

Additional Information

Impact

[nomeata]

Thanks for your report. The nix setup to develop Lean packages isn't well supported anymore, unfortunately, and we recommend to use elan, which you can get from nixpkgs. That said, if you can debug the issue and open a PR it will likely be merged (probably just Std, which was recently added, needs to be added to some list where previously only Init and Lean was listed.)

[noghartt]

Thanks for your report. The nix setup to develop Lean packages isn't well supported anymore, unfortunately, and we recommend to use elan, which you can get from nixpkgs. That said, if you can debug the issue and open a PR it will likely be merged (probably just Std, which was recently added, needs to be added to some list where previously only Init and Lean was listed.)

Oh, I get it.

Seeing the bootstrap.nix, seems that having something wrong at the $LEAN_CC variable. It it right, it should be ${Std.staticLib}/libStd.a here on the bootstrap.nix.

https://github.com/leanprover/lean4/blob/master/nix/bootstrap.nix#L128

I'll write a derivation and test it, if everything OKs, I'll submit a PR. Thanks!

[nomeata]

@noghartt Did you have success here? Is this related to #3811?

[noghartt]

Hey @nomeata,

Did you have success here?

Not yet, I didn't have much time to take a look on it, to be honest.

Is this related to https://github.com/leanprover/lean4/pull/3811?

I need to take a look on it, but seeing the diff, it seems to be related. I'll do some tests with this new merged PR.

[Kha]

The Nix build has been officially deprecated #4895