The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Keep in mind, also that Coq semantics does not take into account whether evaluation is lazy or eager.

If you want to extract code to Haskell or OCaml, execution time behaviour can largely differ.

2015-11-02 9:14 GMT+01:00 Tillmann Weisser <tweisser AT laas.fr>:

Dear Coq-Club,

I want to do a time analysis of a function in my code. However, I don't really know how to do this. Here is my problem:

Given 3 types A, B and C and converting functions g: A -> B and h: B -> C. I want to analyse the function f:= h o g.  In particular I'm interested in the question which part of f (i.e. g or h)  takes most of the time.

Let now a be of type A. I ran the commands

Time Eval vm_compute in (f a).
Time Eval vm_compute in (g a).
Let b:= Eval vm_compute in (g a).
Time Eval vm_compute in (h b).

However, the evaluation of (h b) is as slow as the evaluation of (f a), whereas the evaluation of (g a) is a little bit faster than the others. (The times of (g a) and (h b) do not sum up to the time of (f a).) What can I conclude from that? Is there a better way to analyse f?

Thanks for your help in advance!
 Tillmann