Multiple lake packages in the same git repository?

Stream: lean4

[Daniil Kisel]

When a package depends on multiple packages from subdirectories of the same git repository, lake-packages gets a clone per package. Is there a workaround? Or should I split the repository? (use case - similarly themed small interdependent libraries)

[Mac Malone]

I believe it would be possible to have Lake clone such packages via --sparse and perform a sparse checkout of the particular subdirectory (along with maybe a --filter). So, it is probably worth making an issue requesting this feature on the Lean 4 repository. Some caveats here are that this would raise the required Git version for Lake to something much newer and that Git's support for this is still not bullet-proof (see StackExchange questions like (1) and (2)).

[Daniil Kisel]

Should I use the RFC template for feature requests?

[Mac Malone]

Or the bug one, either is probably fine for this.

[Daniil Kisel]

Done: lean4#2773.