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