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 14:23:22 -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-f173.google.com
Ironport-phdr: 9a23:DLFpYxDs5kATnO3iD3nuUyQJP3N1i/DPJgcQr6AfoPdwSP74rsbcNUDSrc9gkEXOFd2CrakU1qyL6eu5BSQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTqkb3osMSPKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kbVGwKkhNOSyzI7Q/3WIu55in9sOt+1S2XMOX5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=

On 11/13/2015 01:56 PM, Jason Gross wrote:

Is [abstract (rewrite in |- *; admit)] faster than than [rewrite in |- *;
admit]?

Yes. Going back to the slow case (no prior subgoals abstracted or admitted), I did this:

Time (rewrite ?RW in *|-; admit).
Undo.
Optimize Proof.
Time (rewrite ?RW in *|-; admit).
Undo.
Time abstract (rewrite ?RW in *|-; admit).

and got this:

Finished transaction in 2.553 secs (2.551u,0.003s) (successful)
Evars: 44246 -> 2
Finished transaction in 2.568 secs (2.556u,0.s) (successful)
Finished transaction in 0.116 secs (0.112u,0.003s) (successful)

There's a vernacular (or tactic) that compacts the evar map, right?

Optimize Proof does that - but it didn't help above.

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