On Wed, 1 Sep 2010, Johannes Hölzl wrote:
Am Mittwoch, den 01.09.2010, 15:40 +0200 schrieb Makarius:
For some week or so there are sparadic failures of HOL-Decision_Procs like
this:
[..]
The special things about the approximation method are:
* uses reflection (i.e. the generated code as an oracle)
* probably the only user of large ML-integers and division
* long running proofs
Is it possible to get a more detailed exception trace?
There is some chance that it is due to large ML integers in the parallel
setting -- this is a pre-5.4 version of Poly/ML where arbitrary precision
arithmetic has been changed significantly. (It can optionally use GNU MP,
although I did not compile it into that particular binary, IIRC.)
The failure has now repeatly occured here:
*** Theory loader: undefined theory entry for "Approximation_Ex"
*** Failed to finish proof
*** At command "by" (line 42 of
"/mnt/nfsbroy/home/isatest/isadist/Isabelle_04-Sep-2010/src/HOL/Decision_Procs/ex/Approximation_Ex.thy")
i.e. this proof:
lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
by (approximation 80)
Is there a way to report the internal results produced here? Then we can
show David Matthews some more concrete problem report than "Failed to
finish proof".
Makarius_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
