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