Re: [isabelle] Isabelle2016-1-RC0 available for testing



Hi Makarius,

All the concrete cases in which I ran into this problem have been fixed now. But I've attached a small example that shows the problem. The lemma has a pointless assumption, but this is only to get the theorem sufficiently large such that transfer runs for a while

As is, the proof of the lemma goes through, but if you delete the declaration of map_concat as a simp rule, then it will not, but keep running for quite some time (if your patience is longer than mine, just add a few more universal quantifiers in the assumptions of the lemma; the backtracking in transfer grows exponentially with the number of quantifiers). What I then typically do is to change the non-terminating line of proof, usually by adding a space somewhere in transfer (i.e., "by tra nsfer simp") or completely deleting it.

But despite these changes, the proof method keeps running and Isabelle/jEdit does no longer update the Output and State panels any more.

Best,
Andreas

On 25/10/16 14:15, Makarius wrote:
On 10/10/16 17:07, Andreas Lochbihler wrote:

I played a bit with RC0 and noticed that reactivity seems to be a bit
lower than with Isabelle2016. In particular, when I have a
non-terminating proof command like

  subgoal by transfer simp

and (due to some changes in the theory above) the proof loops, then I
have found no way to interrupt the proof.

Someone else reported a similar problem some weeks ago.

Is there a concrete example somewhere, that shows the effect?


	Makarius

Attachment: Scratch.thy
Description: application/example



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