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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
