[isabelle-dev] Recent instabilities of HOL-Decision_Procs

[Makarius]

For some week or so there are sparadic failures of HOL-Decision_Procs like 
this:

HOL-Decision_Procs FAILED
(see also /Users/makarius/.isabelle/heaps//polyml-5.4.0_x86_64-darwin/log/HOL-Decision_Procs)
            (Var 0))))))
  (replicate 3 None) [0, 0, 0]
approx_tse_form 30 3 1
  (Bound (Var 0) (Num (Float 0 0)) (Num (Float 1 0))
    (LessEqual (Power (Var 0) 2) (Var 0)))
### Ignoring duplicate rewrite rule:
### Suc ?n1 == ?n1 + 1
### Ignoring duplicate rewrite rule:
### Suc ?n1 == ?n1 + 1
### Ignoring duplicate rewrite rule:
### Suc ?n1 == ?n1 + 1
### Ignoring duplicate rewrite rule:
### Suc ?n1 == ?n1 + 1
### Ignoring duplicate rewrite rule:
### Suc ?n1 == ?n1 + 1
*** Theory loader: undefined theory entry for "Approximation_Ex"
*** Failed to finish proof
*** At command "by" (line 42 of 
"/Users/makarius/isabelle/repos/src/HOL/Decision_Procs/ex/Approximation_Ex.thy")
Exception- TOPLEVEL_ERROR raised
*** ML error

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.

The line 42 above is an invocation of the "approximation" method, but it 
might also happen in other places.

Does anybody have any idea what could be wrong in this particular 
situation?


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 "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