compiling dependencies as static libraries

Stream: lean4

[Bhakti Shah]

I need the dependencies of my project to compile as static libraries instead of dynamic libraries. So far I've been doing this by going into build/lake-packages/dep/lakefile.lean and adding defaultFacets := ##[LeanLib.staticFacet] and rebuilding in build/lake-packages/dep but this is super hacky and manual, and ideally i want to be able to configure this in my package's lakefile itself. Is there a more straightforward way to do this? Thanks :)

[Mac Malone]

@Bhakti Shah You can also use lake build dep:static to build a dependency's static library.

[Bhakti Shah]

thanks! is there a way to put this into the lakefile so just lake build defaults to building dependencies as static?

[Mac Malone]

@Bhakti Shah no, but you could make a Lake script that builds the root package's dependencies' static libraries.

[Mac Malone]

Actually, if you want lake build to do it, you could make a default custom target (i.e., @[default_target] target all_static ...) that builds the packages dependencies as static libraries.

[Bhakti Shah]

oh that's an interesting idea, i'll try it out! I think I did try something with a custom target but I couldn't quite get the syntax right; i'll take another go at it though. Thank you :)