On Thu, 27 Oct 2011, Lawrence Paulson wrote:
If my memory is correct, quicksort was the clear winner in the
performance tests that I undertook for my book.
I can confirm it for some later measurements of the refined implementation
-- data from 2005..2007, IIRC.
There are some anecdotes about other tips from the book, such as the
floating-point based random generator. This made its way into Moscow ML,
from there into Metis, from there back into the Metis version of Isabelle.
Here it caused huge performance issues, especially in parallel Poly/ML.
Later David Matthews improved that significantly, and the random generator
for Metis was replaced by an old word-based version according to Knuth.
Nonetheless, we still have the real-based Library.random from "ML for the
working programmer", because without it quickcheck performs really bad.
See also
http://dilbert.com/dyn/str_strip/000000000/00000000/0000000/000000/00000/2000/300/2318/2318.strip.gif
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
