Modifying link command in lake to use nix develop

Stream: lean4

[Anders Christiansen Sørby]

To simplify using lake in an FFI setting with lots of dependencies I've wrapped build commands for things like rust or gcc inside nix develop --command to ensure that they always build with the correct env. It is also possible to just run nix develop first, but for a simpler workflow just running lake commands right away would be easier. The problem is the linker. Is it possible (easy) to configure package to use a different link command?
I want to add more nix support to lake in the future so that the UX is more smooth. Converting lake jobs into nix derivations would be very nice.

[James Gallicchio]

Anders Christiansen Sørby said:

Is it possible (easy) to configure package to use a different link command?

Last time I was messing with this, it is easy to add arguments to the linker command, but I don't recall there being a way to change the linker command itself... it would probably be in the PackageConfig structure if it exists?

[Anders Christiansen Sørby]

Yes, anything is possible, but it seems like the package interface does not have this option currently

[Anders Christiansen Sørby]

On a related note: @Mac How do I let lake know it needs to relink when I use manual link arguments? Now I have to run lake clean to relink

[Mac Malone]

Anders Christiansen Sørby said:

How do I let lake know it needs to relink when I use manual link arguments?

Are you asking about how to relink when the arguments themselves change or when the manually linked libraries change? For the later, you need to use extraDepTargets. For the former, that should happen automatically.

[Anders Christiansen Sørby]

I am using extraDepTargets but the relink does not happen. How does lake know when a target needs to rebuild? Does it hash the file tree?