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
lxbroy10 (x86-linux):

97f16ada519c 2m16.102s
18f3d341f8c0 2m22.646s
Isabelle2016-1 2m19.796s


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
versions above.


Of course, the example is pathological in any case. It is just a matter
how non-termination is presented to the user.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.