Stream: math-comp users

Topic: Rewriting takes long time, how to debug?


view this post on Zulip abab9579 (Sep 08 2022 at 00:50):

Hello, I have a code which hangs for so long on rewrite tactic.
I profiled it, it turns out rewrite in ssreflect cannot be broken down into inner invocations.

total time:  69.352s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─rewrite (ssrrwargs) (ssrclauses) ------ 100.0% 100.0%       1   69.352s

 tactic                                   local  total   calls       max
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─rewrite (ssrrwargs) (ssrclauses) ------ 100.0% 100.0%       1   69.352s

It runs for so long, but it is not infinite loop - it stops at 69.352s.
Let's say this is rewrite fooE.
Funny thing is, rewrite {1}fooE terminates instantly. rewrite {2}fooE runs indefinitely long, though.
What is the possible cause of this? How do I debug this problem? I do not even know where to look for.

Thanks in advance!

view this post on Zulip Cyril Cohen (Sep 08 2022 at 13:50):

Can we have a concrete piece of code where rewrite takes time?


Last updated: Jan 29 2023 at 18:03 UTC