Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using vm_compute and reflexivity

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using vm_compute and reflexivity


Chronological Thread 
  • 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 22:08:04 -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 nm12-vm4.bullet.mail.ne1.yahoo.com
  • Ironport-phdr: 9a23:oxfSWxSD2E4Xx1Rn/yaLehlizdpsv+yvbD5Q0YIujvd0So/mwa69bBaN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4KBrSB/vlCcHMiQ28GDTisBpla5VoBysqh58zoLNfY2ZKud1cqfScN8GQGZMWNtaWS5cDYOmd4YBD/YOM+lXoIfgqVUOowWwCguvCu3o0TJImmb23agm3+QhDQ3L3gotFM8OvnTOq9X1Mb8fX+Wrw6nOyzXMce9W2Tfg44bUdRAuv+yHULVzccXPz0kgChnFjlKOpoH+PzOV0fgNs22B4OphUeKjkXIoqwZ0ojW2wMonl4rHhpoNx13A9ih12ps5KNO7RUJhZdOoDYFcuzyYOodoWs8vR2JltDwnxrAIupO3ZisHxZs9yxPQZfGKdZWD7Aj5W+aLOzh4gWpoeLKhiBa29kit0uv8Vsyp3FpUtyZFjNzMu38X2xPI98iHTv998Vm92TqV0gDc8OBEIUQumardNZEt36Q8l5oJvkTDGS/2n1/6g7ORdkUh4uSo6uLnbav6ppKEM4J5iRvyPrkgl8G8G+g1NhUCU3KG9em+yrHv5Uj5T69Ljv0ynKnZqpfaJcEDq666HQBV1Jss6wy4Dzi4y9kYnX4HLE5AeB2djojpP0vCL+z/Dfe6m1isiitkx+jaPr39BZXANmTMkLD4fbpk90FczBczwstE6pJPCrABJerzVVXruNzZCB85KQ20zPz9BNVzzINNEV6IV6SeKebZtUKCzuMpOeiFIoEP6xjnLP1wxPPoi3IlmRcneqThiZgabnyiGflOI0KFZHPthpEKFmJc7Vl2d/DjlFDXCW0bXH21Ra9pumk2

The vm_compute is considerably slower than just using compute. I don’t think
the issue is with computation time. The size of the structure returned is
about the same as the structure passed in. It still seems way too slow
given the structure—but I’ll experiment with a “count_size” predicate.

- Ken

> On Apr 22, 2017, at 6:58 PM, Laurent Thery
> <Laurent.Thery AT inria.fr>
> wrote:
>
>
> Hi,
>
> I don't know what you mean by returning complex structure. Is it really
> huge?
> In that case vm_compute can be slow because it needs to recreate the large
> structure.
>
> What I would do is to write a simple recursive function
>
> count_size : complex_structure -> Z
>
> that gives a rough measure of the size of the complex structure.
>
> Then I would do a
>
> Time vm_compute in count_size (propagateExists ......).
>
> If it is slow this means that your computation is slow.
> If you are using 8.6, you may then try native_compute to get a speed up.
>
> If it is fast but the return integer is quite large this means that
> the time is spend in allocating your result.
> The solution maybe then to try to accumulate your computation and only
> perform your computation when the result is "small".
>
> --
> Laurent




Archive powered by MHonArc 2.6.18.

Top of Page