Linear chain of lake dependencies

Stream: lean4

[Jakob von Raumer]

I have a package A that depends on mathlib, a package B that depends on A, and a package C that depends on B. For some reason while a lake update && lake build in A and B is super quick, bumping the versions in C and building takes much longer because while it does download the mathlib cache, it goes through Running ... all the mathlib files, which takes quite some time, esp for tactics. Does anyone know what I could have misconfigured there? @Mac Malone

[Mac Malone]

Are A, B, and C all on the same Lean toolchain? If B is not on mathlib's toolchain when updating C, then C will not necessarily update to mathlib's toolchain before building. Instead, it will update to whatever B is on.

[Jakob von Raumer]

Yes, all on leanprover/lean4:v4.20.0-rc5

[Jakob von Raumer]

C in case has a .toml lakefile, while the other ones have a .lean one, but that shouldn't matter, right?

[Ruben Van de Velde]

No, should be fine

[Jakob von Raumer]

Hmm, I'll try to reproduce it on another machine...