Re: [isabelle] nonterminating simp terminates without output
On 06/10/17 15:21, Dmitriy Traytel wrote:
> But it seems that the amount of "patience" needed has reduced (compared to Isabelle2016-1). For both, I use the default ML_OPTIONS="-H 500".
I have made some more experiments. This command-line invocation works
best to see the error:
$ isabelle process -T Scratch
### Warning - Unable to increase stack - interrupting thread
Exception- Interrupt raised
To compare the amount of "patience" required, here are some results on
In contrast, I did see a difference on my home machine (x86-linux):
Isabelle2017-RC3: approx. 5min
Isabelle2016-1: approx. 44min
I am unsure which side-conditions can cause such an effect.
Also note that the Poly/ML version is essentially the same in all
Of course, the example is pathological in any case. It is just a matter
how non-termination is presented to the user.
This archive was generated by a fusion of
Pipermail (Mailman edition) and