The Coq mailing list

["Tillmann Weisser" <tweisser AT laas.fr>]

Dear Michael,

Here I'm talking about times above 100 seconds and more. For example

Time Eval vm_compute in (f a). (* 119 sec *)
Time Eval vm_compute in (g a). (* 39 sec *)
Let b:= Eval vm_compute in (g a).
Time Eval vm_compute in (h b). (* 116 sec *)

Best regards,
 Tillmann

Am Montag, 02. November 2015 11:36 CET, "Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 schrieb:

> Dear Tillmann,
>
> did you consider that vm_compute involves some overhead, e.g. compilation 
> to byte code? In my experience for times above a few 100ms this is 
> negligible and times add up to about 10%, but for times below 100ms not. 
> About what time scale are we talking in your case?
>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>