The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Tillmann,

I see. Another question is how large the term b is. If it is rather large, 
the marshalling of the term to the VM might take a considerable amount of 
time. Did you try calling an identity function with term b and see how long 
this takes? This should then be subtracted from the run time of h b.

Best regards,

Michael

> 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
> >
> 
> 
> 
> 
> 

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