stack overflow with StateM

Stream: lean4

[Alexandre Rademaker]

I am implementing the Gale-Shapley in Lean. My code will need to handle real data. One of the inputs has 18430 candidates and 43 posts, resulting in 792490 potential interactions. I am getting Stack overflow detected. Aborting. in the command line after building and executing it with lake exec.

I am using StateM monad, can it be the problem? Is there any limitation in the StateM? I am running on MacOS, with

% ulimit -s
65520

[Notification Bot]

A message was moved here from #lean4 > stack overflow by Alexandre Rademaker.

[Eric Wieser]

Can you share an example?

[Alexandre Rademaker]

It will be hard to reduce to a MWE.. but I will share the link …

[Alexandre Rademaker]

https://gist.github.com/arademaker/67982be24c455756ecd43d4b21817e5b

[Alexandre Rademaker]

The way I call the function is

def main (args : List String) : IO Unit := do
 match args with
 | [] => println! "Usage: lake cpnu NUM"
 | a :: _ =>
  let (cs, ps) ← buildInstance "/Users/ar/r/cpnu/2025.2/dados" a.toNat!
  println! s!"candidates x posts: {cs.size} x {ps.size} = {cs.size * ps.size}"
  let m := (galeShapley cs ps).run (initialState cs)
  for k in m.2.assignments.keys do
   IO.println s!"Assignments: {k} => {m.2.assignments[k]?}"

[Alexandre Rademaker]

I would be interested in any ideas about how to debug the code. How can I add some extra flags to understand the functional call stack that is causing the stack overflow?

candidate 281972 selected from 1586 free

Stack overflow detected. Aborting.
zsh: abort      .lake/build/bin/cpnu 7

This happened almost at the end of the loop... But the next dataset can be 40% bigger.

[Robin Arnez]

Does gdb help?

[Kyle Miller]

It might also be worth experimenting with abbrev GS := StateRefT MatchState IO, just to get it to run.

It'd be nice to understand what's causing the stack overflow with StateM though.

[Alexandre Rademaker]

@Robin Arnez how to flag the lake build to add -g in the compilation? I suppose this would be my first question for trying to use gdb. Debugging at the C level will probably be more complex, but I am willing to try anything to solve the problem.

[Robin Arnez]

You can put moreLeancArgs = ["-g"] into your lakefile (if I read the code correctly)

[Alexandre Rademaker]

@Kyle Miller ... I will try, but I need to understand StateRefT first.

[Kyle Miller]

I expect you won't need to change very much. It just changes the underlying implementation of how the state is threaded through the computation, though while also making your code be in the IO monad rather than be pure.

[Alexandre Rademaker]

Yep. no need to make changes, but I ended up with the same problem... Stack overflow detected. Aborting.