*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] nonterminating simp terminates without output*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Fri, 6 Oct 2017 15:21:39 +0200*Cc*: Makarius <makarius at sketis.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <70552bdf-680b-2886-942d-ab237f30bfe2@inf.ethz.ch>*References*: <aefe421a-ba68-c0c2-e057-211111860bbf@sketis.net> <99BAF758-DE06-458F-8AED-75BAB76D5810@inf.ethz.ch> <70552bdf-680b-2886-942d-ab237f30bfe2@inf.ethz.ch>

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 >>>

**Follow-Ups**:**Re: [isabelle] nonterminating simp terminates without output***From:*Makarius

**References**:**Re: [isabelle] nonterminating simp terminates without output***From:*Dmitriy Traytel

**Re: [isabelle] nonterminating simp terminates without output***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] nonterminating simp terminates without output
- Next by Date: Re: [isabelle] nonterminating simp terminates without output
- Previous by Thread: Re: [isabelle] nonterminating simp terminates without output
- Next by Thread: Re: [isabelle] nonterminating simp terminates without output
- Cl-isabelle-users October 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list