Janno (Nov 29 2021 at 18:12): Janno (Nov 29 2021 at 18:12):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?
Janno (Nov 29 2021 at 18:13):Here is a perf flamegraph in case that helps: https://share.firefox.dev/3FS29WO (limited to 5 seconds)
Janno (Nov 29 2021 at 18:14):I guess I could try to reverse engineer the input from that
Janno (Nov 29 2021 at 18:21):Looking at the graph again it seems like this is actually a case of reduction looping. Hm..
Janno (Nov 30 2021 at 08:06):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: Jun 04 2023 at 19:30 UTC