Zulip Chat Archive

Stream: lean4

Topic: Small PR to fix Compiling Mathlib4 with Nix

Enrico Borba (Mar 31 2023 at 19:38):

I saw that the contributing guides specify discussing PRs here before submitting them:

I'm on NixOS and tried to compile mathlib4 with nix, using buildLeanPackage. However, because of the size of mathlib, there is a part of the build process involving a bash script that fails because a generated environment variable is too large (because of an OS limit). The specific error is bash: Argument list too long. The offending section is here. I have a very small PR to fix this (a 5-line change) and I was wondering if the maintainers would be open to me submitting it. Here's the commit itself on my fork.

Sebastian Ullrich (Mar 31 2023 at 19:53):

I would appreciate a PR fixing this, but I believe you should use passAsFile instead to avoid creating additional derivations

Sebastian Ullrich (Mar 31 2023 at 19:54):

Obligatory disclaimer that with Nix you're missing out on the mathlib4 cache, and also Nix seems to start to struggle a bit with Lean projects of this size

Enrico Borba (Mar 31 2023 at 20:14):

Was hoping to hear that I didn't do this correctly! Thanks for the tip on passAsFile. I'll add that and open a PR.

Can you explain a bit more about missing out on the cache? Is this to do with lake?

And Indeed having to compile mathlib is kind of annoying (takes ~10 minutes) on my laptop, but with this fix I am able to have a dev environment where nix build . will recognize mathlib imports.

Sebastian Ullrich (Mar 31 2023 at 20:22):

10min is actually impressive, I think for most people it's closer to 20min or more

Enrico Borba (Mar 31 2023 at 20:23):

Eh perhaps I'm underestimating. It definitely didn't feel _that_ long...

Sebastian Ullrich (Mar 31 2023 at 20:24):

Can you explain a bit more about missing out on the cache? Is this to do with lake?

mathlib4 comes with an executable cache that downloads .oleans into Lake's build/ directory. Which of course is not at all how it works in Nix.

Enrico Borba (Mar 31 2023 at 20:32):

Ah got it. If I understand correctly, I think I'll just have to recompile mathlib every time I update it?

Sebastian Ullrich (Mar 31 2023 at 21:03):

The parts that are affected by the update at least, yes

Enrico Borba (Mar 31 2023 at 21:32):

Ah got it. Thanks again for the help, here's the PR: https://github.com/leanprover/lean4/pull/2179/commits/3c757e39fa4e4478d21228124bf6e3160b97ac28

Last updated: Dec 20 2023 at 11:08 UTC