The Coq mailing list

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

Dear Tillmann,

True. But what you can do, if you are interested in measuring time, is to 
call vm_compute with a trivial function, which accepts b and returns a unit. 
Then you can subtract this time in your equation and see if both sides get 
closer:

Time g a + Time h b - Time "return_unit_from_any_type" b = Time f a

Best regards,

Michael 

> -----Original Message-----
> From: 
> coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  On
> Behalf Of Tillmann Weisser
> Sent: Monday, November 02, 2015 2:47 PM
> To: 
> coq-club AT inria.fr
> Subject: RE: [Coq-Club] Time analysis
> 
>  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
> >
> 
> 
> 
> 
> 

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