[isabelle-dev] Recent instabilities of HOL-Decision_Procs

Makarius makarius at sketis.net
Wed Sep 8 14:42:09 CEST 2010


On Mon, 6 Sep 2010, Johannes Hölzl wrote:

> However I have not yet access to macbroy6 so I don't know if there is a 
> difference in reproducing the error.

There is nothing specific to macbroy6 here -- it happens equally on 
macbroy2, or another 4-core Linux box that I have tried.  The critical bit 
is polyml-5.4.0 together with parallel proofs.  (I did have a sequential 
polyml-svn isatest for many months, without ever encountering the 
problem.)


 	Makarius


More information about the isabelle-dev mailing list