Stack overflow because of Multiset.fold

Stream: mathlib4

[Thomas Vigouroux]

Hey there,
I am hitting a problem with a code I have, that crashes because of a stack overflow in a function called l_List_redLength___rarg (which I assume is List.redLength. I can't find any place where my code uses List.toArray so I don't understand why this function is ever being called. How can I debug that ?

[Thomas Vigouroux]

I think my question is somewhat related to "How to debug lean code ?"

[Thomas Vigouroux]

Can it be because of a fold operation ? I am honestly confused by this

[Mario Carneiro]

this could be used in pattern matching code, or syntax match? It's hard to tell without an MWE

[Thomas Vigouroux]

Sadly, making a MWE out of this is completely out of my league.
I can link to to project that causes the bug though.

[Thomas Vigouroux]

There it is: https://git.sr.ht/~vigoux/busybeaver

[Thomas Vigouroux]

It seems that the binary crashes on initialization for some reason

[Thomas Vigouroux]

It looks like this is because I am trying to initialize a huge thing in called Init_TacticsExtra

[Sebastian Ullrich]

Do you have a stack trace?

[Thomas Vigouroux]

I'll provide one tomorrow but yeah I have one

[Thomas Vigouroux]

I did a bit of debugging.
The bug occurs _after_ doing a 'Finset.fold' for some reason.
Here is a back trace (numbers are off because I reordered them by call order):

#0  0x00005555578f52a8 in l_Finset_fold___rarg ()
#2  0x00005555560f7a92 in _init_l_main___closed__5 () at ././.lake/build/ir/Main.c:653
#1  0x000055555791f497 in l_Busybeaver (x_1=0x5, x_2=0x3, x_3=0x7fffe0ca2800, x_4=0x7fffdab764b8) at ././.lake/build/ir/Busybeaver.c:900
#3  0x00005555560f7074 in initialize_Main (builtin=1 '\001', w=0x1) at ././.lake/build/ir/Main.c:840
#4  0x00005555560f7206 in main (argc=1, argv=0x7fffffffd2f8) at ././.lake/build/ir/Main.c:861

[Thomas Vigouroux]

The offending code is essentially a Finset.fold operation on a pretty big Finset.
It seems that the fold operation goes through (after stepping through instruction by instruction).
There is something after the execution of the underlying Multiset.foldR operation though that calls toArray for some reason, and this causes the problem.

[Thomas Vigouroux]

I'll try to recompile mahlib with debug information so that I can have a better stack trace.

[Thomas Vigouroux]

So the problem definitely comes from Finset.fold, that for some reason calls toArray at some point.

[Sebastian Ullrich]

I don't understand what that backtrace is supposed to represent. A stack overflow backtrace should be thousands of frames. You shouldn't need a debug build either, just run it under gdb until it stops

[Thomas Vigouroux]

Oh, I did cut the thousands of l_List_... calls

[Thomas Vigouroux]

There you go, I just thought this was less interesting:

#0  0x000055555b2a07e2 in l_List_redLength___rarg ()
#1  0x000055555b2a07fe in l_List_redLength___rarg ()
#2  0x000055555b2a07fe in l_List_redLength___rarg ()
#3  0x000055555b2a07fe in l_List_redLength___rarg ()
#4  0x000055555b2a07fe in l_List_redLength___rarg ()
#5  0x000055555b2a07fe in l_List_redLength___rarg ()
#6  0x000055555b2a07fe in l_List_redLength___rarg ()
#7  0x000055555b2a07fe in l_List_redLength___rarg ()
#8  0x000055555b2a07fe in l_List_redLength___rarg ()
#9  0x000055555b2a07fe in l_List_redLength___rarg ()
#10 0x000055555b2a07fe in l_List_redLength___rarg ()
#11 0x000055555b2a07fe in l_List_redLength___rarg ()
#12 0x000055555b2a07fe in l_List_redLength___rarg ()
#13 0x000055555b2a07fe in l_List_redLength___rarg ()
#14 0x000055555b2a07fe in l_List_redLength___rarg ()
#15 0x000055555b2a07fe in l_List_redLength___rarg ()
#16 0x000055555b2a07fe in l_List_redLength___rarg ()
#17 0x000055555b2a07fe in l_List_redLength___rarg ()
#18 0x000055555b2a07fe in l_List_redLength___rarg ()
#19 0x000055555b2a07fe in l_List_redLength___rarg ()
#20 0x000055555b2a07fe in l_List_redLength___rarg ()

[Sebastian Ullrich]

So there is no List.toArray in the stack trace?

[Thomas Vigouroux]

I'll try to search for it, I remember there was

[Thomas Vigouroux]

Nope, the stack overflow occurs in a call to l_List_foldrTR___rarg

[Thomas Vigouroux]

The top of the stack when the stack overflow occurs:

#0  0x000055555b2a07e0 in l_List_redLength___rarg ()
#1  0x000055555b242c3c in l_List_foldrTR___rarg ()
#2  0x00005555560f84a1 in _init_l_main___closed__14 () at ././.lake/build/ir/Main.c:796
#3  0x00005555560f779c in initialize_Main (builtin=1 '\001', w=0x1) at ././.lake/build/ir/Main.c:1055
#4  0x00005555560f7956 in main (argc=1, argv=0x7fffffffd2f8) at ././.lake/build/ir/Main.c:1080

[Thomas Vigouroux]

I suspect there is a problem in the stack trace though

[Thomas Vigouroux]

I just can't wrap my head around why foldrTR would call redLength though

[Thomas Vigouroux]

The issue is reproducible using the following:

def main: IO Unit := do
  let all := Finset.univ (α:=Fin 3000000)
  let res := all.fold Nat.add 0 (λ n ↦ n.val)
  IO.println s!"Res: {res}"

[Thomas Vigouroux]

The call to toArray is in List.foldrTR

[Thomas Vigouroux]

I think that my question amounts to "Why foldr in Multiset.fold instead of foldl, which is already tail recursive ?"

Is it possible to move this thread to #mathlib4 ?

[Notification Bot]

This topic was moved here from #lean4 > Stack overflow because of List.toArray by Kevin Buzzard.

[Thomas Vigouroux]

Sorry to bother, but I have an issue with Multiset.fold causing a stack overflow.

Apparently Multiset.fold uses List.foldr which quite a bad idea because it in turns imply a toArray conversion. Is there a specific reason for chosing List.foldr instead of List.foldl ?

[Kevin Buzzard]

Maybe the answer is "because these things were written with proofs in mind rather than computational efficiency"? I don't know, that's just a conjecture. But certainly when I write code which I want to PR to mathlib I don't think at all about computational efficiency or tail recursion or anything.

[Thomas Vigouroux]

That's a good reason to me :wink:

[Kevin Buzzard]

Maybe the answer is "if you actually have a multiset with 300,000 elements and you want to run code rather than prove theorems then you might want to think about using a more computationally efficient model for multisets"? I have never regarded it as mathlib's job to offer computationally efficient data structures (cf the steady stream of questions we have about why polynomials aren't computable: answer -- this makes it easier to prove theorems about them).

