Re: [isabelle] nonterminating simp terminates without output
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:
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.)
lemma [simp]: "length xs = length (rev xs)"
lemma "P (length xs)"
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 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
The corresponding repository versions of Isabelle and AFP are
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and