Re: [isabelle] nonterminating simp terminates without output



Hi Andreas,

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

Dmitriy

> On 6 Oct 2017, at 15:09, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 
> Hi Dmitriy,
> 
> Red errors in jedit without a message are nothing new in Isabelle2017. I've also seen them in Isabelle2016-1 in case the PolyML runs out of memory, e.g., a non-terminating value [code] command which constructs ever larger terms (e.g. an infinite codatatype value). Then the command just showed a red error mark without any error message. In Isabelle2016-1, I haven't seen this happen with simp, though, but maybe I was never patient enough. But I suspect this is precisely what is happening in your example, simp will create increasingly large terms.
> 
> Andreas
> 
> On 06/10/17 14:54, Dmitriy Traytel wrote:
>> Hi Makarius,
>> a student in our Isabelle-course has alerted me about the following behavior in Isabelle2017-RC2. (I'm currently traveling and can't test RC3.)
>> theory Scratch
>>   imports Main
>> begin
>> lemma [simp]: "length xs = length (rev xs)"
>>   by simp
>> lemma "P (length xs)"
>>   by simp
>> end
>> The second call to simp will turn from purple to red after a few minutes on my (and the student's) machine without outputting anything. In Isabelle2016-1, I couldn't reproduce this behavior (i.e., it would stay purple). The fact that it turns red is at least better than what happened in Isabelle2013-1, but it still can be confusing. Is this happening on purpose?
>> Dmitriy
>>> On 23 Sep 2017, at 15:52, Makarius <makarius at sketis.net> wrote:
>>> 
>>> Dear Isabelle users,
>>> 
>>> the coming Isabelle2017 release is scheduled for the second week of
>>> October 2017. Thus there is still some time left for testing of release
>>> candidates, presently http://isabelle.in.tum.de/website-Isabelle2017-RC3
>>> 
>>> Everything should be now ready and complete, including the "system" and
>>> "jedit" manuals.
>>> 
>>> 
>>> The corresponding repository versions of Isabelle and AFP are
>>> https://bitbucket.org/isabelle_project/isabelle-release/commits/4f73201b8043
>>> and
>>> https://bitbucket.org/isa-afp/afp-devel/commits/dcf4dc3a3594
>>> 
>>> See also http://sketis.net/2017/release-candidates-for-isabelle2017 for
>>> notable changes within the line of release candidate.
>>> 
>>> 
>>> When posting problems, observations, suggestions, etc. the mail
>>> subject line should be changed to something meaningful, and the
>>> particular Isabelle version given in the message body.
>>> 
>>> 
>>> 	Makarius
>>> 





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