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

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. Even when I delete the whole
> line, PolyML and the JVM keep running at 100% for minutes and I don't
> get any updates in the output or state buffer any more. I really have to
> shut down Isabelle/jEdit and restart to get back to work. This never
> happened to me with Isabelle2016 in the past six months.
> In the test, I ran Isabelle with the default settings on a quad core
> Intel from 4 years ago with 16GB of RAM under Ubuntu 14.04.

I think these are just variations on the old theme of Denial-of-Service
attack on the Prover IDE by massive markup reports. Here it is the
backtracking from "transfer" to "simp", which is invoked afresh each
time, with repeated reports. Thus the IDE is busy stacking up duplicate
markup trees, and reactivity of interrupts is generally delayed -- it
should stop eventually, though.

The same happens in Isabelle2016 already, and probably several earlier
releases. It is unclear to me, why the problem has now more impact in

Anyway, in changesets and I have
reworked that a bit to produce PIDE markup exactly once.

This can be tried out with the nightly snapshot from (produced in approx. 2h when all works

There will be also a formal release candidate Isabelle2016-1-RC1,
probably within 24h.


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