[isabelle-dev] Merge-Sort Implementation

[Makarius]

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