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



Dear Makarius,

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.

Andreas

On 07/10/16 10:10, Makarius wrote:
Dear Isabelle users,

the year 2016 is an "Isabelle leap-year", with more than one release.
(The usual distance between regular releases is 8-10 months.)

Many changes and improvements have been accumulated in the past few
months. A preview of what is coming is available here:
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0

This corresponds to Isabelle/666c7475f4f7 and AFP/1e958cc1942e. Note
that the website and documentation still need to be updated.


Despite the name "Isabelle2016-1", this is not a revised version of
Isabelle2016, but a completely new major release. See also
the NEWS file
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0/dist/Isabelle2016-1-RC0/doc/NEWS.html

When discussing problems, observations, suggestions, etc. the mail
subject line should be changed to something meaningful (but the release
candidate number still given in the message body).


	Makarius





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