I am looking at a seemingly endless (and also endlessly allocating) loop in
interp_constr_may_eval. The trouble is that I do not even know which tactic is being called. I've added debug messages to everything I can think of but I've had no luck and I am running out of patience since my only test case is ~30 minutes into our code base and absolutely unminimizable. Is there a way to figure out what is triggering
interp_constr_may_eval so that I can try to find out what the heck is going on? Or does anybody know a specific case that would make it try to eat its own tail?
Here is a perf flamegraph in case that helps: https://share.firefox.dev/3FS29WO (limited to 5 seconds)
I guess I could try to reverse engineer the input from that
Looking at the graph again it seems like this is actually a case of reduction looping. Hm..
It took me a few hours of debugging but I finally found the problem. This is not an infinite loop. It is "just" a case of
simpl taking a long time and a lot of memory to reduce the goal. (More than 100GB of memory, to be precise). The goal itself is barely a screen of text and the terms that
simpl (probably) wants to reduce are of the shape
f (f (f (f (f x)))). So I suspect this is a pathological example of coq/coq#13772.
Last updated: Dec 05 2023 at 06:01 UTC