The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

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