Re: [isabelle] nonterminating simp terminates without output



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.