elan nix package installs way more than it promises

Stream: general

[MangoIV]

It’s quite tedious to use elan from nixpkgs, together with the lean4 flake because it installs its own version of lean, lake and so on. It would be nice if it only installs what it says it will install to avoid having to fiddle around picking the correct binaries.

[MangoIV]

Wait. Why does it just link all the names to elan?

[Sebastian Ullrich]

That's how it does its main job of redirecting lean invocation to the correct toolchain

[MangoIV]

Aha! So what do I need elan for except for if I install lean and lake from the lean repo? I see that lake exe cache get fails without elan installed (or the “hook” thing that gets executed when you’re trying to lake update after adding mathlib as a dep)

[Sebastian Ullrich]

Using the flake together with mathlib just seems like a recipe for unnecessary suffering. Everyone else is using elan so nobody is testing e.g. the hook script with alternative setups.

[MangoIV]

Alright, thank you anyways!