coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3
Date: Fri, 13 Nov 2015 11:33:02 +0100

On 13/11/2015 05:41, Jonathan Leivent wrote:
> I compared a problematic rewrite in *|- against a
> repeat/match/context/rewrite tactic that does the same set of rewrites
> in the goal, and the rewrite in *|- was 8X slower. But, removing the
> context pattern removes the 8X speedup.

Probably due to the cost of finding paths through setoid_rewrite. Do you
have a reproducible and minimal example?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
- Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/13/2015
  - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
    - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
      - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jason Gross, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Clément Pit--Claudel, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/16/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/16/2015