The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

First result—I tried native_compute.  I got the following:

Toplevel input, characters 0-15:> native_compute.> ^^^^^^^^^^^^^^^Anomaly: 
Compilation failure. Please report.

               - 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