Yannick Zakowski (Jul 18 2020 at 15:26): Yannick Zakowski (Jul 18 2020 at 15:26):Hello,
I have a rewrite foo that takes 18s to perform that is puzzling me slightly. The lemma foo of interest is of the form: forall a b c, P a b c -> equiv (pattern1 a b) (pattern2 a b) where equiv is some homemade relation. The TC part to justify the rewrite is instantaneous, but it seems to first spend 18s trying to find pattern1 in the goal.
However, weirdly enough, doing:
match goal with
|- context[pattern1 ?a ?b] => rewrite (foo a b)
end.
Is instantaneous, where I would have assumed that finding the needed pattern via this match to be the same process as what rewrite foo must do internally.
Would anyone have insights in this problem? Alternatively, is there anyway to get debug informations to understand exactly where these 18s are spent?
Yannick Zakowski (Jul 18 2020 at 15:27):The actually lemma is of course more complicated, quantifying on 13 variables
Pierre-Marie Pédrot (Jul 18 2020 at 15:56):Is is vanilla rewrite or setoid rewrite? The latter has quite a few issues with performance blowups, but the former is not totally devoid of them either.
Pierre-Marie Pédrot (Jul 18 2020 at 15:57):From what you describe it could be some tricky unification issue, but it's hard to tell without profiling it
Pierre-Marie Pédrot (Jul 18 2020 at 15:57):As far as I am concerned I debug this kind of issues with low-level tools like the linux perf program, but you need to be used to the source code of Coq to make sense of th result
Yannick Zakowski (Jul 18 2020 at 15:58):I have the same behavior using the rewrite or setoid_rewrite tactic, but the relation that is rewritten is not eq
Pierre-Marie Pédrot (Jul 18 2020 at 15:59):Ah, so it's definitely calling setoid rewriting.
Pierre-Marie Pédrot (Jul 18 2020 at 15:59):We've got quite a collection of performance bug reports about this one.
Pierre-Marie Pédrot (Jul 18 2020 at 16:00):If you have a reproducible example I can have a look.
Pierre-Marie Pédrot (Jul 18 2020 at 16:01):The fact you have a lot of quantified variables for instance is likely to be the cause of such slowdowns, I can probably find the relevant bug report
Yannick Zakowski (Jul 18 2020 at 16:01):I can definitely have a reproducible example, but that's gonna depend on quite a few things. I'm going to see if I can cut at least Helix from the dependencies
Yannick Zakowski (Jul 18 2020 at 16:02):Another surprising point is that I have since my initial post stumble upon a similar one that still takes 9s even after providing explicitly all arguments
Yannick Zakowski (Jul 18 2020 at 16:27):@Pierre-Marie Pédrot Here are two fairly minimal examples: https://github.com/vellvm/vellvm/blob/slow-rewrite/src/coq/Slow_Rewrite.v
It would require you to install Vellvm to reproduce it though.
Thanks for any insights!
Gaëtan Gilbert (Jul 18 2020 at 19:14):Possibly pattern is syntactic but rewrite reduces when trying to unify.
You can Set Debug Tactic Unification and see if there's a difference between the outputs
Yannick Zakowski (Jul 18 2020 at 19:17):Oh I finally found it. The problem appears to have to do with modules. We have a functor Denotation that is instantiated in a file TopLevel.v to some module D := Denotation A B .
Now the file InstrLemmas, where we define the problematic lemmas, reinstantiated locally the functor with the same arguments to some D' := Denotation A B instead of simply loading D.
If I understand correctly, this led to somehow D and D' having to be unified every time one of these lemmas were used.
Loading D instead in InstrLemmas solves the problem
Yannick Zakowski (Jul 18 2020 at 19:24):I am not sure I finely understand how that led to the difference between pattern and rewrite though, but a least that solves it in practice.
Out of curiosity I'll give a shot at some debugging with Set Debug Tactic Unification to see if that helps me understand better what goes on under the hood. Thanks for the pointer Gaëtan
Last updated: Apr 16 2024 at 20:02 UTC