coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3
Date: Fri, 13 Nov 2015 09:58:56 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f169.google.com
Ironport-phdr: 9a23:jF/KGR+++TKCQv9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdidtqsP1baempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lR8iP1o/pi6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhSg2G+nsVVC0ynxtWDg7ZpEX4WZHwsSb+u+dV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9

On 11/13/2015 05:33 AM, Pierre-Marie Pédrot wrote:

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?

It will take me a while to prepare something small. Maybe Jason's coq-bug-finder can be used to assist this process. I'll work on it...

However, note that none of the hypotheses in the example I tested have binders, and the rewrite itself is just on Liebniz equality.

-- Jonathan

[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