Re: [isabelle] Isabelle2013-2-RC2 available for testing


process termination upon exit now seems to work well under OS X.

I still could get the Isabelle interaction to 'freeze' after continuously editing after a non-terminating "by (intro TrueE)" for about 30 seconds. So the situation is greatly improved compared to RC1. I then waited for about 5 minutes without any change, then after removing the non-terminating command it required waiting about 2 minutes until the command was finally interrupted and interaction came back.


P.s. This isn't a regression but when hovering over items in the Sidekick panel the height of the status bar changes and causes half of the UI to 'jump' around.

Am 28.11.13 15:34, schrieb Makarius:
Dear Isabelle users,

this is yet another release candidate for the second attempt to make a stable release of Isabelle this autumn:

The final Isabelle2013-2 should appear next week, unless further problems show up.

Notable changes versus Isabelle2013-2-RC1:

  * Reactivated Isabelle/Scala kill command for external processes on Mac
    OS X (e.g. poly), after 6 months of suffering from some Ubuntu/Debian
    Linux workaround that did not take Apple's BSD into account.

  * More status information about commands that are interrupted
    accidentally (via physical event or Poly/ML runtime system signal,
    e.g. out-of-memory).

  * Second attempt to get ML task termination right, while the user
    continues editing.

There should not be any incompatibilites wrt. Isabelle2013-1, which means everybody who is already on the latest release can try out the new release candidate without any extra efforts.

Ongoing changes were motivated by a really stable release of Isabelle/jEdit, but such delicate details of Isabelle command execution can also affect TTY and Proof General. I've have made some basic tests of the latter, but have problems recalling how manual script management used to work.

Observations from testing release candidates may be discussed here on isabelle-users (not isabelle-dev), on the bitbucket tracker or via private mail.


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