stack overflow in cache get

Stream: mathlib4

[Ruben Van de Velde]

$ lake exe cache get

Stack overflow detected. Aborting.

Anyone else hitting this / know how to debug it?

[Adam Topaz]

Is this happening on mathlib4 master?

[Adam Topaz]

FWIW, I just ran this command in a fresh copy of mathlib4 with no issues.

[Ruben Van de Velde]

Yeah, but also on an older branch where I'm sure it worked before. Must be something on my side, but I don't know where to start looking

[Arthur Paulino]

You can try placing dgb_trace calls in the cache code to find where the stack overflow is being triggered. This is one of the advantages of having cache implemented in Lean (easiness of debugging+maintaining the code)

[Ruben Van de Velde]

Looks like it's happening in RBTree.ofList in getLocalCacheSet with a list of 175827 paths

[Arthur Paulino]

Maybe your local cache is too big? Try lake exe cache clean to throw away a bunch of old files

[Kyle Miller]

By the way, the definition of RBTree.ofList is

@[specialize] def ofList : List α → RBTree α cmp
  | []    => mkRBTree ..
  | x::xs => (ofList xs).insert x

which isn't tail recursive. If you're ok with inserting things in the opposite order, the function could be switched to docs4#RBTree.fromList which is.

[Arthur Paulino]

That's a nice one! Thanks Kyle. @Ruben Van de Velde feel free to switch to fromList.

Btw, why are there ofList and fromList? I think the current ofList should be purged and fromList should be renamed to ofList to keep up with other Lean 4 names

[Kevin Buzzard]

Arthur Paulino said:

Maybe your local cache is too big? Try lake exe cache clean to throw away a bunch of old files

Is this the kind of command which I can do randomly from time to time without fear of breaking anything (in the sense that I can always lake exe cache get on a branch to get any caches back)?

[Kevin Buzzard]

ooh I have 6 gigs which I didn't have 10 seconds ago

[Ruben Van de Velde]

Nice. !4#3507 fixes the issue for me.

[Arthur Paulino]

Kevin Buzzard said:

Arthur Paulino said:

Maybe your local cache is too big? Try lake exe cache clean to throw away a bunch of old files

Is this the kind of command which I can do randomly from time to time without fear of breaking anything (in the sense that I can always lake exe cache get on a branch to get any caches back)?

Yes, cache clean discards everything that's not potentially used by your current branch state. And if you do cache clean! then it just wipes your cache files completely, regardless of how useful they are.

Both options are safe and don't compromise cache get/cache get!. The immediate consequence on that regard is that you might need to redownload some files, but this is expected ofc