Conditional transitive dependencies are downloaded unconditionally

[ghost]

Transitive dependencies which are only dependencies of a dependency conditionally (for example, doc-gen4 is a dependency of mathlib only if mathlib gets the config option doc = on) are downloaded even if they shouldn't because the condition is false.

To reproduce, run:

mkdir test && cd test && lake init test math && lake update

This should not download doc-gen4 (at least, with the current dependencies listed by mathlib, std4, etc.), and instead, lake update should only download doc-gen4 if (e.g.) the lakefile is edited to read require mathlib ... with <options> to specify doc=on.
However, currently it does download doc-gen4 (and all its transitive dependencies).

[tydeu]

Dependencies' packages are installed by reading their lake-manifest.json. Mathlib 4's manifest contains doc-gen4 , so it will always be downloaded and installed with mathlib.

[Kha]

Well that describes Lake's current behavior, but I don't see why that needs to be the case. If a package is not reachable via require clauses, it shouldn't matter whether it exists on disk.

[ghost]

lake new test math && cd test && lake update now only clones the mathlib, Qq, aesop and std packages.
So the original issue is resolved.

This appears to be due to a mathlib4 commit removing the other packages from mathlib's lake-manifest.json, rather than a change in Lake, though.

[tydeu]

@Kha

Well that describes Lake's current behavior, but I don't see why that needs to be the case. If a package is not reachable via require clauses, it shouldn't matter whether it exists on disk.

The lake-manifest.json is meant to lock the dependency configuration to its specified state. Changes in the lakefile.lean are only suppose to be reflected in the lake-manifest.json upon a lake update. At least, that is how I understood the philosophy agreed upon in leanprover/lake#138. Thus, at the moment, I consider this behavior a feature of Lake, not a bug.

However, I do think better handling of conditional dependencies is something to keep in mind -- if Lake stored some representation of the condition in the manifest, then this issue could be resolved while preserving the dependency lock. In essence, I think Gabriel may be right when he observed in leanprover/lake@1bd8430#r82491382 that meta if is not the best solution for conditional dependencies and something more like Julian's original environment proposal in leanprover/lake#80 (comment) may be appropriate.