[isabelle-dev] Datatypes & Isatest failures

[Makarius]

On Thu, 25 Sep 2014, Jasmin Christian Blanchette wrote:

> Hi Florian,
>
> Thanks for your input.
>
>>> 1. Increase the timeout from 3600 s to, e.g. 4800.
>
> [...]
>
>> So, (1) is my opinion.
>
> Unfortunately, that didn't do the trick (cf. 7f30ec82fe40, 
> e4d540c0dd57).

The change e4d540c0dd57 was my reaction in the sense of (1) -- although I 
am presently not quite up-to-date concerning open threads and this 
particular situation.


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.


 	Makarius