[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Johannes Hölzl]

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:
[..]

> This only happenes when running in parallel mode, which is the default
> on modern hardware for quite some time already.  I estimate the
> probability of the incident 5-10% -- which makes it a bit hard to
> bisect in the change history.

If we add 6 times the test cases to Approximate_Ex we would get a
incident rate of 50% (or 21 times for 90%). I don't know if this is a
good idea.

> In general there are two main ways to make the behaviour of proof tools 
> depend on the weather:
> 
>    * real-time timeouts
> 
>    * Unsynchronized.ref
> 
> The latter are being shot at since 2-3 years already, and need to 
> disappear altogether for tools that care about surviving the next big 
> reform in user interaction, where the assumption of a single execution 
> path is plain wrong.  (For the moment Proof General still incurs a drastic 
> sequentialization that makes unsafes tool appear to work.)

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

Is it possible to get a more detailed exception trace?

 - Johannes


> The "configuration option" concept introduced some time ago provides an 
> easy drop-in replacement for bool/int/string options, even with the 
> possibility for process-global defaults (such as for simp trace etc.). It 
> also does the proper job concerning "localization".  This avoids one 
> obsolete concept (Unsynchronized.ref) being replaced by another one 
> (global theory-only parameters).
> 
> Going beyond bool/in/string is also possible, but requires a bit extra 
> work with attribute syntax (and Generic_Data).
> 
> 
>  	Makarius