On Mon, 6 Sep 2010, Johannes Hölzl wrote:
Attached is the code generated by Approximate_Ex line 42. I generated it
by using ML {* ML_Context.trace := true *}. I also added some functions
from integer.ML to work properly on pure polyml.
The result needs to contain:
val res = true : bool
whe
On Mon, 6 Sep 2010, Johannes Hölzl wrote:
However I have not yet access to macbroy6 so I don't know if there is a
difference in reproducing the error.
There is nothing specific to macbroy6 here -- it happens equally on
macbroy2, or another 4-core Linux box that I have tried. The critical bit
> The failure has now repeatly occured here:
>
> *** Theory loader: undefined theory entry for "Approximation_Ex"
> *** Failed to finish proof
> *** At command "by" (line 42 of
> "/mnt/nfsbroy/home/isatest/isadist/Isabelle_04-Sep-2010/src/HOL/Decision_Procs/ex/Approximation_Ex.thy")
>
>
> i.e. t
On Wed, 1 Sep 2010, Johannes Hölzl wrote:
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:
[..]
The special things about the approximation method are:
* uses reflection (i.e. the generated code as an o
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 referenc
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
> probabi
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) (