[Thomas Vigouroux]

Actually, having a quotient of list up to permutation is awesome computationally: a set is just a list on which I can make no assumption on the order, and the type system enforces that

[Thomas Vigouroux]

But if I make a PR that changes from foldr to foldl (fixing the lemmas), will this be accepted (under the assumption that is fixes my problem) ?

[Kevin Buzzard]

OK then if you think it's already computationally efficient then you could try making the PR which changes it from one fold to the other :-)

[Thomas Vigouroux]

I seems computationally efficient enough to me :wink:

[Kevin Buzzard]

I would imagine that it would be a tricky job getting mathlib to compile after the change, but feel free to try! I'll defer to others about whether such a PR would be merged, I don't know the first thing about computation.

[Thomas Vigouroux]

I am trying my change as we speak, I'll report back !

[Eric Wieser]

!3#161 might be related

[Thomas Vigouroux]

Probably.

Note that this change seems to fix my problem.

[Thomas Vigouroux]

I just have to fix a bunch of lemmas in Finset and Multiset and it should be good to go hopefully.

[Ruben Van de Velde]

So to get better definitional equalities, but I think it's a bug if we rely on them anywhere outside the basic API lemmas anyway

[Ruben Van de Velde]

I'd be surprised if making the change would be terribly hard, though

[Thomas Vigouroux]

Making the change is very easy
But it breaks in unexpected places e.g. Multiset.Lattice

[Eric Wieser]

An easy way out might be to use @[csimp] to give Multiset.fold a faster runtime implementation

[Thomas Vigouroux]

In my specific case, I don't need this

[Thomas Vigouroux]

Multiset.fold already boils down (I went through the assembly) List.foldr in a few instructions

[Eric Wieser]

The faster runtime version would be the one that unfolds to List.foldl

[Thomas Vigouroux]

Changing it to foldl will turn that into something tail-recursive

[Eric Wieser]

My point is that if you use csimp you don't have to fix anything downstream

[Thomas Vigouroux]

Oh I see

[Thomas Vigouroux]

This way I don't have to make a PR to mathlib :wink:

[Thomas Vigouroux]

Or better: I can make a PR to mathlib that adds the csimp

[Thomas Vigouroux]

Adding the csimp fixes the issue.

[Ruben Van de Velde]

Please put the changes you already made somewhere, I probably want to land them anyway

[Thomas Vigouroux]

Here is my version of it, do you want me to open a PR ?

private def fold_impl : α → Multiset α → α :=
  foldl op (right_comm _ hc.comm ha.assoc)

@[csimp]
theorem fold_eq_fold_impl : @fold = @fold_impl := by {
  funext
  exact fold_eq_foldl _ _ _
}

[Eric Wieser]

I think probably a reasonable approach here is:

• Merge a PR adding that csimp lemma, to unblock usage like yours, with a TODO comment to...
• Evaluate (in terms of the effect on downstream proofs, and the effort required) whether we should just use foldl as the definition in the first place

[Thomas Vigouroux]

Well, the advantage of this csimp is to avoid having to think about that at all actually.

[Thomas Vigouroux]

But I see what you mean

[Eric Wieser]

Step 2 is only for if Ruben or someone else decides they want to think about it. I agree that step 1 is great because it means you can avoid worrying about it

[Eric Wieser]

(I get the feeling Ruben would like to see how far you got with that second step, even if you now are abandoning it)

[Ruben Van de Velde]

Yes, exactly

[Thomas Vigouroux]

I'm not abandonning it

Step 1 is a great quickfix to my problem.
I'll try to make step 2 go through too

[Thomas Vigouroux]

As indeed, there should not be any reason as to why this causes problems

[Thomas Vigouroux]

There you go: https://github.com/leanprover-community/mathlib4/pull/15617

Step one