debugging maximum recursion depth

Stream: lean4

[Chris B]

Is there any way to get more info about/debug a maximum recursion depth has been reached (use set_option maxRecDepth <num> to increase limit) error? I'm getting this in a very odd spot, but it's not feasible for me to reduce the context to a self-contained mwe.

[Henrik Böving]

The only thing that would come to my mind would be to place sensible dbg_traceand figure out from that what is happening but maybe there is more sophisticated things.

[Chris B]

Thanks. Whatever it is, it doesn't seem to be easily reachable with print debugging. I have something like:

have h : min (min a b) c <= c := min_le_right _ _
refine le_trans h ?x

and it's only giving me the error at the le_trans part.

[Chris B]

I'm actually getting this in two places with le_trans, so it seems to have something to do with that.