coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using vm_compute and reflexivity

From: Kenneth Roe <kendroe AT hotmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Using vm_compute and reflexivity
Date: Sat, 22 Apr 2017 17:58:46 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=SoftFail smtp.mailfrom=kendroe AT hotmail.com; spf=None smtp.helo=postmaster AT nm17-vm3.bullet.mail.ne1.yahoo.com
Ironport-phdr: 9a23:DDNNWxOqjDSIZ969d70l6mtUPXoX/o7sNwtQ0KIMzox0LfT/rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr8zWTSi6LtrSBryhycGMz416XjbhMx+ga9Zox+tvgFzz5DJa42RO/dyYqbRcNUHTmRDQ8lRTTRMDIOgYIQAEuQPM+hYoZf/qFUNqhWzHhOjCP/qyjJShn/6wa833uI8Gg/GxgwgGNcOvWzRotrrMqcSV/66zLXIzT7ec/1W3iny45XPfxAiv/6MW69/cdDWyUYxDA7FjlKQqZDgPzyP1+QNt3KX4PZnVeKqkmMqrRx6rDu3xso0joTEhZgZxk3K+Ch62oo4IcC0RFRmbdOrEpZcryWXOohsTs8/TWxluzw2xqMYtZO6ZiQG1ZoqywDZZveaaYaH+AjjW/yUITpghHJqZra/hxGq/Eimz+3wS8u53E9UripAnNTArGsC1wHX6siDVPR94l2t2TOV2ADS7uFIO0Y0mrTGJ5I7wr8/jJoTsUPEHiPshEr2i6qWel0l+uiu9evnfq3rq5ufOoNulw3zPKcjlta7DOglKAQCQmeW9Oak2L3m50L5QbFKjvMskqnetZDXPccbqbC/AwBIyIYj7AiwAiym0NQfgXkHKUhKeBODj4TzJ17OJ/X4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDGmIG+qSNL7YmV6O/OMmZeeWN6EPvzOoCPUj4fPyjTcDnlJVKaqk25cNb32QHvN6JkyYZTznhdJXQjRChRY3UOG/0A7KajVUfXvnA/ox

I tried your suggestion. It still appears that the call to vm_compute is very slow. In my system, the “3+4” is in fact a term that is considerably more complex. Is there a way to obtain profile information to figure out where the time is going?

- Ken

On Apr 22, 2017, at 9:13 AM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

match goal with |- exists _, _ = ?X =>
let y := eval vm_compute in X in
exists y; vm_cast_no_check (refl_equal y)

[Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017
- Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
  - Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
    - Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017
      - Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/22/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Laurent Thery, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
        
        Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/23/2017
    - Re: [Coq-Club] Using vm_compute and reflexivity, Kenneth Roe, 04/22/2017