Lean4 nix build?

Stream: lean4 dev

[Tom]

I am trying to build Lean 4 from source to submit a small PR. I am following the instructions here.

I've installed nix and cloned the repo but after running nix develop I get errors along with

trace: warning: The Nix-based build is deprecated

Is this build not supported anymore, or am I doing something wrong?

[Mario Carneiro]

there are build instructions both with and without nix

[Mario Carneiro]

you should use the one appropriate for your OS

[Tom]

yeah, I think I can make that work but was curious if the Nix build (which is supposed to work on MacOS, Linux and Windows) is actually deprecated or if I'm doing something wrong.

[Sebastian Ullrich]

Merely using the dev shell is not deprecated, the warning is just overzealous

[Tom]

Thanks for confirming!

[Notification Bot]

Tom has marked this topic as resolved.

[Tom]

FWIW, the nix instructions didn't "just work" for me on MacOS so I built Lean following the "manual" steps and submitted the PR that way. Unfortunately, I don't know enough about Nix and the Nix lean setup to help fix the issue but just FYI.

[Leni Aniva]

I made a Lean 4 nix flake here: https://github.com/lenianiva/lean4-nix

[Eric Wieser]

What is the step between running nix develop and getting a lean binary?

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

In particular, the suggested

# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

commands don't work because build/release isn't actually created by nix develop

[Eric Wieser]

Ah, nix develop .#test seems to make progress

[Sebastian Ullrich]

Eric Wieser said:

What is the step between running nix develop and getting a lean binary?

The generic build instructions shared with all other platforms

[Eric Wieser]

Oh, I read "that's it" as "you can stop reading all further instructions".

[Alex Keizer]

nix develop just puts you in a shell that has all the right dependencies in PATH, but you still have to do the actual build

[Sebastian Ullrich]

I can see how the wording is not ideal :)

[Eric Wieser]

I guess I was hoping I could somehow use nix to get a cached build rather than having to wait for a full compile

[Tom]

(I had the same question a while ago but didn't get a good answer - or at least one I could understand, given that I don't really use nix. Also, I think I had the same misunderstanding as you :grinning:)

Having said that, the non-nix build instructions are pretty good. Especially if you install ccache, the (incremental) builds are pretty quick.

[Tom]

haha, I didn't notice you revived my old thread!