[isabelle-dev] Datatypes & Isatest failures

Makarius makarius at sketis.net
Mon Sep 29 15:51:52 CEST 2014

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.


More information about the isabelle-dev mailing list