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,
* Second attempt to get ML task termination right, while the user
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
https://bitbucket.org/isabelle_project/isabelle-release/issues or via
This archive was generated by a fusion of
Pipermail (Mailman edition) and