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: Mon, 16 Nov 2015 10:52:21 -0500
Authentication-results: mail2-smtp-roc.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-qk0-f176.google.com
Ironport-phdr: 9a23:QTzelx/wMw3sg/9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdidtq0P1LuempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lR8iP0I/ohqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEzhSg2G+nsVVC0ynxtWDg7ZpEX4WZHwsSb+u+dV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9

On 11/13/2015 01:50 PM, Pierre-Marie Pédrot wrote:

On 13/11/2015 17:43, Jonathan Leivent wrote:

So, "rewrite in |-*" is carrying around some burden from prior subgoals
in the same proof. Perhaps it is performing the search on the entire
proof term up to that point (which is large if I don't do those admits
or abstracts), instead of just on the particular subgoal's context?

I don't see where it could be doing so, but that's difficult to judge
without a test-case...

Working on it...

Jason's script has been running since Friday.

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