The Coq mailing list

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

Dear Michael, dear Julien,

thank you for your help.
@ Michael: the marshalling of b was not a problem. It took less than one 
second.
@ Julien: Circumnavigating the type checking was a helpful idea. Now I the 
timings sum up in a reasonable way.

Thanks a lot again and best regards,
 Tillmann

On Monday, November 2, 2015 15:04 CET, "Soegtrop, Michael" 
<michael.soegtrop AT intel.com>
 wrote:

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