Cache.lean?

Stream: mathlib4

[Damiano Testa]

In the context of lake exe mkAll, I noticed that the libraries on which Mathlib depends all have a library.lean file importing all the .lean files of the library except for Cache. I realize that no one probably wants to import Cache, but this argument would apply also to MathlibExtras and docs.

Should Cache.lean be (auto-)generated?

[Yaël Dillies]

That's a bit strange indeed. Was not having Cache.lean a conscious design decision or an oversight?

[Mario Carneiro]

Cache is not really a library, it's an exe which is too big for one file

[Mario Carneiro]

and lake has some silly restrictions about lake exes not having multiple modules