[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Johannes Hölzl]

Am Samstag, den 04.09.2010, 14:06 +0200 schrieb 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".

Attached is the code generated by Approximate_Ex line 42. I generated it
by using ML {* ML_Context.trace := true *}. I also added some functions
from integer.ML to work properly on pure polyml.

The result needs to contain:

  val res = true : bool

when the computation was successfully.

There are two version, one is using reals when comparing two Floats.
This changed now to use integers, which also results in a lot of less
code generated (and it is also faster). However I have not yet access to
macbroy6 so I don't know if there is a difference in reproducing the
error.

 - Johannes

-------------- next part --------------
A non-text attachment was scrubbed...
Name: approximate.ML
Type: text/x-ocaml
Size: 40774 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100906/0d6434a3/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: approximate_real.ML
Type: text/x-ocaml
Size: 61533 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100906/0d6434a3/attachment-0005.bin>