Dear all,
this is my first mail to the list, so first I wanted to say hello and kindly ask you for forgiveness if I break any conventions that usually apply in the list.
We were doing some program performance testing with Poly ML 5.5 and we detected the following behavior when trying to use the information provided by "PolyML.timing" (I tried to produce a toy example).
fun fact (n : int) = (if n = 0 then 1 else n * fact (n -1 )); PolyML.timing true; open TextIO; val foo = openOut ("foo"); open Int; output (foo, toString (fact (10000)));
The last function returns a "run" time of "0.1" in a Linux machine, but "11.7" (approx) in our Windows machine, when the real time can be checked in both machines to be of the order of "0.1" (actually, the Windows machine in our case has much better hardware and is indeed faster in computations, this is the reason why we wanted to stick to it). Somehow, the timing information provided in the Windows machine is not correct. It scales to greater computations, where 200 seconds of real run time are shown in Windows as maybe 2000.
In our Linux machine we have used the polyml version shipped with Isabelle 2013, whereas in the Windows machine we are using the binary version for Windows obtained from sourceforge.
Are we doing anything wrong? Is this a known issue?
Thanks for any hints,
Jesus
-- Jes?s Mar?a Aransay Azofra Universidad de La Rioja Dpto. de Matem?ticas y Computaci?n tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logro?o, Espa?a