The Coq mailing list

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

 Dear Michael,

Indeed, the size of the term b is a problem. However, I have no idea how to 
provide the term b other then by defining Let b:= Eval vm_compute in (g a).

Best,
 Tillmann

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

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