[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Makarius]

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