[isabelle-dev] Datatypes & Isatest failures
makarius at sketis.net
Thu Sep 25 21:25:15 CEST 2014
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,
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
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.
More information about the isabelle-dev