Re: [isabelle] nonterminating simp terminates without output

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.


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

lemma [simp]: "length xs = length (rev xs)"
   by simp

lemma "P (length xs)"
   by simp


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?


On 23 Sep 2017, at 15:52, Makarius <makarius at> 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

Everything should be now ready and complete, including the "system" and
"jedit" manuals.

The corresponding repository versions of Isabelle and AFP are

See also 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.


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