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?
The actually lemma is of course more complicated, quantifying on 13 variables
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.
From what you describe it could be some tricky unification issue, but it's hard to tell without profiling it
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
I have the same behavior using the
setoid_rewrite tactic, but the relation that is rewritten is not
Ah, so it's definitely calling setoid rewriting.
We've got quite a collection of performance bug reports about this one.
If you have a reproducible example I can have a look.
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
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
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
@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!
pattern is syntactic but rewrite reduces when trying to unify.
Set Debug Tactic Unification and see if there's a difference between the outputs
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
If I understand correctly, this led to somehow
D' having to be unified every time one of these lemmas were used.
D instead in
InstrLemmas solves the problem
I am not sure I finely understand how that led to the difference between
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: Oct 05 2023 at 02:01 UTC