Stack overflow in `lake exe cache get`

Stream: mathlib4

[Sébastien Gouëzel]

On the branch pfaffelh_caratheodory1, I get a stack overflow when doing lake exe cache get. I'm on windows. Can anyone reproduce, or is it just me?

[Rémy Degenne]

I see the same error. Stack overflow detected. Aborting.

[Sébastien Gouëzel]

Could that be a corrupt olean on the cloud?

[Sébastien Gouëzel]

It already failed in https://github.com/leanprover-community/mathlib4/actions/runs/13042162431/job/36386203480, when CI tried to build the branch.

[Sébastien Gouëzel]

It doesn't look like a corrupt olean, because lake exe cache get- (just downloading the files but not uncompressing them) also fails, as well as lake exe cache clean. I've merged master, but it doesn't make a difference.

[Sébastien Gouëzel]

@Mario Carneiro , do you have an idea what could be going on here? The branch is #21036

[Arthur Paulino]

Maybe this helps: last time I saw this it was due to some cyclic import making the hashing algorithm loop

[Ruben Van de Velde]

There's no import cycle, is there?

[Sébastien Gouëzel]

Good catch, thanks! Changing the imports indeed fixes it.

[Ruben Van de Velde]

The command should really handle this better, but at least some of us recognize the symptoms now :)

[Sébastien Gouëzel]

Yes, the Zulip error message is much more helpful than the built-in one :-)

[Jon Eugster]

I've added this to the pile in #21238:

jon@computer mathlib4 % lake exe cache get
uncaught exception: dependency loop found involving Mathlib.Init!