[isabelle-dev] Datatypes & Isatest failures

[Makarius]

On Thu, 25 Sep 2014, Makarius wrote:

> HOL-Proofs is important in various ways: theoretically it opens the 
> possibility for independent checking of proofs by a different system, 
> and thus raising the level of confidence in Isabelle results; 
> practically it indicates how close we are to the next concrete wall of 
> resource limits.
>
> Moreover, Poly/ML 5.3.0 is still important, since it has more thorough 
> exception trace, which is required in hard cases of ML diagnostics.
>
>
> We've had such unclear situations occasionally in the past, and usually 
> managed to get things under control again, after looking 2 or 3 times 
> more closely.  Softening concrete walls has always been a routine trick 
> in long-term Isabelle maintenance.

After some experiments this morning, my impression is that there is 
nothing special, just a very old test machine.  I have changed that in 
ab4b94892c4c, so lets hope for the best for tomorrow's isatest run.


 	Makarius