abab9579 (Sep 08 2022 at 00:50): 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!
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