[isabelle-dev] Datatypes & Isatest failures
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