Conditional dependencies in lakefile

Stream: lean4

[Raghuram Sundararajan]

I created a new Lake package with lake new test math and ran lake update in it. I expected that since test only depends on mathlib and without -Kdoc=on or similar, none of mathlib or its transitive dependencies depend on doc-gen4, that doc-gen4 would not be cloned. However, it was.

Is this the expected behaviour? That is, is the conditional nature of meta if configuration only supposed to apply during lake build, etc., and not when downloading dependencies using lake update?

[Raghuram Sundararajan]

bump

[Raghuram Sundararajan]

It is a bit annoying to clone Unicode as a 100 MB doc-gen4 dependency in every toy project that depends on mathlib.

[Arthur Paulino]

As a reference, some package managers use the concept of "dev dependencies", which shouldn't be downloaded if the package is being used as a dependency of another

[Wojciech Nawrocki]

This sounds like a bug in Lake @Raghuram Sundararajan , it would be good to have this recorded as an issue on https://github.com/leanprover/lake .

[Raghuram Sundararajan]

Wojciech Nawrocki said:

This sounds like a bug in Lake Raghuram Sundararajan , it would be good to have this recorded as an issue on https://github.com/leanprover/lake .

Done here. Sorry for the delay; I forgot about this.