toward "lake2nix"

Stream: general

[Quinn]

currently, i just don't nixify projects with dependencies. I like my hercules CI / flake parts nixification for lean projects that don't depend on other lean libraries, but I fall back to github for projects that depend

In principle, I feel like it'd be easy enough to walk lake-manifest.json and use pkgs.fetchGitHub to grab each repo at each rev, recursively call lake2nix on each dependency, then wire up all the symlinks.

Has anyone started this or have major disagreements about the high level conceptual design?

Note, I have less clear an idea of a developer experience with dependencies in devshells than I do of simply a build / CI experience (as well as lifting every lake exe foo to a nix run foo)

[James Sully]

I will be extremely psyched when there's an easy way to build lean projects with nix

[Sebastian Ullrich]

Speaking as someone who has investigated this topic before, a few caveats that ultimately made me give up on that approach: if you want to build each module as a separate Nix derivation (not absolutely necessary for deployment, but probably necessary for local development), then

• expect at least ~30% build time overhead. Nix is not made for building thousands of small derivations, there may even be some quadratic overhead in there.
• keep in mind that you will not be able to profit from the Mathlib cache or other non-Nix caches
• be aware that there hasn't been any progress on the content-addressed cache for Nix in years, without which you will not be able to benefit from any system changes we make in the future to avoid rebuilds either

[Quinn]

thanks for the insight! what would a content-addressed cache look like? not super familiar with that term.

[Sebastian Ullrich]

https://discourse.nixos.org/t/content-addressed-nix-call-for-testers/12881