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.

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.