Stream: Coq devs & plugin devs

Topic: Debugging an infinite loop in `interp_constr_may_eval`

view this post on Zulip 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?

view this post on Zulip Janno (Nov 29 2021 at 18:13):

Here is a perf flamegraph in case that helps: (limited to 5 seconds)

view this post on Zulip Janno (Nov 29 2021 at 18:14):

I guess I could try to reverse engineer the input from that

view this post on Zulip Janno (Nov 29 2021 at 18:21):

Looking at the graph again it seems like this is actually a case of reduction looping. Hm..

view this post on Zulip 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: Dec 05 2023 at 06:01 UTC