[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Makarius]

On Wed, 1 Sep 2010, Johannes Hölzl wrote:

> The Approximation theory only uses relfection and the code generator
> (with setup for code integer and efficient nat). Last year the usage of
> Unsynchronized.ref was remove in reflection. Since this time the
> approximation method should not use any references.
>
> 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

This means it could be some problem almost everywhere, say in the code 
generator.  Or if the proofs are driving the system to the edege 
concerning memory requirements (which are also higher in parallel mode) it 
could be some spurious Interrupt that is handled accidentally by 
the infamous "handle _" still lurking in code occasionally.

In the end it could as well be a side-effect of some (ongoing) 
rearrangements of how the system manages theory and proof checking.

Another possibility: side-effect of an adhoc change that I did on your 
oracle code (see 3c3b4ad683d5) that fits perfectly well into the presumed 
time range of introducing the problem.


> Is it possible to get a more detailed exception trace?

With Toplevel.debug := true (in ROOT.ML) you get global exception traces 
for actual failures.  This does not cover plain empty result sequence of 
proof method application, because that is not a failure in the execution
only in the search process.


 	Makarius