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?

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 `rewrite`

or `setoid_rewrite`

tactic, but the relation that is rewritten is not `eq`

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!

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

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

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: Oct 05 2023 at 02:01 UTC