refactor: nix: avoid adding search path symlinks to the nix store

[nomeata]

This fixes #2508.

(Includes release branch commits for easier testing, will fix that
before undrafting)

[Kha]

Nice, any benchmarks yet? E.g. echo "-- $(date)" >> src/Init/Prelude.lean; time nix build --offline

[nomeata]

Before:

real	8m9,954s
user	0m1,514s
sys	0m0,785s

after

real	8m56,574s
user	0m1,453s
sys	0m0,760s

I wonder if it is even significant, -j8 on my laptop. Let me rerun… nope, seems reproducible.

I didn’t expect a regression, it has to create the same symlink trees as before, just during the per-module build rather than as a separate nix derivation. So that’s strange.

Maybe invoking cp more often makes a difference?

(Of course, the goal isn’t to make it faster per se, it’s to not have these symlink trees in /nix/store because they eat inodes like hell… but it’s worrying that it did become slower.)

[nomeata]

Still no good idea why it’s slower, but I can report that the code works building all of mathlib (as part of the loogle deploy)

[Kha]

Maybe invoking cp more often makes a difference?

Could be. Try measuring your script vs the corresponding lndir?

[nomeata]

Any idea why CI doesn’t run?

[Kha]

Not sure. You might need to push again after the base change.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2568 has successfully built against this PR. (2023-09-23 11:49:04) View Log

[nomeata]

No longer using this for loogle, so closing. Hopefully we will have a good lake-based nix setup eventually.